proposition: Fact ra_plus_rel v e : ⟦ra_plus⟧ v e <-> e = vec_head v + vec_head (vec_tail v).
proof: Proof. unfold ra_plus; simpl. rewrite ra_iter_rel with (f := S). + vec split v with n; vec split v with m; vec nil v; simpl. apply eq_equiv; induction n; simpl; f_equal; auto. + intros; simpl; unfold s_succ; simpl; tauto. 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)