proposition: Lemma aleph_le_lec x y: x <=o y -> \aleph x <=c \aleph y.
proof: Proof. move=> xy. apply /(ocle3 (CS_aleph (proj31 xy))(CS_aleph (proj32 xy)));exact:aleph_le_leo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)