proposition: Lemma setU1_succ_card x n: cardinalp n -> cardinal x = csucc n -> exists u v, [/\ x = u +s1 v, ~(inc v u) & cardinal u = n].
proof: Proof. move=> cn cx. case: (emptyset_dichot x) => h. by case:(@succ_nz n); rewrite - cx h cardinal_set0. move: h=> [y yx]. have xt:= (setC1_K yx). exists (x -s1 y), y;split =>//;first by apply: setC1_1. apply: csucc_inj; fprops. by rewrite - cx -xt (csucc_pr1 x y) xt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)