proposition: Lemma sub_correct u pi qi p q : pi >:: p -> qi >:: q -> sub u pi qi >:: PolR.sub tt p q.
proof: Proof. move=> Hp Hq k; rewrite /PolR.sub /sub /nth /PolR.nth. apply (@map2_correct R I.type) =>//. - exact: J.zero_correct. - by move=> v /J.contains_only_0 ->; rewrite Ropp_0; apply: J.zero_correct. - by move=> t ?; rewrite -Ropp_0; apply: J.neg_correct. - move=> *; exact: J.neg_correct. - exact: J.contains_only_0. - by move=> ? ? ? H1 /J.contains_only_0 ->; rewrite Rminus_0_r. - by move=> ? ? ? /J.contains_only_0 -> H2; rewrite Rminus_0_l; apply: J.neg_correct. - by move=> v1 ? ? ? ?; rewrite -(Rminus_0_r v1); apply: J.sub_correct. - by move=> v2 ? ? ? ?; rewrite -(Rminus_0_l v2); apply: J.sub_correct. - by move=> *; apply: J.sub_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