proposition: Lemma EPpermi_pr h n k (j := EPpermi_fct h n k) (P := fun m => EPperm_compat0 r2 h n k (Vf g m)) : (forall i j, i<c j -> j <c n -> glt r2 (h i) (h j)) -> (forall j, j <c n -> inc (h j) (substrate r2)) -> natp n -> k <=c n -> n <> \0c -> [/\ inc j Nat, P j & forall k, inc k Nat -> P k -> j <=c k].
proof: Proof. move:eta_like_r2 bij_g => [[tor _ pa pb pc] _ ][bg sg tg] iss qa nN lin nz. set E := (Zo Nat (fun j => EPperm_compat0 r2 h n k (Vf g j))). have ha: sub E Nat by apply: Zo_S. have [z za zb]:exists2 j, inc j Nat & EPperm_compat0 r2 h n k (Vf g j). by apply:EPpermi_compat0_exists. have hb: nonempty E by exists z;apply : Zo_i. move: (inf_Nat ha hb) => [/Zo_P [hc hd] he]; split => //m ka kb; apply:he. by apply : Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)