proposition: Lemma cleSltP a: natp a -> forall b, (csucc a <=c b <-> a <c b).
proof: Proof. move=> aN b. case (p_or_not_p (cardinalp b)) => h; last first. split => lt;case: h; [ exact :proj32 lt | exact :proj32_1 lt]. case: (Nat_dichot h) => H; first by apply /(cleSlt0P (CS_nat aN) H). split => _; first by apply:(clt_fin_inf (Nat_hi aN)). apply:(cle_fin_inf (Nat_hi (NS_succ aN)) H). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)