proposition: Fact ra_div_val n m : m <> 0 -> ⟦ra_div⟧ (n##m##vec_nil) (div n m).
proof: Proof. intros Hm. generalize (div_rem_spec1 n m) (div_rem_spec2 n Hm); intros H1 H2. destruct (ra_div_spec n Hm) as (k & H3 & H4). assert (k = div n m); try lia; subst; auto. clear H3. rewrite Nat.mul_succ_r in H4. apply (@div_rem_uniq _ k (n-m*k) (div n m) (rem n m) Hm); try lia. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list gcd crt sums finite pos vec) Undecidability.MuRec.Util(recalg recomp prim_min)