proposition: Lemma primitive_correct u ci c pi p : ci >: c -> pi >:: p -> primitive u ci pi >:: PolR.primitive tt c p.
proof: Proof. move=> Hc Hp; rewrite /primitive /PolR.primitive /nth /PolR.nth. apply: polyCons_correct =>//. apply: (mkseq_correct (Rel := fun r i => i >: r)) =>//. - exact: J.zero_correct. - move=> k; rewrite /int_coeff_shift /PolR.int_coeff_shift. apply: J.div_correct =>//. rewrite INR_IZR_INZ. exact: I.fromZ_correct. - move=> k /andP [_k k_]; rewrite /PolR.int_coeff_shift. by rewrite [seq.nth _ _ _](PolR.nth_default _k) /Rdiv Rmult_0_l. - move=> k /andP [_k k_]; rewrite /PolR.int_coeff_shift. by rewrite [seq.nth _ _ _](nth_default_alt Hp _k) /Rdiv Rmult_0_l. 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