Fstar is having trouble with this if we were to remove "--z3cliopt 'smt.arith.nl=false'"

MatrixIndexTransform.fst

module MatrixIndexTransform

let ( *) (x y: int) : (t:int{(x>0 /\ y>0) ==> t>0}) = op_Multiply x y

let under (k: pos) = x:nat{x<k}
 
let flattened_index_is_under_flattened_size (m n: pos) (i: under m) (j: under n) 
  : Lemma ((((i*n)+j)) < m*n) = assert (i*n <= (m-1)*n)
   
let get_ij (m n: pos) (i:under m) (j: under n) : under (m*n) = flattened_index_is_under_flattened_size m n i j; i*n + j

let get_i (m n: pos) (ij: under (m*n)) : under m = ij / n
let get_j (m n: pos) (ij: under (m*n)) : under n = ij % n

let consistency_of_ij (m n: pos) (ij: under (m*n)) : Lemma (get_ij m n (get_i m n ij) (get_j m n ij) == ij) = ()

let get_ji (m n: pos) (ij: under (m*n)) : under (n*m) 
  = 
  assert (get_j m n ij < m*n);
  assert (get_i m n ij < m);
  flattened_index_is_under_flattened_size n m (get_j m n ij) (get_i m n ij);
  (get_j m n ij)*m + (get_i m n ij)

open FStar.Math.Lemmas

let lemma_jm_plus_i_mod_m (m: pos) (i: under m) (j: nat) : Lemma ((j*m+i)%m = i) = lemma_mod_plus i j m
let lemma_jm_plus_i_div_m (m: pos) (i: under m) (j: nat) : Lemma ((j*m+i)/m = j) = lemma_mod_plus i j m

#push-options "--z3cliopt 'smt.arith.nl=false'"
let dual_indices (m n: pos) (ij: under (m*n)) : Lemma (
     (get_j n m (get_ji m n ij) = get_i m n ij) /\
     (get_i n m (get_ji m n ij) = get_j m n ij)
 ) = 
    let i = get_i m n ij in
    let j = get_j m n ij in
    let ji = get_ji m n ij in
    consistency_of_ij m n ij;
    assert (i*n+j == ij); 
    calc (=) {
      get_j n m (get_ji m n ij); 
      == {} 
      ji % m;
      = {}
      (j*m+i)%m;
      = { lemma_jm_plus_i_mod_m m i j }
      i;      
    }; 
    consistency_of_ij n m ji;
    calc (=) {
      get_i n m (get_ji m n ij); 
      = {}
      get_i n m ji;
      = {}      
      ((get_j m n ij)*m + (get_i m n ij)) / m;
      = { lemma_jm_plus_i_div_m m i j  }    
      j;
    }  
#pop-options