proposition: Lemma Exercice6_8c E: infinite_set E -> let s1 := Zo (\Po (coarse E)) (fun r => order_on r E) in let s2 := Zo (\Po (coarse E))(fun r => worder_on r E) in (s1 =c s2 /\ s2 =c (\Po E)).
proof: Proof. move=> isE s1 s2. have: sub s2 s1 by move=> r /Zo_P [pa [[pb1 pb2] pc]]; apply /Zo_P. move/ (sub_smaller) => le1. have /sub_smaller: sub s1 (\Po (coarse E)) by apply: Zo_S. rewrite (Exercise6_4a isE) => le3. move: (Exercice6_8b E); rewrite (Exercice6_5h isE) -/s2 => le4. split; [ exact:(cleA (cleT le3 le4) le1) | exact: (cleA (cleT le1 le3) le4)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)