proposition: Lemma Exercise4_11i M N: max_pure A R M -> max_pure A R N -> M \Eq N.
proof: Proof. move => pM pN. case: (finite_or_infinite_set (N -s M)) => h1; first by apply:EqS;apply: Exercise4_11g. case: (finite_or_infinite_set (M -s N)) => h2; first by apply: Exercise4_11g. move: (Exercise4_11h pM pN) (Exercise4_11h pN pM). set C1 := (M -s N); set C2 := (N -s M) => s1 s2. move: (cleT (sub_smaller s1) (csum_pr1 _)); aw => le1. move: (cleT (sub_smaller s2) (csum_pr1 _)); aw => le2. set f1:= (Lg C2 (fun a : Set => cardinal (Vg (Lg C2 [eta Ex4_11EM M]) a))). set f2:= (Lg C1 (fun a : Set => cardinal (Vg (Lg C1 [eta Ex4_11EM N]) a))). have fg1 : fgraph f1 by rewrite /f1; fprops. have fg2 : fgraph f2 by rewrite /f2; fprops. have h1': infinite_c (cardinal C2) by move: h1; move /infinite_setP. have h2': infinite_c (cardinal C1) by move: h2; move /infinite_setP. have cd1: cardinal (domain f1) <=c cardinal C2 by rewrite /f1; aw; fprops. have cd2: cardinal (domain f2) <=c cardinal C1 by rewrite /f2; aw; fprops. move: mnr => [q1 q2 q3 q4]. have l1: (forall i, inc i (domain f1) -> Vg f1 i <=c cardinal C2). rewrite /f1; aw; move => i idf; rewrite !LgV//; apply: cle_fin_inf => //. move: idf => /setC_P[i1 i2]. have i3: inc i (A -s M) by apply /setC_P;split => //;apply: (proj31 pN _ i1). move: (Exercise4_11d pM i3) => [ _ tf]. move: (q2 _ tf); apply: sub_finite_set; fprops. have l2: (forall i, inc i (domain f2) -> Vg f2 i <=c cardinal C1). rewrite /f2; aw. move => i idf; rewrite !LgV//; apply: cle_fin_inf => //. move: idf => /setC_P [i1 i2]. have i3: inc i (A -s N) by apply /setC_P;split => //; apply:(proj31 pM _ i1). move: (Exercise4_11d pN i3) => [ _ tf]. move: (q2 _ tf); apply: sub_finite_set; fprops. move: (cleT le1 (notbig_family_sum h1' cd1 l1)) => l3. move: (cleT le2 (notbig_family_sum h2' cd2 l2)) => l4. apply/card_eqP; apply: cardinal_setC3; exact: (cleA l3 l4). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)