proposition: Lemma Exercice6_5i E: infinite_set E -> (derangements E) =c (\Po E).
proof: Proof. move=> isE. set s:= (permutations E). apply: cleA; first by apply: Exercise6_5d. set F := E \times C3. have pa: F =c E. apply: cprod_inf3 => //; first by exists C2; rewrite /C3; fprops. apply cle_fin_inf => //; last by apply /infinite_setP. apply: setU1_finite; apply: set2_finite. rewrite -(Exercice6_5f pa). pose fa z := (Yo (z = C0) C1 (Yo (z = C1) C2 C0)). pose fb z := (Yo (z = C0) C2 (Yo (z = C1) C0 C1)). pose fc H z := (J (P z) (Yo (inc (P z) H) (fa (Q z)) (fb (Q z)))). pose f H := Lf(fc H) F F. suff injf: injection (Lf f (\Po E) (derangements F)). by move:(inj_source_smaller injf); aw. have t1: inc C0 C3 by apply /setU1_P; left; fprops. have t2: inc C1 C3 by apply /setU1_P; left; fprops. have t3: inc C2 C3 by apply /setU1_P; right; fprops. move:C2_ne_C01 C1_ne_C0 C0_ne_C1 => [tpne4 tpne7] tpne5 tpne6. have tpne3: C1 <> C2 by apply : nesym. have tpne8: C0 <> C2 by apply:nesym. have pb: forall v, sub v E -> lf_axiom (fc v) F F. move => v vE z /setX_P [za zb zc]; apply: setXp_i => //. rewrite /fa/fb; Ytac p1; Ytac p2; fprops; Ytac p3; fprops. have pc: forall t, inc t E -> inc (J t C0) F by move => t tE;apply /setXp_i. apply: lf_injective. move => u /setP_P uE; move: (pb _ uE) => ax1; rewrite /f. have t3d: forall x, inc x C3 -> x <> C0 -> x <> C1 -> x = C2. by move => x /setU1_P [] // /set2_P; case. have bfu: bijection (f u). have fc3: forall y, inc y F -> fc u (fc u (fc u y)) = y. move => y /setX_P [p1 p2 p3]; rewrite - {2} p1. rewrite /fc !pr1_pair !pr2_pair; apply: f_equal; Ytac pu; Ytac0; Ytac0; rewrite /fa/fb; case: (equal_or_not (Q y) C0) => p4; Ytac0; try (Ytac0; Ytac0; Ytac0; Ytac0 => //); case: (equal_or_not (Q y) C1) => p5; Ytac0; try (Ytac0; Ytac0; Ytac0; Ytac0 => //); symmetry; apply: t3d => //. apply: lf_bijective => //. by move => x y xF yF h; rewrite - (fc3 _ xF) - (fc3 _ yF) h. move => y yF; exists (fc u (fc u y)). by apply: (ax1); apply: ax1. by symmetry;apply: fc3. apply: Zo_i. by apply: Zo_i => //;apply /functionsP; red;saw; fct_tac. move => x xF; rewrite /fc/fa/fb LfV// => eq1; move: (f_equal Q eq1); aw. Ytac p1; Ytac p2; rewrite ? p2; fprops;Ytac p3; rewrite ? p3; fprops. move => u v /setP_P uE /setP_P vE sf. move: (pb _ uE)(pb _ vE) => ax1 ax2. set_extens t => tu. move: (pc _ (uE _ tu)) => pF. move: (f_equal (fun z => (Q (Vf z(J t C0)))) sf); rewrite /f/fc ! LfV//; aw. Ytac0; Ytac tv => //; rewrite /fa/fb; Ytac0; Ytac0; Ytac0; Ytac0 => //. move: (pc _ (vE _ tu)) => pF. move: (f_equal (fun z => (Q (Vf z (J t C0)))) sf); rewrite /f/fc !LfV//; aw. by Ytac0; Ytac tv => //; rewrite /fa/fb; Ytac0; Ytac0; Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)