proposition: Lemma EPperm_extend_M4: EPperm_M (identity \1c) \1c.
proof: Proof. split; first by apply: permutation_id. move => i j lij lj1; move: (lj1) => [_ nj1]. case:(clt2 (clt_ltT lj1 clt_12)) => // jz. by move: lij; rewrite jz => /clt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)