proposition: Lemma cleSlt0P a b: cardinalp a -> natp b -> (csucc a <=c b <-> a <c b).
proof: Proof. move => ca bN. split => hyp. by apply/(cltSSP ca (CS_nat bN)); apply/(cltSleP bN). by apply/(cltSleP bN) /(cltSSP ca (CS_nat bN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)