proposition: Lemma mul_coeffE p q k : mul_coeff p q k = \big[C.add u/C.zero]_(0 <= i < k.+1) C.mul u (nth p i) (nth q (k - i)).
proof: Proof. rewrite BigOp.bigopE /reducebig /mul_coeff foldl_rev. by congr foldr; rewrite /index_iota subn0. Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec