proposition: Lemma Exercice6_5g E: singletonp E \/ nonempty (derangements E).
proof: Proof. have re: forall F, F =c E -> nonempty (derangements F) -> nonempty (derangements E). move => F /Exercice6_5f h /card_nonempty1. rewrite h => h1. case:(emptyset_dichot (derangements E)) => // h2. by case h1; rewrite h2 cardinal_set0. case: (finite_or_infinite (CS_cardinal E)) => ie; last first. move /infinite_setP: (ie) => iE; right. pose f z := J (P z) (variant C0 C1 C0 (Q z)). pose f':= Lf f (E \times C2)(E \times C2). have h: (E \times C2) =c E. apply: cprod_inf3 => //; first by exists C0; fprops. by apply: cle_fin_inf => //; apply: set2_finite. apply: (re _ h); exists f'. have pa: lf_axiom f (E \times C2) (E \times C2). move => x /setX_P [pa pb pc]; rewrite /f; apply: setXp_i=> //. rewrite /variant; Ytac s; fprops. have pb: forall x, inc x (E \times C2) -> f (f x) = x. move => x /setX_P [qa qb qc]; rewrite /f/variant; aw. case: (equal_or_not (Q x) C0) => aux; Ytac0; Ytac0. by rewrite - aux qa. by case /set2_P: qc => // <-; rewrite qa. have pc: bijection (Lf f (E \times C2) (E \times C2)). apply: lf_bijective => //. by move => u v u1 v1 eq; rewrite -(pb _ u1) -(pb _ v1) eq. by move => y ys; move: (pa _ ys) => xs; ex_tac; rewrite pb. rewrite /f';apply :Zo_i; first apply: Zo_i => //. apply /functionsP; red; saw; fct_tac. rewrite /f; move => x xi; rewrite LfV// => p; move: (f_equal Q p); aw. rewrite /variant; Ytac s; [rewrite s |]; fprops. move/NatP: ie; set n:= cardinal E => nN. case: (equal_or_not n \1c) => no; first by left; apply/ set_of_card_oneP. right. case: (equal_or_not n \0c) => nz. exists (identity E). have ->: E = emptyset by apply: card_nonempty; ue. apply: Zo_i; last by move => x /in_set0. apply: Zo_i; first by apply /functionsP; apply: identity_prop. apply: identity_fb. apply: (re n); first by rewrite /n; aw. move: (cpred_pr nN nz) => [pb pc]. pose f x := Yo (x = cpred n) \0c (csucc x). exists (Lf f n n). have ta: forall i, inc i n -> inc (f i) n. move => m /(NltP nN) mn; apply/(NltP nN);rewrite pc. rewrite /f; Ytac mp; first by apply:succ_positive. by apply/cltSS;split => //; apply/(cltSleP pb); rewrite -pc. have injf: surjection (Lf f n n). apply: lf_surjective => // y /(NltP nN) [yN yy]. case: (equal_or_not y \0c) => yz. exists (cpred n); last by rewrite /f; Ytac0. apply/(NltP nN); rewrite {2} pc; apply: cltS; fprops. move: (cpred_pr (NS_le_nat yN nN) yz) => [pyN ysc]. exists (cpred y); rewrite /f -?ysc. by apply /(NltP nN); rewrite - cleSltP // -ysc. by rewrite Y_false// => ss; case:yy;rewrite ysc pc ss. apply: Zo_i;first apply: Zo_i;first by apply /functionsP;saw;fct_tac. apply: bijective_if_same_finite_c_surj; aww. by apply:finite_set_nat. move => x xf; rewrite LfV// /f; Ytac xx. by move => aux; move: pc; rewrite -xx -aux succ_zero. move/NatP:(NS_inc_nat nN xf); case/ finite_cP;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)