proposition: Lemma rational_arctan_small_wd : forall (a1 a2 : Q) (p1 : -1 <= a1 <= 1) (p2 : -1 <= a2 <= 1), a1 = a2 → rational_arctan_small p1 = rational_arctan_small p2.
proof: Proof. intros. unfold rational_arctan_small. apply ucFun2_wd. rewrite H. reflexivity. apply AltSeries_wd. 2: reflexivity. intro p. rewrite Str_pth_arctanStream, Str_pth_arctanStream, H. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRexp CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower Coq.QArith.Qabs Coq.QArith.Qround CoRN.model.ordfields.Qordfield CoRN.reals.Q_in_CReals CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.transc.MoreArcTan CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q Coq.Init.Datatypes