proposition: Lemma mul_coeff_eq0 p q k : (forall i, i <= k -> nth p i = 0%R \/ nth q (k - i) = 0%R) -> (\big[Rplus/R0]_(0 <= i < k.+1) (nth p i * nth q (k - i)) = 0)%R.
proof: Proof. move=> H. rewrite big_mkord big1 // => [[i Hi]] _ /=. rewrite ltnS in Hi. by case: (H i Hi) =>->; rewrite ?(Rmult_0_l, Rmult_0_r). 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