proposition: Lemma EPperm_extend_perm n k s : natp n -> k <=c n -> inc s (permutations n) -> [/\ lf_axiom (EPperm_extend_aux n k s) (csucc n) (csucc n) & inc (EPperm_extend n k s) (permutations (csucc n))].
proof: Proof. move => nN lin /permutationsP [[_ [ff sf]] pc pd]. have nsN := (NS_succ nN). have ax: lf_axiom (EPperm_extend_aux n k s) (csucc n) (csucc n). rewrite/EPperm_extend_aux;move => z za /=; Ytac h1. apply (proj33 (cleS nN)); rewrite - pd; apply:(Vf_target ff); rewrite pc. by move/(NltP nN): (clt_leT h1 lin). case: (equal_or_not z k) => ekz; Ytac0; first by apply: (Nsucc_i nN). apply (proj33 (cleS nN)); rewrite - pd; apply:(Vf_target ff); rewrite pc. case: (equal_or_not z \0c) => zz. case: h1; split => //; rewrite zz; apply: (cle0x (proj31 lin)). have zN:= (NS_inc_nat nsN za). move:(cpred_pr zN zz) => [qa qb]. by apply/(NltP nN) /(cleSltP qa); rewrite - qb; apply/(NleP nN). split=> //. rewrite /EPperm_extend; apply:perm_ints; aw; trivial. apply:(lf_surjective ax); rewrite /EPperm_extend_aux. move => y /(NleP nN) yn; case: (equal_or_not y n). move => ->; exists k; first by apply/(NleP nN). Ytac h;[ by case: (proj2 h) | by Ytac0 ]. move => nyn. have : inc y (target s) by rewrite pd; apply/(NltP nN). move/sf => [z sz ->]; rewrite pc in sz. move/(NltP nN): sz => sz; move: (NS_lt_nat sz nN) => nz. case: (cleT_el (proj31 lin) (CS_nat nz)) => h; last first. exists z; [ apply/(NleP nN); exact: (proj1 sz) | by Ytac0]. move: (cltS nz) => h3; move:(cle_ltT h h3) => [h4 h5]. exists (csucc z); first by apply/(NltP nsN); apply:cltSS. rewrite (Y_false (cleNgt h4)) (Y_false (nesym h5)) cpred_pr2//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)