proposition: Lemma sup_out : forall x : Ensf, ~ dans (natural (sup x)) x.
proof: Proof. intro. red in |- *. intro. cut (sup x < sup x). change (~ sup x < sup x) in |- *. apply lt_irrefl. apply lt_n_sup. assumption. Qed.
imports: Le Lt Ensf Arith.Max