proposition: Lemma mul_trunc_correct u n pi qi p q : pi >:: p -> qi >:: q -> mul_trunc u n pi qi >:: PolR.mul_trunc tt n p q.
proof: Proof. move=> Hp Hq; rewrite /nth /PolR.nth. apply: (mkseq_correct (Rel := fun r i => i >: r)) =>//. - exact: J.zero_correct. - exact: mul_coeff_correct. - by move=> k; rewrite ltn_leqN. - by move=> k; rewrite ltn_leqN. 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