proposition: Lemma AQarctan_pos_prf3 {a : AQ} : ¬a ≤ 2 → 1 < a.
proof: Proof. intros. apply orders.lt_le_trans with 2. apply semirings.lt_1_2. now apply orders.le_flip. 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