proposition: Fact ra_div_rel v e : vec_pos v pos1 <> 0 -> ⟦ra_div⟧ v e <-> e = div (vec_pos v pos0) (vec_pos v pos1).
proof: Proof. vec split v with a; vec split v with b; vec nil v; intros H. split. + intros H1; apply ra_rel_fun with (1 := H1), ra_div_val; auto. + intros; subst; apply ra_div_val; auto. 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)