proposition: Lemma EPperm_extend_M2 n s (k:= EPperm_next_index n s) (s':= (EPperm_extend n k s)): natp n -> n <> \0c -> EPperm_M s n -> EPperm_M s' (csucc n).
proof: Proof. move => pc pd pe. exact: (EPperm_extend_M pc pd pe (EPperm_next_indexP pc pd pe)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)