proposition: Theorem csucc_inj: {when cardinalp &, injective csucc}.
proof: Proof. move=> a b ca cb /=; rewrite !csuccE; move /card_eqP. by move/(succ_inf_aux_ord (proj1 ca) (proj1 cb)) /card_eqP; rewrite ! card_card. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)