proposition: Lemma mul_correct u pi qi p q : pi >:: p -> qi >:: q -> mul u pi qi >:: PolR.mul tt p q.
proof: Proof. move=> Hp Hq; rewrite /mul /PolR.mul /nth /PolR.nth. apply: (mkseq_correct (Rel := fun r i => i >: r)) =>//. - exact: J.zero_correct. - exact: mul_coeff_correct. - move=> k /andP [Hk _]; rewrite PolR.mul_coeffE. rewrite PolR.mul_coeff_eq0 //. move/addn_pred_leqI in Hk. by move=> i Hi; case: (Hk i Hi); move/PolR.nth_default=>->; intuition. - move=> k /andP [Hk _]; rewrite PolR.mul_coeffE /size. rewrite PolR.mul_coeff_eq0 //. move/addn_pred_leqI in Hk. by move=> i Hi; case: (Hk i Hi); move/nth_default_alt=>->; 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