proposition: Lemma EPperm_next_indexP n s (k:= EPperm_next_index n s): natp n -> n <> \0c -> EPperm_M s n -> (EPperm_compat s n k).
proof: Proof. move => nN nz pe. suff [ //]: ((EPperm_compat s n k) /\ (inc k Nat)). rewrite /k / EPperm_next_index; Ytac0. apply: select_pr. move:(EPperm_compat_exists nN nz pe) => [j ja]. exists j => //;move: ja => [ja _ _ _]; apply: (NS_le_nat ja nN). move => j1 j2 _ ja _ jb; exact:(EPperm_compat_uniq nN pe ja jb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)