proposition: Lemma ZtoQ : forall n:positive, AQtoQ (ZtoAQ (Zpos n)) == (Zpos n#1).
proof: Proof. induction n. - change (Z.pos n~1) with (1+2*Z.pos n)%Z. pose proof (rings.preserves_plus (f:=cast Z AQ) 1 (2*Z.pos n)). rewrite H5. clear H5. rewrite rings.preserves_plus, rings.preserves_1. rewrite rings.preserves_1. pose proof (rings.preserves_mult (f:=cast Z AQ) 2 (Z.pos n)). rewrite H5. clear H5. rewrite rings.preserves_mult, IHn. rewrite rings.preserves_2, rings.preserves_2. unfold Qeq; simpl. rewrite Pos.mul_1_r. reflexivity. - change (Z.pos n~0) with (2*Z.pos n)%Z. pose proof (rings.preserves_mult (f:=cast Z AQ) 2 (Z.pos n)). rewrite H5. rewrite rings.preserves_mult, IHn. rewrite rings.preserves_2. pose proof (rings.preserves_2 (f:=cast AQ Q)). rewrite H6. reflexivity. - pose proof (rings.preserves_1 (f:=cast Z AQ)). rewrite H5. rewrite rings.preserves_1. reflexivity. Qed.
imports: Coq.QArith.Qround Coq.QArith.Qpower MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.MetricMorphisms CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRsin CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.faster.ARAlternatingSum CoRN.reals.faster.ARArith