proposition: Fact prim_min_spec n : f n = 0 -> f (prim_min n) = 0 /\ forall i, i < prim_min n -> f i <> 0.
proof: Proof. intros Hn. destruct (min_f Hn) as (k & H1 & H2 & H3). assert (prim_min n = k) as H4. { unfold prim_min. unfold prim_min_rec. replace n with (n-k+k) by lia. rewrite iter_plus. fold (prim_min_rec k 0). rewrite prim_min_rec_spec_0 with (n := k) (a := 0); auto. rewrite Nat.add_comm; apply prim_min_rec_spec_1; auto. intros; apply H3; lia. } rewrite H4; auto. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat)