proposition: Lemma aleph_ltc_lt x y: ordinalp x -> ordinalp y -> \aleph x <c \aleph y -> x <o y.
proof: Proof. by move => ox oy lt; apply: aleph_lto_lt => //; apply:oclt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)