proposition: Lemma AQarctan_mid_prf (a : AQ) : 0 < a → -(a+1) < a-1 < a+1.
proof: Proof. split. - rewrite rings.negate_plus_distr. apply (strictly_order_preserving (+ _)). now apply rings.between_pos. - apply (strictly_order_preserving (_ +)). apply rings.between_pos. apply semirings.lt_0_1. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.MetricMorphisms CoRN.reals.fast.CRarctan_small CoRN.reals.fast.CRarctan CoRN.reals.fast.CRpi_fast CoRN.reals.faster.ARpi CoRN.reals.faster.ARarctan_small CoRN.reals.faster.ARArith