proposition: Lemma cltSSP n m: cardinalp n -> cardinalp m -> ((csucc n <c csucc m) <-> (n <c m)).
proof: Proof. move => cn cm; split; last by apply:cltSS. move => [pa pb]; split; first by move/(cleSSP cn cm) : pa. by move => h; case: pb; rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)