proposition: Lemma EPfun_aux_bij : bijection_prop EPfun_aux Nat Nat.
proof: Proof. have pa :=EPfun_aux_M. have [pb pc pd pe hv] := EPfun_aux_pr1. move: (proj1 pb) => gh. move:eta_like_r1 => [[[or1 tor1] _ ppa ppb ppc] _ ]. move: bij_f => [bf sf tf]; move: (proj1 (proj1 bf)) => ff. have ih: injection EPfun_aux. split => // i j; rewrite pc => iN jN sv. have ra: inc (Vf f i) (substrate r1) by Wtac. have rb: inc (Vf f j) (substrate r1) by Wtac. case: (equal_or_not (Vf f i) (Vf f j)) => sv2. move: (proj2 (proj1 bf));rewrite sf => h; exact:(h _ _ iN jN sv2). case: (tor1 _ _ ra rb) => rc. by move/(pa i j iN jN): (conj rc sv2) => [_]; rewrite sv. by move/(pa j i jN iN): (conj rc (nesym sv2)) => [_]; rewrite sv. have bh: bijection EPfun_aux by split. split => //; apply: extensionality => //. set E := Nat -s target EPfun_aux. case: (emptyset_dichot E); [ by move/empty_setC | move => nE]. have EN: sub E Nat by apply: sub_setC. move:(inf_Nat EN nE); set x := intersection E. move => [/setC_P [xN xi]] ha. have hu: forall i, i <c x-> inc i (target EPfun_aux). move => i lix; ex_middle bad. have ie: inc i E by apply/setC_P; split => //; apply: (NS_lt_nat lix xN). case: (cltNge lix (ha _ ie)). clear ha;case: xi; move: x xN hu; clear E nE EN. move => n nN Hrec. case (equal_or_not n \0c) => nz. rewrite nz - pe;Wtac; rewrite pc; exact NS0. set hi := Vf (inverse_fun EPfun_aux). have bih:= (inverse_bij_fb bh). have fih:= (proj1 (proj1 bih)). have tih: target (inverse_fun EPfun_aux) = Nat by rewrite /inverse_fun; aw. have sih: source (inverse_fun EPfun_aux) = target EPfun_aux by rewrite /inverse_fun; aw. have hr1: forall i, i<c n -> natp (hi i) /\ Vf EPfun_aux (hi i) = i. move => i lin; move:(Hrec _ lin) => ra. split; [by rewrite /natp/hi; Wtac| exact: (inverse_V bh ra) ]. set F := fun_image n hi. have fsF: finite_set F by apply:finite_fun_image; apply: finite_set_nat. have fN: sub F Nat. move => t /funI_P [z /(NltP nN) zz ->]. by rewrite - tih /hi; Wtac; rewrite sih; apply: Hrec. have nef: nonempty F. exists \0c; apply/funI_P; exists \0c. apply/(NltP nN); split; first apply:cle0x; fprops. rewrite - {2} pe /hi inverse_V2 // pc; apply: NS0. move:(finite_subset_Nat fN fsF nef) => [m' /fN m'N H0]. set m := csucc m'. have mN: natp m by apply: NS_succ. have mz:m <> \0c by apply: succ_nz. have mm: m' <c m by apply: cltS. have cpm: cpred m = m' by apply: cpred_pr2. have zm: \0c <c m by apply: succ_positive. have mm1: inc m' m by apply/(NltP mN). case: (p_or_not_p (exists i, i<c m /\ Vf EPfun_aux i = n)). move => [i [ im <-]];Wtac;rewrite pc; apply:(NS_lt_nat im mN). move => h. have H: forall i, i <c m -> Vf EPfun_aux i <> n. by move => i im eq; case h; exists i. have H1: forall i, natp i -> Vf EPfun_aux i <c n -> i <c m. move => i iN ha;apply /(cltSleP m'N);apply: H0. apply /funI_P; exists (Vf EPfun_aux i);first by apply /(NltP nN). by rewrite /hi inverse_V2 // pc. clear F fsF fN nef H0 h. move:(EPfun_aux_pr2 mN). rewrite /EPpermi_prop; set hr := restriction1 _ _. move => [fhr shr thr hrm]. move: (EPperm_recs_mon mN); set s := EPperm_rec m => sprop. move: (sprop) => [sa sb]. move /permutationsP: (sa) => [bs sc ts]; move:(proj1 (proj1 bs)) => fs. pose h i := Vf g (Vf EPfun_aux (Vf s i)). have [or2 tor2]:total_order r2 by move: (eta_like_r2) =>[[]]. move: bij_g => [bg sg tg]; move: (proj1 (proj1 bg)) => fg. have [k0 k0p]: exists k, EPperm_compat0 r2 h m k (Vf g n). have nsg:inc n (source g) by rewrite sg. have ra w: w <c m -> inc (Vf s w) m by move => /(NltP mN) wi;Wtac. have rc w: w <c m -> inc (Vf EPfun_aux (Vf s w)) (source g). move => / ra / NS_inc_nat wa; rewrite sg; apply: pd; Wtac. by rewrite pc;apply: wa. apply:EPperm_compat0_exists => //. + rewrite - tg; Wtac; rewrite sg. + move => w / rc wa; rewrite /h; Wtac. move => w wm p; move:(proj2 (proj1 bg) _ _ (rc _ wm) nsg p). by apply: H; apply/(NltP mN); apply: ra. have k0m: k0 <=c m by move: k0p => []. have k0N:= (NS_le_nat k0m mN). pose f1 i := (Vf f (Vf s i)). have qa: forall i, i <c m -> inc (f1 i) (substrate r1). move => i /(NltP mN) im;rewrite /f1; Wtac; rewrite sf; apply: (NS_inc_nat mN); Wtac. have cpE: exists2 i, inc i Nat & EPperm_compat0 r1 f1 m k0 (Vf f i). by apply: EPpermi_compat0_exists. set E := Zo Nat (fun i => EPperm_compat0 r1 f1 m k0 (Vf f i)). have nE: nonempty E by move:cpE => [i ia ib]; exists i; apply: Zo_i. have EN: sub E Nat by move => t /Zo_S. move: (inf_Nat EN nE); set k1 := intersection E. move => [/Zo_P [k1N k1p] Ht]. have: forall k, natp k -> EPperm_compat0 r1 f1 m k0 (Vf f k) -> k1 <=c k. by move => k ka kb; apply: Ht; apply: Zo_i. clear Ht; move: k1 k1N k1p; clear E cpE nE EN => k1 k1N k1p k2p. case: (NleT_el mN k1N)=> lk1m; last first. have Hf1: forall i j, i <c m -> j <c m -> glt r1 (f1 i) (f1 j) -> i <c j. move => i j im jm gt. case (cleT_ell (proj31_1 im) (proj31_1 jm)) => // ha. by case: (proj2 gt); rewrite ha. move: (sb _ _ ha im) => hb; order_tac. move/(NltP mN):lk1m; rewrite - ts => / (proj2 (proj2 bs)) [ i ia ib]. have lim: i <c m by apply /(NltP mN); rewrite - sc. move: k1p;rewrite /EPperm_compat0 ib -/(f1 i); move => [_ ua ub uc]. case: (equal_or_not k0 \0c) => kz. case:(clt0 (Hf1 _ _ lim zm (ua kz))). case (equal_or_not k0 m) => ekm. move:(ub ekm kz); rewrite cpm => ha. by move: (Hf1 _ _ mm lim ha) => /(cleSltP m'N) /(cltNge lim). move:(conj k0m ekm) => lkm; move:(uc lkm kz) => [pa1 pb1]. have kim :=(Hf1 _ _ lim lkm pb1). have [q1 q2] := (cpred_pr k0N kz). have lpkm: cpred k0 <c m by apply/(cleSltP q1); rewrite - q2. by move: (Hf1 _ _ lpkm lim pa1) =>/(cleSltP q1); rewrite - q2=> /(cltNge kim). suff: (Vf EPfun_aux k1) = n by move <-; Wtac. pose r i := exists k, EPperm_2pos i k1 k n. have rm: r m by exists k0; split. have rec: (forall i, m <=c i -> i <c k1 -> r i -> r (csucc i)). move => i lmi lik1 [k hk]. have iN := (NS_lt_nat lik1 k1N). have inz:= (nesym (proj2 (clt_leT zm lmi))). case: (equal_or_not (EPperm_next_index i (EPperm_rec i)) k) => k1i. move:(EPperm_next_indexP iN inz (EPperm_recs_mon iN)). rewrite k1i => pra. by move: hk => [[_ tt] _]; move: (tt _ iN pra) =>/(cltNge lik1). move:(@ EPpermi_extension2 i k k1 n iN inz k1i hk). by set k2 := Yo _ _ _ => hn; exists k2. move:(Nat_induction3 mN k1N rm rec lk1m (cleR (proj32 lk1m))). move => [k3 [[q1 q2] q3]]. have k1pos:= (clt_leT zm lk1m). have k1nz:= (nesym (proj2 k1pos)). have k0k1:= cleT k0m lk1m. have k3v: k3 = (EPperm_next_index k1 (EPperm_rec k1)). move: (EPperm_next_indexP k1N k1nz (EPperm_recs_mon k1N)). set k4 := (EPperm_next_index k1 (EPperm_rec k1)) => praa. exact:(EPperm_compat_uniq k1N (EPperm_recs_mon k1N) q1 praa). have H1':(forall i, natp i -> Vf EPfun_aux i <c n -> i <c k1). by move => i iN lin; move:(clt_leT (H1 _ iN lin) lk1m). clear sprop sa sb bs sc ts fs s h k0p f1 qa k1p k2p. clear m mN mz mm cpm zm mm1 H H1 hr fhr shr thr hrm k0m lk1m r rm rec. clear k0 k0N k0k1. have fh:= (proj1 pb). set s:= EPperm_rec k1. pose f1 i := Vf f (Vf s i). pose h i := Vf g (Vf EPfun_aux (Vf s i)). move: (EPperm_recs_mon k1N) => [sa sb]; rewrite -/s in sa sb. move /permutationsP: sa => [bs sc ts]; move:(proj1 (proj1 bs)) => fs. have hsr: (forall i, i <c k1 -> inc (h i) (substrate r2)). move => i /(NltP k1N) im;rewrite /h; Wtac; rewrite sg; apply: pd; Wtac. rewrite pc; apply: (NS_inc_nat k1N); Wtac. have h_M: forall i j, i <c j -> j <c k1 -> glt r2 (h i) (h j). move => i j lij ljm. have its: inc i (source s). by rewrite sc; apply/(NltP k1N); exact: (clt_ltT lij ljm). have jts: inc j (source s) by rewrite sc; apply/(NltP k1N). have fiN: inc (Vf s i) Nat by apply: (NS_inc_nat k1N); Wtac. have fjN: inc (Vf s j) Nat by apply: (NS_inc_nat k1N); Wtac. by apply/(pa _ _ fiN fjN); apply: sb. have hM1: forall i j, i<c k1 -> j <c k1 -> glt r2 (h i) (h j) -> i <c j. move => i j lim ljm [lt1 lt2]. case: (cleT_ell (proj31_1 lim)(proj31_1 ljm)) => // cp. by case: lt2; rewrite cp. move:(h_M _ _ cp lim) => hh; order_tac. move:(q3) => [k3m _ _ _]. have ->: Vf EPfun_aux k1 = EPpermi_fct h k1 k3. rewrite k3v (hv _ k1N) /EPpermi_next; Ytac0; apply:EPpermi_exten => //. move => i /(NltP k1N) lim;rewrite restriction1_V //. by rewrite pc; apply:(NS_inc_nat k1N). rewrite -/s; Wtac. move: (@EPpermi_pr h k1 k3 h_M hsr k1N k3m k1nz). set k := (EPpermi_fct h k1 k3); move => [h1 h2 h3]. ex_middle nk2n. have lkn: k<c n by exact:(conj (h3 _ nN q3) nk2n). move:(hr1 _ lkn) => []; set i := (hi k) => [iN iv]. have: i <c k1 by apply: H1' => //; rewrite iv. move/(NltP k1N);rewrite -ts; move /(proj2 (proj2 bs)) =>[j js jv]. have ljm: j <c k1 by apply / (NltP k1N); rewrite - sc. move: h2 => [_]; rewrite - iv jv -/(h j) => ta tb tc. case: (equal_or_not k3 \0c) =>k0z. by case: (clt0 (hM1 _ _ ljm k1pos (ta k0z))). have mm:cpred k1 <c k1 by apply: cpred_lt. have [pmN pmv]:= (cpred_pr k1N k1nz). case: (equal_or_not k3 k1) => ekm. move: (hM1 _ _ mm ljm (tb ekm k0z)) => /(cleSltP pmN). by rewrite - pmv => /(cltNge ljm). have lkm:=(conj k3m ekm). have [td te] :=(tc lkm k0z). have jk0 :=(hM1 _ _ ljm lkm te). have [ka kb]:=(cpred_pr (NS_le_nat k3m k1N) k0z). have ckm : (cpred k3) <c k1. apply: cle_ltT _ lkm; rewrite {2} kb; exact(cleS ka). move /(cleSltP ka): (hM1 _ _ ckm ljm td). by rewrite - kb; move/(cltNge jk0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)