proposition: Lemma lt_le_trans : forall a b c, a < b -> b <= c -> a < c.
proof: Proof. Proof (Lt_Le_trans AX1). Lemma le_trans : forall a b c, a <= b -> b <= c -> a <= c. Proof (Le_trans AX1). Lemma lt_irrefl : forall a, ~ (a < a). Proof. intros a Ha; now apply ( @Lt_irreflexive Ord lt AX1 a). Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)