proposition: Lemma exists_min (cond : nat -> Prop) (H: exists n, cond n) : exists n, cond n /\ forall j, j < n -> ~ cond j.
proof: Proof. desc; assert (IN: In n (List.seq 0 (S n))). by apply in_seq; lia. assert (L: findP cond (List.seq 0 (S n)) < S n). { rewrite <- (seq_length (S n) 0) at 2. revert IN; generalize (List.seq 0 (S n)). induction l; ins; desf; intuition. } forward eapply findP_spec with (cond := cond) (l := List.seq 0 (S n)) (d := 0) as X; desc; eauto. rewrite seq_nth in *; ins. eexists; split; eauto; ins; specialize_full X0; eauto. rewrite seq_nth in *; ins; lia. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt