proposition: Lemma ARtoCR_preserves_pi : 'ARpi = CRpi.
proof: Proof. unfold ARpi, CRpi. rewrite ARtoCR_preserves_AQpi. rewrite rings.preserves_1. reflexivity. 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