proposition: Lemma sup_mono (X Y : Ensemble Ord) : Countable X -> Countable Y -> (forall x, In X x -> exists y, In Y y /\ x <= y) -> |_| X <= |_| Y.
proof: Proof. intros H H0 H1; apply sup_least_upper_bound; auto with schutte. intros x Hx; case (H1 x Hx); intros y (Hy,Hy'). apply le_trans with y;auto with schutte. apply sup_upper_bound;auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)