proposition: Lemma deriv_correct u pi p : pi >:: p -> deriv u pi >:: PolR.deriv tt p.
proof: Proof. move=> Hpi; rewrite /deriv /PolR.deriv /deriv_loop /PolR.deriv_loop. apply: (seq_foldri_correct (Rel := fun v t => t >: v)) =>//. - by move=> k; rewrite !nth_behead. - move=> x s i Hx Hs [|k] /=. + by move/J.contains_only_0: Hx->; rewrite Rmult_0_l; apply: J.zero_correct. + by move: (Hs k); rewrite nth_nil. - move=> x s i Hx Hs [|k] /=. rewrite -(Rmult_0_l (INR i)). apply: J.mul_correct =>//; rewrite INR_IZR_INZ; apply: I.fromZ_correct. by move: (Hs k); rewrite nth_nil. - move=> x xi y yi i Hx Hy [|k] //=. by apply: J.mul_correct =>//; rewrite INR_IZR_INZ; apply: 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