proposition: Lemma mderiv_is_linear i : linear (mderiv i).
proof: Proof. move=> c p q; pose_big_enough j; first rewrite !(mderivwE j) //. rewrite scaler_sumr -big_split /=; apply/eq_bigr=> k _. rewrite !scalerA -scalerDl; congr (_ *: _). by rewrite mcoeffD mcoeffZ mulrDr !mulrA commr_nat. by close. 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