Library prelude.wf_minimal

Require Import Relations.
Require Import Classical.

 Variable U : Type.
 Variable lt : U -> U -> Prop.

 Hypothesis wf_lt : well_founded lt.

 Let le := fun x y => x=y \/ lt x y.
 Hypothesis tr : transitive U lt.

 Definition minimal := fun m => forall x, not (lt x m).

 Lemma not_all_not_ex' :
   forall P:U -> Prop, ~ (forall n:U, ~ P n) -> ex P .
 Proof.
  intros P H.
  elim (not_all_ex_not _ (fun n:U => ~ P n) H).
  intros n Pn; exists n.
  apply NNPP; trivial.
Qed.

 Theorem minimal_exists : forall u, exists m, le m u /\ minimal m.

intro u;pattern u;
eapply (well_founded_ind wf_lt).
 intros x Hx.
 apply not_all_not_ex'.
 intro H.
 case (classic (minimal x)).
 intro Hm.
 case (H x).
 split;auto.
 red.
 left;auto.
 intro.
 unfold minimal in H0.
 assert (exists x0:U, lt x0 x).
 apply not_all_not_ex'.
 auto.
 case H1;intros m' Hm'.
 case (Hx _ Hm').
 intros x0 (H2,H3).
 case (H x0);split;auto.
 case H2.
intro;subst m'.

 right;auto.
 right.

 apply tr with m';auto.
Qed.