proposition: Lemma ZtoAQ_pos : forall (z:Z), 0 < z -> 0 < ('z : AQ).
proof: Proof. intros z zpos. pose proof (rings.preserves_0 (f:=cast Z AQ)). rewrite <- H5. exact (strictly_order_preserving (cast Z AQ) 0 z zpos). 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