proposition: Lemma aleph_lt_ltc x y: x <o y -> \aleph x <c \aleph y.
proof: Proof. move=> xy; move: (xy) => [[ox oy _] _]. apply /(oclt3 (CS_aleph ox)(CS_aleph oy));exact:aleph_lt_lto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)