proposition: Lemma aleph_leo_le x y: ordinalp x -> ordinalp y -> \omega x <=o \omega y -> x <=o y.
proof: Proof. move=> oa ob lef. case: (oleT_el oa ob) => // aux. case: (oleNgt lef (aleph_lt_lto aux)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)