proposition: Lemma not_gt_le : forall a b, ~ b < a -> a <= b.
proof: Proof. intros a b H1; tricho a b H2; auto with schutte; contradiction. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)