proposition: Lemma aleph_lto_lt x y: ordinalp x -> ordinalp y -> \omega x <o \omega y -> x <o y.
proof: Proof. move => ox oy lt1. case: (oleT_el oy ox) => // h. case:(oltNge lt1 (aleph_le_leo h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)