proposition: Lemma dotmuldiv_correct u a b pi p : seq.size a = seq.size b -> pi >:: p -> dotmuldiv u a b pi >:: PolR.dotmuldiv tt a b p.
proof: Proof. move=> Hs Hp. move=> k; rewrite nth_dotmuldiv PolR.nth_dotmuldiv. do ![case: ifP] => /or3P A /or3P B. - exact: J.zero_correct. - case B. by move/nth_default_alt =>->; rewrite ?Rmult_0_r; try exact: J.zero_correct. by move/or3P in A; move=> K; rewrite K orbT in A. by move/or3P in A; move=> K; rewrite K !orbT in A. - case A=> K. rewrite <- (Rmult_0_r (Rdiv (IZR (seq.nth 0%Z a k)) (IZR (seq.nth 0%Z b k)))). apply J.mul_correct. by apply: J.div_correct; apply: I.fromZ_correct. have->: 0%R = PolR.nth p k. by move/PolR.nth_default: K. exact: Hp. by move/or3P in B; rewrite K !orbT in B. by move/or3P in B; rewrite K !orbT in B. - apply: J.mul_correct =>//. apply: J.div_correct =>//; exact: I.fromZ_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