proposition: Lemma Exercice6_8b E: (cardinal (permutations E)) <=c (cardinal (Zo (\Po (coarse E)) (fun r => worder_on r E))).
proof: Proof. set s3 := permutations E; set s2 := Zo _ _. pose C f r:= graph_on (fun x y => gle r (Vf f x) (Vf f y)) E. have Cp1: forall f r, inc f s3 -> inc r s2 -> inc (C f r) s2. move=> f r => /Zo_P [] /functionsP [ff sf tf] bf. move /Zo_P => [] /setP_P rc [[or wor] sr]; apply: Zo_i. apply /setP_P; apply: Zo_S. have pa: forall a : Set, inc a E -> gle r (Vf f a) (Vf f a). by rewrite - sf => a aE; order_tac; rewrite sr -tf;Wtac. have sfr: substrate (C f r) = E. rewrite /C graph_on_sr //;split => //. have pb: order (C f r). rewrite /C; apply: order_from_rel1 => //. move=> x y z; simpl => le1 le2; order_tac. rewrite - sf => x y xE yE le1 le2; move: bf => [[_ injf] _]. apply: injf =>//; order_tac. rewrite /worder;split => //; split => //;move=> x xE nex. set X := Vfs f x. rewrite sfr in xE. have XE: sub X (substrate r). rewrite sr -tf;apply: fun_image_Starget1 => //. have sxt: sub x (source f) by rewrite sf. have neX: nonempty X. move: nex => [a ax]; exists (Vf f a); apply /(Vf_image_P ff sxt);ex_tac. move: (wor _ XE neX) => [y []];rewrite iorder_sr //; move => yX ylX. move: yX => /(Vf_image_P ff sxt) [u ux wu]. have pc: sub x (substrate (C f r)) by ue. exists u; red; rewrite iorder_sr //;split => // a ax; apply /iorder_gle0P => //; apply /Zo_P;aw. split; first by apply: setXp_i;fprops. have wx: inc (Vf f a) X by apply /(Vf_image_P ff sxt); ex_tac. by move: (iorder_gle1 (ylX _ wx)); rewrite -wu. have Cp2: forall f r, inc f s3 -> inc r s2 -> order_isomorphism f (C f r) r. move=> f r fs3 rs2; move: (Cp1 _ _ fs3 rs2). move:fs3 rs2 => /Zo_P [] /functionsP [ff sf tf] bf. move => /Zo_P [] /setP_P rc [[or wor] sr] /Zo_P [] rc1 [[or1 wor1] sr1]. split => //; first by split => //; ue. move => x y xsf ysr; split;first by move /Zo_P => [_]; aw. move => pa; apply /Zo_P;aw;split => //; apply: setXp_i => //; ue. have cp3: forall f1 f2 r, inc f1 s3 -> inc f2 s3 -> inc r s2 -> C f1 r = C f2 r -> f1 = f2. move=> f1 f2 r f1s3 f2s3 rs2 sv; move: (Cp2 _ _ f1s3 rs2)(Cp2 _ _ f2s3 rs2). rewrite - sv => p1 p2. move: (order_isomorphism_w p1) (order_isomorphism_w p2) => p3 p4. move: rs2 (Cp1 _ _ f1s3 rs2) => /Zo_P [q1 [q2 q3]] /Zo_P [q4 [q5 q6]]. have sr1: segmentp r (Imf f1). move: p1 => [_ _ [ [_ sj1] _ tf1] _ ]. rewrite (surjective_pr0 sj1) tf1; apply: substrate_segment; fprops. have sr2: segmentp r (Imf f2). move: p2 => [_ _ [ [_ sj1] _ tf1] _ ]. rewrite (surjective_pr0 sj1) tf1; apply: substrate_segment; fprops. exact (isomorphism_worder_unique q5 q2 sr1 sr2 p3 p4). move: (Zermelo E) => [r [wor sr]]. have rs2: inc r s2. apply: Zo_i => //; apply /setP_P;rewrite - sr. apply: sub_graph_coarse_substrate; fprops. have p3: injection (Lf (fun f => C f r) s3 s2). apply: lf_injective => //. by move=> f fe; simpl; apply: Cp1. by move=> u v us3 vs3 su; apply: (cp3 _ _ _ us3 vs3 rs2). by move: (inj_source_smaller p3); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)