proposition: Lemma EPperm_recs n: natp n -> n <> \0c -> (EPperm_rec (csucc n)) = EPperm_extend n (EPperm_next_index n (EPperm_rec n)) (EPperm_rec n).
proof: Proof. move => pa pb. by rewrite /EPperm_rec (induction_terms _ _ pa); Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)