proposition: Fact ra_prim_min_val i v : ⟦ra_prim_min⟧ (i##v) (prim_min (f v) i).
proof: Proof. Proof using Hf. unfold ra_prim_min. rewrite ra_iter_n_rel with (f := fun _ => 0) (g := fun w i => match f w i with 0 => i | _ => S i end). + unfold prim_min; simpl; auto. + intros; rewrite ra_cst_n_rel; tauto. + intros; apply ag_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)