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.