proposition: Fact ra_rem_val n m : m <> 0 -> ⟦ra_rem⟧ (n##m##vec_nil) (rem n m).
proof: Proof. intros Hm. generalize (div_rem_spec1 n m) (ra_rem_val_0 n Hm); intros. replace (rem n m) with (n-m*div n m); auto. rewrite Nat.mul_comm; 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)