proposition: Lemma succ_injective2 a b: cardinalp a -> cardinalp b -> a +c \1c = b +c \1c -> a = b.
proof: Proof. move=> ca cb hyp. suff: equipotent a b. by move/card_eqP; rewrite (card_card ca) (card_card cb). move: (disjointU2_pr3 a card_one C1_ne_C0) => eq1. move: (disjointU2_pr3 b card_one C1_ne_C0) => eq2. rewrite -hyp in eq2; clear hyp. move: (esym eq1) => /card_eqP [f [bf sf tf]] {eq1}. move: (esym eq2)=> /card_eqP[g [bg sg tg]] {eq2}. set (A0:= Vfs f (a *s1 C0)). set (B0:= Vfs g (b *s1 C0)). rewrite /card_one in sf sg. set xA:= J emptyset C0; set xB:= J emptyset C1. have main: (forall c h, bijection h -> source h = (c *s1 C0) \cup ((singleton emptyset) *s1 C1) -> let w:= Vfs h (c *s1 C0) in let v:= Vf h xB in [/\ ~(inc v w), target h = w \cup (singleton v) & c \Eq w]). move=> c h bh sh w v. move: (bij_function bh)=> fh. have sh1:sub (c *s1 C0) (source h) by rewrite sh; apply: subsetU2l. have sh2: inc xB (source h). rewrite sh; apply: subsetU2r; rewrite /xB;apply /indexed_P;aw;split;fprops. split. move /(Vf_image_P fh sh1) => [u vs vw]. have uW: (u = xB). by move: bh=> [[ _ ih] _]; apply: ih=>//; apply: sh1. move: vs; rewrite uW; move /indexed_P=> [_ _]; rewrite /xB; aww. set_extens t. move:bh => [_ sjh] tt; move:((proj2 sjh) _ tt)=> [y ys hy]. rewrite sh in ys; case /setU2_P: ys => p. apply /setU2_P; left; rewrite hy; apply /(Vf_image_P fh sh1); ex_tac. have yp: y = xB. move:p => /indexed_P; aw; move => [py Py Qy]. by apply: pair_exten; rewrite /xB; aww; move /set1_P: Py. rewrite hy yp -/v; apply /setU2_P; right; fprops. case /setU2_P. move /(Vf_image_P fh sh1)=> [u us ->]; Wtac. move /set1_P=> ->; rewrite /v; Wtac. apply: (EqT (Eq_indexed c C0)). exists (restriction1 h (c *s1 C0));split. by apply: restriction1_fb; move: bh => [ih _]. by rewrite /restriction1; aw. by rewrite /restriction1; aw. apply/card_eqP. move: (main _ _ bf sf) (main _ _ bg sg); clear main. simpl; fold A0 B0. move=> [nWxfA0 tfA /card_eqP ->][nWxfB0 tgB /card_eqP ->]. have tfg: target f = target g by ue. case: (equal_or_not (Vf f xB) (Vf g xB))=> efg. suff: (A0 = B0) by move=> ->. set_extens t => ts. have : (inc t (target f)) by rewrite tfA; apply: subsetU2l. rewrite tfg tgB;case /setU2_P =>//. move /set1_P;rewrite -efg =>tv; case: nWxfA0; ue. have : (inc t (target f)) by rewrite tfg tgB; apply: subsetU2l. rewrite tfA; case /setU2_P =>//. move /set1_P; rewrite efg =>tv; case: nWxfB0; ue. set (C0:= A0 \cap B0). have ->: (A0 = C0 \cup (singleton (Vf g xB))). set_extens t => ts. have : (inc t (target f)) by rewrite tfA;apply: subsetU2l. rewrite tfg tgB; case /setU2_P. by move=> tB; apply :setU2_1; apply: setI2_i. move /set1_P => ->; apply /setU2_P; right; fprops. case /setU2_P: ts; first by move/ setI2_P => []. move /set1_P => tu. have: (inc t (target f)). rewrite tfg tgB tu; fprops. by rewrite tfA; case/setU2_P =>// /set1_P tw; case: efg; rewrite -tu -tw. have ->: (B0 = C0 \cup (singleton (Vf f xB))). set_extens t => ts. have : (inc t (target g)) by rewrite tgB;apply: setU2_1. rewrite -tfg tfA; case /setU2_P. by move=> tB; apply: setU2_1; apply: setI2_i. move /set1_P => ->; apply /setU2_2; fprops. case /setU2_P: ts; first by move /setI2_P => []. move /set1_P => tu. have: (inc t (target f)). rewrite tfA; apply: setU2_2; aw; ue. rewrite tfg tgB; case /setU2_P =>// /set1_P tw. by case: efg; rewrite -tu -tw. rewrite !csucc_pr //;move /setI2_P => [] //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)