proposition: Lemma csucc_pr3 x: csucc (cardinal x) = x +c \1c.
proof: Proof. move:(ordinal_irreflexive (OS_cardinal (CS_cardinal x))) => w. rewrite - (double_cardinal x) - (csucc_pr w). by rewrite(csum2_pr5(disjoint_setU1 w)) - csum2cr csum2cl cardinal_set1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)