proposition: Lemma csucc_pr a b: ~ (inc b a) -> cardinal (a +s1 b) = csucc (cardinal a).
proof: Proof. move=> bna; rewrite csuccE; apply/card_eqP. have ana := (ordinal_irreflexive (OS_cardinal (CS_cardinal a))). have [f fp]: a \Eq cardinal a by apply/card_eqP; aw. by apply:(succ_inf_aux_p1 bna ana); exists f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)