proposition: Lemma power4bound : forall (q:Q), (q <= inject_Z (4^(Z_of_nat (let (n,_):= q in match n with Zpos p => Psize p | _ => O end)))%Z).
proof: Proof. intros q. eapply Qle_trans. apply power3bound. generalize (let (n, _) := q in match n with | 0 => 0%nat | Zpos p => Psize p | Zneg _ => 0%nat end)%Z. intros n. unfold Qle. simpl. ring_simplify. induction n. apply Z.le_refl. rewrite inj_S. unfold Z.succ. do 2 rewrite Zpower_exp by auto with zarith. ring_simplify. apply Zmult_le_compat. 1, 3: discriminate. assumption. clear -n. induction n. discriminate. rewrite inj_S. unfold Z.succ. rewrite Zpower_exp; auto with *. 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