proposition: Lemma Exercise4_11g M N: max_pure A R M -> max_pure A R N -> finite_set (M -s N) -> M \Eq N.
proof: Proof. set C := (M -s N). have : C = (M -s N) by done. move: C; move => C cv mp mp' fsc; move: C fsc M N cv mp mp'. apply: finite_set_induction0. move => M M' iz mp mp'. symmetry in iz; move: (empty_setC iz) => l1. move: mp mp' => [mp0 mp1 mp2] [mp5 mp3 mp4]. rewrite (mp2 _ mp3 l1 mp5);fprops. move => C a Hrec naC M N cv Mp Np. have : inc a (C +s1 a) by fprops. rewrite cv; move => /setC_P [aM naN]. have aAN: inc a (A -s N) by apply /setC_P; split => //;apply (proj31 Mp). move:(Exercise4_11d Np aAN) => [seN teR]. case: (emptyset_dichot ((Ex4_11EM N a) -s M)) => esd. move: (empty_setC esd) => s1. have s2: sub ((Ex4_11EM N a) +s1 a) M by move => t; case /setU1_P; fprops => ->. by move: (proj32 Mp _ s2). move: esd => [b] /setC_P [bt nb]. move: (Exercise4_11f Np aAN bt). set T := ((N +s1 a) -s1 b) => mpT. have pa: C = M -s T. set_extens t. move => tc; apply /setC_P. have: inc t (C +s1 a) by fprops. rewrite cv => /setC_P [tm tn]; split => //. move /setC1_P => [] /setU1_P; case => // ta _;case: naC; ue. move => /setC_P [tm] /setC1_P aux. have ntb: t <> b by move=> tb; case: nb; ue. case: (equal_or_not t a) => nta. by case: aux; split; [ rewrite nta;fprops | exact]. case: (inc_or_not t N) => ntN; first by case: aux; split; [ fprops | exact]. have: inc t (C +s1 a) by rewrite cv; apply /setC_P; split. by case /setU1_P. apply /card_eqP. set s := (N +s1 a). have bs: inc b s by apply /setU1_P;left; apply: seN. have ias: inc a s by rewrite /s;fprops. move: (csucc_pr2 bs) (csucc_pr2 ias). rewrite (setU1_K naN); move => -> ss. have ca: cardinalp (cardinal N) by apply: CS_cardinal. have cb: cardinalp (cardinal (s -s1 b)) by apply: CS_cardinal. by rewrite - (csucc_inj cb ca ss);apply/card_eqP; apply:Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)