proposition: Lemma rotation_prop n (m := csucc n) (f := Lf (fun i => variant \0c n (cpred i) i) m m) (g := Lf (fun i => variant n \0c (csucc i) i) m m): natp n -> [/\ inc f (permutations m), inc g (permutations m), inverse_fun f = g & [/\ Vf f \0c = n, forall i, i <c n -> Vf f (csucc i) = i, forall i, i <=c n -> i <> \0c -> Vf f i = (cpred i), Vf g n = \0c & forall i, i <c n -> Vf g i = (csucc i) ] ].
proof: Proof. move => nN. move: (NleP nN) => H. have axf: lf_axiom (fun i => variant \0c n (cpred i) i) m m. rewrite /variant => i /H lin; apply/H. Ytac h; first by apply: (cleR (CS_nat nN)). exact: (cleT (cpred_le (proj31 lin)) lin). have axg: lf_axiom (fun i => variant n \0c (csucc i) i) m m. move => i /H lin; apply/H; rewrite /variant; Ytac h; first by apply:cle0n. by apply/(cleSltP (NS_le_nat lin nN)). have i0m: inc \0c m by apply/H; apply:cle0n. have rA: Vf f \0c = n by rewrite /f/variant LfV//; Ytac0. have rB: forall i, i <c n -> Vf f (csucc i) = i. move => i lin. have sin: inc (csucc i) m by apply/H; apply/(cleSltP (NS_lt_nat lin nN)). rewrite/f LfV//. by rewrite (variant_false _ _ (@succ_nz _)) (cpred_pr1 (proj31_1 lin)). have rC: forall i, i <=c n -> i <> \0c -> Vf f i = (cpred i). move => i lin inz. move: (cpred_pr (NS_le_nat lin nN) inz) =>[pN pv]. rewrite {1} pv rB //; apply/(cleSltP pN); ue. have rD: Vf g n = \0c. rewrite/g LfV//? variant_true //; apply/H; apply: (cleR (CS_nat nN)). have rE: forall i, i <c n -> Vf g i = csucc i. by move => i [lin nn]; rewrite/g LfV// ? variant_false//; apply/H. have fg_val i: inc i m -> Vf f (Vf g i) = i. move => /H lin; case: (equal_or_not i n) => inn. by rewrite inn rD rA. by move:(conj lin inn)=> Hi; rewrite (rE _ Hi) (rB _ Hi). have gf_val i: inc i m -> Vf g (Vf f i) = i. move => /H lin; case: (equal_or_not i \0c) => iz. by rewrite iz rA rD. move: (cpred_pr (NS_le_nat lin nN) iz) =>[pN pv]. rewrite (rC _ lin iz) rE- ? pv //; apply/(cleSltP pN); ue. have [ff sf tf]: function_prop f m m. by rewrite/f;saw; apply:lf_function. have [fg sg tg]: function_prop g m m. by rewrite/g;saw; apply:lf_function. have cgfp: g \coP f by split => //; ue. have cfgp: f \coP g by split => //; ue. have cgf: g \co f = identity (source f). apply: identity_prop0; first by saw; [ apply:compf_f| ue ]. move => i isf; rewrite compfV// gf_val //; ue. have cfg: f \co g = identity (source g). apply: identity_prop0; first by saw; [ apply:compf_f| ue ]. move => i isf;rewrite compfV// fg_val //; ue. move:(bijective_from_compose cgfp cfgp cgf cfg) => [bf bg fgi]. split. - by apply/permutationsP. - by apply/permutationsP. - done. - done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)