proposition: Lemma nth_mul' u p q k : nth (mul u p q) k = \big[Rplus/0%R]_(0 <= i < k.+1) Rmult (nth p i) (nth q (k - i)).
proof: Proof. rewrite nth_mul mul_coeffE; case: leqP => [H|//]. rewrite mul_coeff_eq0 //. move/addn_pred_leqI in H. by move=> i Hi; case: (H i Hi); move/nth_default=>->; intuition. 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