proposition: Fact ra_iter_n_rel v e : ⟦ra_iter_n⟧ v e <-> e = iter (g (vec_tail v)) (vec_pos v pos0) (f (vec_tail v)).
proof: Proof. Proof using Hf Hg. vec split v with i; split. + intros H; apply ra_rel_fun with (1 := H), ra_iter_n_val. + intros; subst; apply ra_iter_n_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)