proposition: Lemma Exercice6_5f E F: E =c F -> (derangements E) =c (derangements F).
proof: Proof. move => /card_eqP [h [pa pb pc]]; symmetry;apply/card_eqP. exists (Lf (fun f => ((inverse_fun h) \co (f \co h))) (derangements F) (derangements E)). move: (inverse_bij_fb pa) => bh'. saw; apply: lf_bijective. by apply: Exercice6_5e. move => u v /Zo_P [] /Zo_P [] /functionsP [p1 p2 p3] _ _. move => /Zo_P [] /Zo_P [] /functionsP [p4 p5 p6] _ _ eq. have q1: u \coP h by split => //; try fct_tac; ue. have q2: v \coP h by split => //; try fct_tac; ue. have q3: function (u \co h) by fct_tac. have q4: function (v \co h) by fct_tac. have q5: inverse_fun h \coP (u \co h) by saw;try fct_tac; ue. have q6: inverse_fun h \coP (v \co h) by saw;try fct_tac; ue. move: (compf_regr bh' q5 q6 eq) => eq1. by move: (compf_regl pa q1 q2 eq1). move => y yE. exists (h \co (y \co (inverse_fun h))). have eq1:inverse_fun (inverse_fun h) = h by apply: ifun_involutive; fct_tac. by rewrite -{1} eq1; apply: (Exercice6_5e bh' _ _ yE); aw. move: yE => /Zo_P [] /Zo_P [] /functionsP [pd pe pf] _ _. have p1: (y \coP inverse_fun h) by saw;try fct_tac; ue. have p2: function (y \co inverse_fun h) by fct_tac. have p3: (h \coP (y \co inverse_fun h)) by saw;try fct_tac; ue. set z := (h \co (y \co inverse_fun h)). have p4: function z by rewrite /z; fct_tac. have p5: inverse_fun h \coP z by rewrite /z;saw;try fct_tac. have p6: z \coP h by rewrite /z;saw;try fct_tac. rewrite (compfA p5 p6) (compfA (composable_inv_f pa) p3)(bij_left_inverse pa). have ->: (source h) = target (y \co inverse_fun h) by aw; rewrite pb pf. rewrite (compf_id_l p2) - (compfA p1 (composable_inv_f pa)). by rewrite (bij_left_inverse pa) pb -pe (compf_id_r pd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)