proposition: Lemma EPperm_recs_mon n: natp n -> EPperm_M (EPperm_rec n) n.
proof: Proof. move:n; apply:Nat_induction. rewrite EPperm_rec0; apply:EPperm_extend_M3. move => n nN Hrec;case: (equal_or_not n \0c) => nz. rewrite nz succ_zero EPperm_rec1; apply :EPperm_extend_M4. by rewrite (EPperm_recs nN nz); apply:EPperm_extend_M2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)