proposition: Lemma power3bound : forall (q:Q), (q <= (3^(Z_of_nat (let (n,_):= q in match n with Zpos p => Psize p | _ => O end)))%Z #1).
proof: Proof. intros [[|n|n] d]; try discriminate. unfold Qle. simpl. Open Scope Z_scope. rewrite Zpos_mult_morphism. apply Zmult_le_compat. 2: apply Pos.le_1_l. 2: discriminate. 2: discriminate. clear - n. apply Z.le_trans with (two_p (Z.succ (Z.log2 (Zpos n)))-1)%Z. - rewrite <- Zle_plus_swap. apply Zlt_succ_le. change (Zpos n+1) with (Z.succ (Zpos n)). apply Zsucc_lt_compat. destruct (Z.log2_spec (Zpos n)); auto with zarith. rewrite two_p_correct. assumption. - replace (Z.succ (Z.log2 (Zpos n))) with (Z_of_nat (Psize n)). + apply Z.le_trans with (two_p (Z_of_nat (Psize n))). auto with *. induction (Psize n); auto with *. rewrite inj_S. simpl. unfold Z.succ. rewrite two_p_is_exp; auto with *. change (two_p 1) with 2. rewrite Zpower_exp. 2: apply Z.le_ge, Zle_0_nat. 2: discriminate. apply Zmult_le_compat. exact IHn0. discriminate. induction (Z_of_nat n0). discriminate. discriminate. discriminate. discriminate. + rewrite <- Psize_Zlog2. induction n as [ p ih | p ih | ]. simpl; rewrite Pos2Z.inj_succ, <- ih; apply Z.P_of_succ_nat_Zplus. simpl; rewrite Pos2Z.inj_succ, <- ih; apply Z.P_of_succ_nat_Zplus. reflexivity. Close Scope Z_scope. 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