proposition: Lemma EPpermi_next_pr1 ph n (k1 := EPpermi_next ph n) (ph1 := extension ph n k1): natp n -> (EPpermi_prop ph n) -> [/\ (Vf ph1 n) = k1, forall i, i <c n -> Vf ph1 i = Vf ph i & (EPpermi_prop ph1 (csucc n))].
proof: Proof. move => nN [fh sh th mh]. have nns: ~(inc n (source ph)) by rewrite sh => /(NltP nN) [_]. have fe := (extension_f k1 fh nns). have Vo := (extension_Vf_out k1 fh nns). have Vi := (extension_Vf_in k1 fh nns). have Vi1: forall i, i <c n -> Vf ph1 i = Vf ph i. by move => i /(NltP nN) lin; apply:Vi; rewrite sh. have sph1: source ph1 = csucc n. by rewrite /ph1 /extension corresp_s sh (succ_of_nat nN). have tph1: sub (target ph1) Nat. rewrite /ph1 /extension; aw => t /setU1_P;case;[by apply: th| move ->]. rewrite /k1 /EPpermi_next; Ytac w; [apply: NS0 | exact: EPpermi_pr0]. set s:= (EPperm_rec n). have pa: EPperm_M s n by apply: EPperm_recs_mon. case: (equal_or_not n \0c) => nz. rewrite nz; split => //. + by rewrite - Vo /ph1 nz. + by move => i /clt0. + split => //; first by rewrite - nz. by move => i j /(cltSleP NS0) /cle0 -> /(cltSleP NS0) /cle0 ->; split => [][_]. have pb:= (EPperm_next_indexP nN nz pa). move:pa => [/permutationsP [bs ss ts] sis]; move: (proj1 (proj1 bs)) => fs. pose h i :=(Vf g (Vf ph (Vf s i))). move: bij_g => [bg sg tg]; move: (proj1 (proj1 bg)) => fg. have pc: forall k, k<c n -> (Vf s k) <c n. by move=> k /(NltP nN) kn; apply /(NltP nN); Wtac. have pe:(forall j, j <c n -> inc (h j) (substrate r2)). move => j /(NltP nN) ljn; rewrite /h - tg; Wtac; rewrite sg; apply: th; Wtac. rewrite sh; Wtac; fct_tac. have pd:(forall i j, i <c j -> j <c n -> glt r2 (h i) (h j)). move => i j lij ljn. apply/(mh _ _ (pc i (clt_ltT lij ljn)) (pc j ljn)); by apply: sis. move: (pb) =>[lk0n _ _ _ ]. move:(EPpermi_pr pd pe nN lk0n nz). set k0:= (EPperm_next_index n s). have <-: k1 = EPpermi_fct h n k0 by rewrite /k1 /EPpermi_next; Ytac0. move => [k1N qb qc]. have [or1 tor1]:total_order r1 by move: (eta_like_r1) =>[[]]. have [or2 tor2]:total_order r2 by move: (eta_like_r2) =>[[]]. move: bij_f => [bf sf tf]; move: (proj1 (proj1 bf)) => ff. have snN:= (NS_succ nN). rewrite -/k0 in pb. have [qb1 qb2 qb3 qb4] := qb. have [pb1 pb2 pb3 pb4] := pb. have qd1:forall j, j <c n -> glt r1 (Vf f n) (Vf f j) -> glt r2 (Vf g k1) (Vf g (Vf ph j)). move => j ljn la. have jts: inc j (target s) by rewrite ts; apply/(NltP nN). move: (proj2(proj2 bs) _ jts) => [i iss iv]; rewrite iv -/(h i). rewrite iv in la. have lin: i<c n by apply/(NltP nN); ue. case: (equal_or_not k0 \0c) => ke0. have ra:= (qb2 ke0). case (equal_or_not i \0c) => iz; first by rewrite iz. have ip: \0c <c i by apply:(card_ne0_pos (proj31_1 lin) iz). by move: (pd \0c i ip lin) => ha; order_tac. have kN :=(NS_le_nat qb1 nN). have [re rf]:= (cpred_pr kN ke0). have nn: cpred k0 <c n by apply/(cleSltP re); ue. case: (equal_or_not k0 n) => ken. move:(qb3 ken ke0) (pb3 ken ke0) => ra rb. have rc:= (lt_lt_trans or1 rb la). rewrite - ken in lin. have lein: i <=c (cpred k0) by apply /(cltSleP re); ue. case: (equal_or_not i (cpred n)) => ltin; first by case: (proj2 rc); ue. rewrite - ken in ltin rc. move:(sis _ _ (conj lein ltin) nn) => rg; order_tac. have [ra rb ] := (qb4 (conj qb1 ken) ke0). have [rc rd]:= (pb4 (conj qb1 ken) ke0). case:(cleT_ell (proj31_1 lin) (proj31 qb1)) => rg. + by rewrite rg. + move:(lt_lt_trans or1 rc la) => rh. have lein: i <=c (cpred k0) by apply /(cltSleP re); ue. case: (equal_or_not i (cpred k0)) => ltin; first by case: (proj2 rh); ue. move: (sis _ _ (conj lein ltin) nn) => ri; order_tac. + by move: (pd _ _ rg lin) => rh; order_tac. have qd2:forall j, j <c n -> glt r1 (Vf f j) (Vf f n) -> glt r2 (Vf g (Vf ph j)) (Vf g k1). move => j ljn la. have jts: inc j (target s) by rewrite ts; apply/(NltP nN). move: (proj2(proj2 bs) _ jts) => [i iss iv]; rewrite iv -/(h i). rewrite iv in la. have lin: i<c n by apply/(NltP nN); ue. case: (equal_or_not k0 \0c) => ke0. have ra := (lt_lt_trans or1 la (pb2 ke0)). case (equal_or_not i \0c) => iz; first by case: (proj2 ra);rewrite iz. have ip: \0c <c i by apply:(card_ne0_pos (proj31_1 lin) iz). move: (sis _ _ ip lin) => rb; order_tac. have kN :=(NS_le_nat qb1 nN). have [re rf] := (cpred_pr kN ke0). have nn: cpred k0 <c n by apply/(cleSltP re); ue. case: (equal_or_not k0 n) => ken. have ra:= (qb3 ken ke0). rewrite ken in re rf nn. have lein: i <=c (cpred n) by apply /(cltSleP re); ue. case: (equal_or_not i (cpred n)) => ltin; first by rewrite ltin. move:(pd _ _ (conj lein ltin) nn) => rg; order_tac. have [ra rb] :=(qb4 (conj qb1 ken) ke0). have [rc rd] := (pb4 (conj qb1 ken) ke0). have rg := (lt_lt_trans or1 la rd). case:(cleT_ell (proj31_1 lin) (proj31 qb1)) => rh. + by case: (proj2 rg); rewrite rh. + have lein: i <=c (cpred k0) by apply /(cltSleP re); ue. case: (equal_or_not i (cpred k0)) => ltin; first by rewrite ltin. move: (pd _ _ (conj lein ltin) nn) => ri; order_tac. + by move: (sis _ _ rh lin) => ri; order_tac. have sra: inc (Vf f n) (substrate r1) by Wtac; ue. have jinv: forall j, j <c n -> (Vf f j) <> (Vf f n). move => j [lejn nejn] eq. have ijs: inc j (source f) by rewrite sf; apply:(NS_le_nat lejn nN). have ins: inc n (source f) by rewrite sf. by move:(proj2 (proj1 bf) _ _ ijs ins eq). have qd3: forall j, j <c n -> ( glt r1 (Vf f n) (Vf f j) <-> glt r2 (Vf g k1) (Vf g (Vf ph j))). move => j ljn; split; [ by apply: qd1 | move => ha]. have ji := (jinv _ ljn). have srb: inc (Vf f j) (substrate r1). Wtac; rewrite sf; apply:(NS_lt_nat ljn nN). case: (tor1 _ _ sra srb) => ra; first by split => //; exact:(nesym ji). move:(qd2 _ ljn (conj ra ji)) => rb; order_tac. have qd4: forall j, j <c n -> ( glt r1 (Vf f j) (Vf f n) <-> glt r2 (Vf g (Vf ph j)) (Vf g k1)). move => j ljn; split; [ by apply: qd2 | move => ha]. have ji := (jinv _ ljn). have srb: inc (Vf f j) (substrate r1). Wtac; rewrite sf; apply:(NS_lt_nat ljn nN). case: (tor1 _ _ sra srb) => ra; last by split => //; exact:(nesym ji). move:(qd1 j ljn (conj ra (nesym ji))) => rb; order_tac. split => //; split => //. move => i j /(cltSleP nN) lin /(cltSleP nN) ljn. case (equal_or_not i n) => ein. rewrite ein Vo. case (equal_or_not j n) => ejn. by rewrite ejn Vo; split; move => [_ ];case. by rewrite (Vi1 _ (conj ljn ejn)); apply: qd3. move: (conj lin ein) => ltin; rewrite (Vi1 _ ltin). case (equal_or_not j n) => ejn; last first. rewrite (Vi1 _ (conj ljn ejn));exact: (mh _ _ ltin (conj ljn ejn)). by rewrite ejn Vo; apply: qd4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)