proposition: Lemma EPpermi_extension2 m k0 k1 n (k2 := EPperm_next_index m (EPperm_rec m)) (k0' := Yo (k0 <c k2) k0 (csucc k0)): natp m -> m <> \0c -> k2 <> k0 -> EPperm_2pos m k1 k0 n -> EPperm_2pos (csucc m) k1 k0' n.
proof: Proof. move => mN mz ne1 [[q1 q2] q3]; hnf. move: (EPperm_next_indexP mN mz (EPperm_recs_mon mN)); rewrite -/k2 => pra. move: pra => [k2m _ _ _ ]. have axs:=proj1 (EPperm_extend_perm mN k2m (proj1 (EPperm_recs_mon mN))). move:(EPperm_recs mN mz). set s := (EPperm_rec m); set s' := (EPperm_rec (csucc m)). rewrite -/k2 => s'v. have wa: forall i, i <=c m -> (Vf s' i) = EPperm_extend_aux m k2 s i. move => i /(NleP mN) lim; rewrite s'v /EPperm_extend LfV//. have lt3: \0c <=c m by apply:cle0n. have lt0: \0c <=c csucc m by exact (proj1 (succ_positive m)). split. have [k0m rb rc rd] := q1. have k0N := NS_le_nat k0m mN. have k0'm: k0' <=c csucc m. move: (cleS mN) => hh; rewrite /k0'; Ytac hw; last by apply:cleSS. exact: (cleT (proj1 hw)(cleT k2m hh)). have lt2: cpred (csucc m) <=c m by rewrite cpred_pr2; fprops. rewrite /EPperm_compat0 (wa _ lt3) (wa _ lt2). case: (equal_or_not k0 \0c) => kz. have wb: \0c <c k2. apply:card_ne0_pos; [ exact: (proj31 k2m)| rewrite - kz; fprops]. rewrite /k0' kz; Ytac0; split. by split => // _; rewrite /EPperm_extend_aux; Ytac0; apply: rb. move => k kn [_ W _ _]; apply: (q2 _ kn); split => // _. by move: (W (erefl \0c)); rewrite /EPperm_extend_aux Y_true. case: (equal_or_not k0' \0c); last move => k0'nz. by rewrite /k0'; Ytac wc => tz; [ case: kz | case:(succ_nz tz) ]. rewrite (cpred_pr2 mN). case: (equal_or_not k0 m) => ekm. have eq1: k0' = csucc m by rewrite /k0' ekm (Y_false (cleNgt k2m)). have hh := cleNgt k2m. have lta: ~(k0 <c m) by case. have ltb: ~(k0' <c csucc m) by case. have ltc: ~ (m = k2) by rewrite - ekm; apply: nesym. rewrite /EPperm_extend_aux; Ytac0; Ytac0. split; first by split => // _ _; move: (rc ekm kz). by move => k kn [_ _ W _]; apply: (q2 _ kn);split => //;move:(W eq1 k0'nz). have lk0m: k0 <c m by split. have lt4: k0' <c csucc m. rewrite /k0'; Ytac wb; first by apply /(cltSleP mN). by apply /cltSS. have lt5 := (proj2 lt4). have k'0N:= NS_le_nat k0'm (NS_succ mN). have [ta tb] :=(cpred_pr k'0N k0'nz). have lt6: k0' <=c m by apply /(cltSleP mN). have lt7:cpred k0' <=c m. by move:(cleS ta);rewrite - tb => h; apply:(cleT h lt6). rewrite (wa _ lt7)(wa _ lt6) /EPperm_extend_aux. have re := (rd lk0m kz). case: (p_or_not_p (k0 <c k2)) => le1. have lt8:= (clt_ltT (cpred_lt k0N kz) le1). move: k0'm lt5; rewrite /k0'; Ytac0; Ytac0; Ytac0. split; [by split | move => k kn [_ _ _ W]; apply: (q2 _ kn)]. split => // _ _; exact:(W (conj k0'm lt5) kz). case: (cleT_ell (proj31 k2m) (proj31 k0m)) => // lk2k0. move:(clt_leT lk2k0 (cleS k0N)) => [/cleNgt lt8 lt9]. move: k0'm lt5; rewrite /k0'. have lt10:=(@succ_nz k0). Ytac0; rewrite (cpred_pr2 k0N); Ytac0; Ytac0; Ytac0; Ytac0. split; [ by split| move => k kn [_ _ _ W]; apply: (q2 _ kn) ]. split => // _ _ ; exact: (W(conj k0'm lt5) lt10). move: q3 => [k0m rb rc rd]. have k0N:= (NS_le_nat k0m mN). hnf; rewrite /k0' (cpred_pr2 mN) (wa _ lt3) (wa _ (cleR (CS_nat mN))). case: (equal_or_not k0 \0c) => kz. have wb: \0c <c k2 by apply:(card_ne0_pos (proj31 k2m));rewrite - kz; fprops. rewrite /k0' kz; Ytac0; split => // _. by rewrite /EPperm_extend_aux; Ytac0; apply: rb. case: (equal_or_not k0' \0c); last move => k0'nz. by rewrite /k0'; Ytac wc => tz; [ case: kz | case:(succ_nz tz) ]. case: (equal_or_not k0 m) => ekm. have hh := cleNgt k2m. have ltb: ~(k0 <c k2) by rewrite ekm. rewrite /EPperm_extend_aux (Y_false ltb) (Y_false hh) - ekm; split. + rewrite ekm; fprops. + by move=> ba;case: (@succ_nz k0). + move => _ _; Ytac0; rewrite ekm; exact: (rc ekm kz). + by case. have res :=(rd (conj k0m ekm) kz). have [ua uv]:=(cpred_pr k0N kz). have lta: cpred k0 <c k0 by move: (cltS ua); rewrite - uv. have cp1: cpred (Yo (k0 <c k2) k0 (csucc k0)) <=c m. Ytac hh; [ exact:(cleT (proj1 lta) k0m)| by rewrite cpred_pr2]. have cp2: (Yo (k0 <c k2) k0 (csucc k0)) <=c m. by Ytac hh => //; apply /(cleSltP k0N). have [ltc ntc] := (cle_ltT k0m (cltS mN)). rewrite (wa _ cp1) (wa _ cp2). case: (p_or_not_p (k0 <c k2)) => le1; Ytac0. have lt4:= (clt_ltT lta le1). by split => // _ _; rewrite /EPperm_extend_aux; Ytac0; Ytac0. have lt4:= (cleSS k0m). have lt5 := (@succ_nz k0). have lt6: csucc k0 <> csucc m. by move /(csucc_inj (proj31 k0m) (proj32 k0m)). case: (cleT_ell (proj31 k2m) (proj31 k0m)) => // k2k0. move: (clt_leT k2k0 (cleS k0N)) => [/cleNgt lt7 lt8]. split => // _ _; rewrite /EPperm_extend_aux (cpred_pr2 k0N). by Ytac0; Ytac0; Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)