proposition: Lemma le_not_gt : forall a b, a <= b -> ~ b < a.
proof: Proof. intros a b H; case (le_eq_or_lt H). - intro;subst b;apply lt_irrefl. - intros H0 H1;case (@lt_irrefl a);eapply lt_trans;eauto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)