proposition: Lemma power4bound' : forall (q:Q), (0 < q) -> ((/inject_Z((4^(Z_of_nat (let (_,d):= q in Psize d)))%Z)) <= q).
proof: Proof. intros [[|n|n] d] H. elim (Qlt_not_eq _ _ H); constructor. 2: elim (Qlt_not_le _ _ H); discriminate. assert (X:=power4bound (Zpos d#n)). simpl in X. rewrite -> Zpower_Qpower by auto with zarith. apply Qle_shift_inv_r. clear - d. induction (Psize d). constructor. rewrite inj_S. unfold Z.succ. rewrite -> Qpower_plus;[|discriminate]. rewrite <- (Qmult_0_r ((4%Z#1) ^ Z.of_nat n)). apply Qmult_lt_l. exact IHn. constructor. rewrite <- Zpower_Qpower by auto with zarith. destruct (inject_Z (Zpos 4%positive ^ Z.of_nat (Psize d))%Z). change ((1 * Zpos (d * Qden)%positive <= Zpos n * Qnum * 1)%Z). ring_simplify. unfold Qle in *. simpl in X. rewrite Zmult_comm. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.NArith.Ndigits Coq.ZArith.ZArith Coq.Program.Basics Coq.QArith.Qpower CoRN.stdlib_omissions.Z