proposition: Lemma beth_M x y: x <o y -> beth x <c beth y.
proof: Proof. move: (proj1 beth_normal) => pa ineq. exact: (oclt3 (CS_beth (proj31_1 ineq))(CS_beth (proj32_1 ineq)) (pa _ _ ineq)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)