proposition: Lemma AQarctan_big_prf (a : AQ) : 1 < a → -a < 1 < a.
proof: Proof. split. 2: exact H5. transitivity 0. 2: apply semirings.lt_0_1. rewrite <- rings.negate_0. apply (rings.flip_lt_negate 0 a). transitivity 1. 2: exact H5. 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