proposition: Lemma shrink_by_three : forall n a, -(3^(S n))%Z <= a <= (3^(S n))%Z -> -(3^n)%Z <= a/3 <= (3^n)%Z.
proof: Proof. intros n a H0. apply AbsSmall_Qabs. apply AbsSmall_Qabs in H0. apply Qmult_lt_0_le_reg_r with (Qabs 3). reflexivity. rewrite <- Qabs_Qmult. unfold Qdiv. rewrite <- Qmult_assoc. setoid_replace (/ 3 * 3) with 1 by reflexivity. rewrite Qmult_1_r. apply (Qle_trans _ _ _ H0). clear H0. change (Qabs 3) with (inject_Z 3). rewrite <- (inject_Z_mult (3^n) 3). rewrite <- Zle_Qle. change (S n) with (1+n)%nat. rewrite (Nat2Z.inj_add 1 n). rewrite ZBinary.Z.pow_add_r, Z.mul_comm. apply Z.le_refl. discriminate. apply (Nat2Z.inj_le 0), Nat.le_0_l. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRexp CoRN.reals.fast.CRpi CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.ordfields.Qordfield Coq.QArith.Qround CoRN.transc.Pi CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.transc.PowerSeries CoRN.transc.SinCos Coq.NArith.Ndigits CoRN.reals.fast.Compress CoRN.reals.fast.PowerBound CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.util.Qdlog Coq(Lia)