proposition: Lemma mul_coeff_correct u pi qi p q : pi >:: p -> qi >:: q -> forall k : nat, mul_coeff u pi qi k >: PolR.mul_coeff tt p q k.
proof: Proof. move=> Hpi Hqi k. rewrite mul_coeffE PolR.mul_coeffE. apply (@big_ind2 R I.type (fun r i => i >: r)). - exact: J.zero_correct. - move=> *; exact: J.add_correct. - move=> *; exact: J.mul_correct. 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