proposition: Lemma lt_n_sup : forall (x : Ensf) (n : nat), dans (natural n) x -> n < sup x.
proof: Proof. simple induction x. intros. absurd (dans (natural n) empty); auto. intros a b H n H0. replace (sup (add a b)) with (max (Z a) (sup b)). 2: auto. cut (n < Z a \/ n < sup b). intro. elim H1; auto. intros; apply lt_le_trans with (Z a); auto with arith. intros; apply lt_le_trans with (sup b); auto with arith. cut (a = natural n :>Elt \/ dans (natural n) b). 2: apply dans_add; auto. intro. elim H1. intro; left. rewrite H2; apply lt_n_Z. intro; right. apply H; assumption. Qed.
imports: Le Lt Ensf Arith.Max