proposition: Lemma mderiv_perm (s1 s2 : seq 'I_n) p : perm_eq s1 s2 -> foldr mderiv p s1 = foldr mderiv p s2.
proof: Proof. pose M q s := foldr mderiv q s; rewrite -!/(M _ _). have h (s : seq 'I_n) (x : 'I_n) q: x \in s -> M q s = M q (x :: rem x s). + elim: s=> [|y s ih] //; rewrite in_cons /=. by case: eqVneq => [->|ne_xy {}/ih ->] //=; rewrite mderiv_comm. elim: s1 s2 => [|x s1 ih] s2. by rewrite perm_sym=> /perm_small_eq=> ->. move=> peq_xDs1_s2; have x_in_s2: x \in s2. by rewrite -(perm_mem peq_xDs1_s2) mem_head. have /h ->/= := x_in_s2; rewrite -ih // -(perm_cons x). by rewrite (permPl peq_xDs1_s2) perm_to_rem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg