proposition: Lemma mderivm_is_linear m : linear (mderivm m).
proof: Proof. move=> c p q; rewrite /mderivm; elim: (enum _)=> //= i s ih. by elim: (m i) => //= {ih}k ->; rewrite mderivD mderivZ. 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