proposition: Lemma Unbounded_ge (alpha : Ord) : Unbounded (ge alpha).
proof: Proof. Proof with auto with schutte. red. intros x ; tricho alpha x H3. - exists (succ x);split ... right; apply lt_trans with x; trivial ... - subst alpha; exists (succ x) ; split ... red;red ... - exists (succ alpha); split. + red;red ... + apply lt_trans with alpha ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)