proposition: Lemma partial_rotation n f (k := Vf (inverse_fun f) n) (g:= fun i => Yo (i <c k) (Vf f i) (Vf f (csucc i))) (G := Lf g n n): natp n -> inc f (permutations (csucc n)) -> [/\ k <=c n, Vf f k = n, lf_axiom g n n & inc G (permutations n)].
proof: Proof. move => nN /permutationsP H. move: (inverse_bij_bp H) => hh. have nsf: inc n (csucc n) by apply:Nsucc_i. move: H => [bf sf tf]. have IP := (NltP nN). have IP' := (NltP (NS_succ nN)). have ff: function f by fct_tac. have iff:= (proj2 (proj1 bf)). have ntf: inc n (target f) by rewrite tf. move: (inverse_V bf ntf); rewrite -/k => kv. have lekn: k <=c n. move: hh => [[[bg _] _] sg tg]; apply/(NleP nN); rewrite/k; Wtac. have kN:=(NS_le_nat lekn nN). have ksf: inc k (source f) by rewrite sf; apply/IP'; apply/cltSleP. have Gv i: g i = Vf f (Yo (i <c k) i (csucc i)) by rewrite/g; Ytac h; Ytac0. have Gs i: i <c n -> inc (Yo (i <c k) i (csucc i)) (source f). move => lin; rewrite sf; apply /IP'. by Ytac h; [ apply:(clt_ltT lin (cltS nN)) | apply :cltSS]. have axg: lf_axiom g n n. move => i /IP lin;move: (Gs _ lin) => usf;rewrite Gv; apply /IP. split; first by apply/(cltSleP nN); apply/IP'; Wtac. rewrite - kv => /(iff _ _ usf ksf). Ytac h => eq; first by case (proj2 h). by case: h; rewrite - eq; apply:(cltS (NS_lt_nat lin nN)). split => //. apply/permutationsP; rewrite/G;split; aw; trivial. apply: lf_bijective => //. move => u v /IP ui /IP vi. rewrite Gv Gv; move/(iff _ _ (Gs _ ui) (Gs _ vi)); Ytac h1; Ytac h2 => eq. - exact. - case: h2; apply:cle_ltT h1; rewrite eq; exact: (cleS (NS_lt_nat vi nN)). - case: h1; apply:cle_ltT h2; rewrite - eq; exact: (cleS (NS_lt_nat ui nN)). - by apply: (csucc_inj (proj31_1 ui) (proj31_1 vi)). move => y /IP yi; move:(clt_ltT yi (cltS nN)) => yi'. have ytf: inc y (target f) by rewrite tf; apply/IP'. move: (proj2 (proj2 bf) _ ytf) => [x xsf ea]; rewrite ea. move: xsf; rewrite sf => /IP' xsn. have xN:= (NS_lt_nat xsn (NS_succ nN)). case: (NleT_ell kN xN) => cix. + by move:(f_equal (Vf f) cix); rewrite kv -ea; move => eb; case: (proj2 yi). + case (equal_or_not x \0c) => xnz. rewrite xnz in cix;case:(clt0 cix). move: (cpred_pr xN xnz) => [sc sd]. move: xsn; rewrite sd;move/(cltSSP (CS_nat sc) (CS_nat nN)) => /IP ci. exists (cpred x) => //; rewrite - sd /g; Ytac h; last by rewrite - sd. by move/(cleSlt0P (CS_nat sc) kN):h; rewrite - sd => /(cltNge cix). exists x; [ apply /IP; exact:(clt_leT cix lekn) | by rewrite /g; Ytac0]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)