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