proposition: Lemma AQpi_prf (x : Z) : 1 < x → -('x : AQ) < 1 < ('x : AQ).
proof: Proof. split. 2: apply semirings.preserves_gt_1, H5. rewrite <- (rings.preserves_1 (f:=cast Z AQ)). rewrite <- (rings.preserves_negate (f:=cast Z AQ)). apply (strictly_order_preserving (cast Z AQ)). unfold one, stdlib_binary_integers.Z_1. rewrite <- (Z.opp_involutive 1). apply Z.gt_lt, CornBasics.Zlt_opp. apply (Z.lt_trans _ 1). reflexivity. exact H5. Qed.
imports: MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRpi_fast CoRN.reals.fast.CRarctan_small CoRN.reals.faster.ARarctan_small