proposition: Lemma EPperm_extend_M n s k: natp n -> n <> \0c -> EPperm_M s n -> (EPperm_compat s n k) -> EPperm_M (EPperm_extend n k s) (csucc n).
proof: Proof. move => nN nz [pe pf] [ph pg1 pg2 pg3]. have [ax pi]:=(EPperm_extend_perm nN ph pe). split => // i j ij jn. have snN:= NS_succ nN. have jN: inc j (csucc n) by apply /(NltP snN). have iN: inc i (csucc n) by apply /(NltP snN); apply: (clt_ltT ij jn). rewrite /EPperm_extend !LfV//. rewrite /EPperm_extend_aux. have kc:= (proj31 ph). case: (p_or_not_p (j <c k)) => ljk; Ytac0. have ik:= (clt_ltT ij ljk). Ytac0; apply: pf => //; exact:(clt_leT ljk ph). have or: order r1 by move:eta_like_r1 => [[[]]]. case (equal_or_not j k) => ejk; Ytac0. rewrite ejk in ij; Ytac0. case (equal_or_not k \0c) => ekz; first by case: (@clt0 i);rewrite - ekz. have ha: glt r1 (Vf f (Vf s (cpred k))) (Vf f n). case (equal_or_not k n) => ekn. by move: (pg2 ekn ekz); rewrite ekn. exact:(proj1 (pg3 (conj ph ekn) ekz)). have [sa sb]:= (cpred_pr (NS_le_nat ph nN) ekz). case: (equal_or_not i (cpred k)); [ by move -> | move => nin]. have ra: i <c cpred k by split => //; apply/(cltSleP sa); ue. have rb: cpred k <c k by rewrite {2} sb; apply: cltS. exact:(lt_lt_trans or (pf _ _ ra (clt_leT rb ph))). have lkj: k <c j by case: (cleT_ell (proj32_1 ij) kc). case: (equal_or_not j \0c) => jz; first by move: lkj; rewrite jz => /clt0. move /(cltSleP nN): (jn) => jn1. have [sa sb] := (cpred_pr (NS_le_nat jn1 nN) jz). have sc: cpred j <c n by apply/(cleSltP sa); rewrite - sb. have sd: k <=c cpred j by apply /(cltSleP sa); ue. case: (p_or_not_p (i <c k)) => lik; Ytac0; first apply: pf (clt_leT lik sd) sc. case: (equal_or_not i k) => eik; Ytac0. case: (equal_or_not k \0c) => ei0. move:(pg1 ei0) => ha; case: (equal_or_not (cpred j) \0c);[by move -> | move => h]. have h1: \0c <c cpred j by apply: card_ne0_pos; fprops. exact:(lt_lt_trans or ha (pf _ _ h1 sc)). have lin:= cle_ltT sd sc. move:(pg3 lin ei0)=> [_ sv];case (equal_or_not k (cpred j)) =>h; first by ue. exact:(lt_lt_trans or sv (pf _ _ (conj sd h) sc)). case: (equal_or_not i \0c) => iz. by case lik; rewrite iz; apply:(card_ne0_pos kc) => kz; case eik; rewrite kz. have kp1: i <=c (cpred j) by apply /(cltSleP sa); ue. have [se sf] := (cpred_pr (NS_le_nat kp1 sa) iz). have ip2: cpred i <c cpred j by apply/(cleSltP se); ue. exact: (pf _ _ ip2 sc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)