proposition: Lemma aleph_inj x y: ordinalp x -> ordinalp y -> \omega x = \omega y -> x = y.
proof: Proof. move=> oa ob lef. by case: (oleT_ell oa ob) => // /aleph_lt_lto []; rewrite lef. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)