proposition: Lemma EPperm_compat_exists n s: natp n -> n <> \0c -> EPperm_M s n -> exists k, EPperm_compat s n k.
proof: Proof. move => nN np [ /permutationsP [[ins [fs ss]] qc qd] _]. have tor: total_order r1 by move:eta_like_r1 => [[]]. move:bij_f => [[[ff ijf] _] sf tf]. have nsf: inc n (source f) by ue. have aux: forall i, inc i n -> inc (Vf s i) (source f). move => i ii; rewrite sf; apply/(NS_inc_nat nN); Wtac. apply:EPperm_compat0_exists => //. + by Wtac. + move => i /(NltP nN) ii; Wtac. + move => i /(NltP nN) ii eq. move:(cpred_pr nN np) => [sa sb]. move: (ijf (Vf s i) n (aux _ ii) nsf eq) => bad. have /(NltP nN) [_ [//]]: inc (Vf s i) n by Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)