proposition: Fact ra_iter_rel v e : ⟦ra_iter⟧ v e <-> e = iter f (vec_pos v pos0) (vec_pos v pos1).
proof: Proof. Proof using Hf. vec split v with k; vec split v with x; vec nil v. split. + intros H; apply ra_rel_fun with (1 := H), ra_iter_val. + intros ->; apply ra_iter_val. 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)