proposition: Lemma add_correct u pi qi p q : pi >:: p -> qi >:: q -> add u pi qi >:: PolR.add tt p q.
proof: Proof. move=> Hp Hq k; rewrite /PolR.add /add /nth /PolR.nth. apply (@map2_correct R I.type) =>//. - exact: J.zero_correct. - exact: J.contains_only_0. - by move=> ? ? ? H1 /J.contains_only_0 ->; rewrite Rplus_0_r. - by move=> ? ? ? /J.contains_only_0 -> H2; rewrite Rplus_0_l. - by move=> v1 ? ? ? ?; rewrite -(Rplus_0_r v1); apply: J.add_correct. - by move=> v2 ? ? ? ?; rewrite -(Rplus_0_l v2); apply: J.add_correct. - by move=> *; apply: J.add_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