proposition: Lemma colt1 a x: cardinalp x -> inc a x -> cardinal a <c x.
proof: Proof. move => cx ax; apply: (oclt3 (CS_cardinal a) cx). move/(oltP (OS_cardinal cx)): (ax) => lt1; move:(proj31_1 lt1) => oa. exact:(ole_ltT (cardinal_pr3 oa) lt1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)