proposition: Lemma EPperm_next_unique2 n s l (k:= EPperm_next_index n s): natp n -> n <> \0c -> EPperm_M s n -> EPperm_compat s n l -> l = k.
proof: Proof. move => nN nz sm h. exact: (EPperm_compat_uniq nN sm h (EPperm_next_indexP nN nz sm)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)