proposition: Lemma Exercice6_5e E F h: bijection h -> source h = E -> target h = F -> (forall f, inc f (derangements F) -> inc ((inverse_fun h) \co (f \co h)) (derangements E)).
proof: Proof. move=> bh sh tg f /Zo_P [/Zo_P [/functionsP [ff sf tf] bf] nfx]. set g := _ \co _. have co: f \coP h by split => //; [fct_tac | ue]. have b1: bijection (f \co h) by apply: compose_fb. move: (inverse_bij_fb bh) => ihb. have co1: (inverse_fun h) \coP (f \co h). split => //; try fct_tac; aw; ue. have bg: bijection g by apply: compose_fb. apply: Zo_i. by apply: Zo_i => //; apply /functionsP;split => //;try fct_tac;rewrite /g;aw. rewrite - sh /g;move => x xE; rewrite ! compfV//; last by aw. set y:= (Vf f (Vf h x)) => eq1. have pe: inc (Vf h x) (source f) by rewrite sf -tg; Wtac; fct_tac. have pd: inc y (target h) by rewrite /y tg -tf; Wtac. rewrite sf in pe; move: (nfx _ pe); rewrite -/y. by move: (inverse_V bh pd);rewrite eq1; move => ->; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)