proposition: Lemma EPpermi_compat0_exists r h n k G : natp n -> n <> \0c -> k <=c n -> eta_like r -> bijection_prop G Nat (substrate r) -> (forall i j, i<c j -> j <c n -> glt r (h i) (h j)) -> (forall j, j <c n -> inc (h j) (substrate r)) -> exists2 i, inc i Nat & EPperm_compat0 r h n k (Vf G i).
proof: Proof. move => nN nz lin [[[or1 tor1] _ pa pb pc] _ ] [bG sG tG] ha hb. have fG: function G by fct_tac. have qb: inc (h \0c) (substrate r). by apply: hb; apply:(card_ne0_pos (CS_nat nN) nz). case: (equal_or_not k \0c) => iz. have [y ya] := (pa _ qb). have : inc y (substrate r) by order_tac. rewrite - tG; move /(proj2 (proj2 bG))=> [jj ja jb]. rewrite iz in lin; rewrite sG in ja. by ex_tac; hnf; rewrite iz; split => //;rewrite - jb. have [sa sb]:= (cpred_pr nN nz). case (equal_or_not k n) => ein. move: (cltS sa); rewrite - sb => /hb /pb [y ya]. have : inc y (substrate r) by order_tac. rewrite - tG; move /(proj2 (proj2 bG))=> [jj ja jb]. rewrite sG in ja; ex_tac; hnf; split => //;[ by rewrite -jb | by move => [_]]. have [sc sd]:= (cpred_pr (NS_le_nat lin nN) iz). move:(cltS sc); rewrite - sd => hc. have [y [ya yb]]:= (pc _ _ (ha _ _ hc (conj lin ein))). have : inc y (substrate r) by order_tac. rewrite - tG; move /(proj2 (proj2 bG))=> [jj ja jb]. by rewrite sG in ja; ex_tac; hnf; split => //; rewrite -jb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)