proposition: Lemma AQarctan_pos_prf1 {a : AQ} : 0 ≤ a → a ≤ 1 ≪ (-1) → -1 < a < 1.
proof: Proof. split. - apply (orders.lt_le_trans _ 0). 2: exact H5. rewrite <- rings.negate_0. apply (rings.flip_lt_negate 0 1). apply semirings.lt_0_1. - apply orders.le_lt_trans with (1 ≪ (-1)); [easy |]. apply (strictly_order_reflecting (cast AQ Q)). rewrite aq_shift_opp_1, rings.preserves_1. split; easy. 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