proposition: Lemma Qbound_lt_ZExp2_spec : forall (q : Q), (q < 2^(Qbound_lt_ZExp2 q))%Q.
proof: Proof. intros q. destruct q as [num den]; unfold Qbound_lt_ZExp2, Qnum; destruct num. - reflexivity. - change (Z.pos_sub (Pos.succ (Pos_log2floor_plus1 p)) (Pos_log2floor_plus1 (Qden (Z.pos p # den))))%Z with ((Z.pos (Pos.succ (Pos_log2floor_plus1 p)) - Z.pos (Pos_log2floor_plus1 (Qden (Z.pos p # den)))))%Z. rewrite Qpower_minus by lra. apply Qlt_shift_div_l. + apply Qpower_0_lt; lra. + do 2 rewrite Qpower_decomp_pos, Pos_pow_1_r. unfold Qlt, Qmult, Qnum, Qden. rewrite Pos.mul_1_r, Z.mul_1_r. pose proof Pos_log2floor_plus1_spec p as Hnom. pose proof Pos_log2floor_plus1_spec den as Hden. apply (Zmult_lt_reg_r _ _ 2). * lia. * rewrite Pos2Z.inj_succ, <- Z.add_1_r. rewrite Z.pow_add_r by lia. replace (Z.pos p * 2 ^ Z.pos (Pos_log2floor_plus1 den) * 2)%Z with (2 ^ Z.pos (Pos_log2floor_plus1 den) * (Z.pos p * 2))%Z by ring. replace (2 ^ Z.pos (Pos_log2floor_plus1 p) * 2 ^ 1 * Z.pos den * 2)%Z with ((Z.pos den * 2) * (2 * 2 ^ Z.pos (Pos_log2floor_plus1 p)))%Z by ring. apply Zmult_lt_compat2; lia. - cbn. assert (Z.neg p # den < 0) as Hnegfrac by (unfold Qlt, Qnum, Qden; lia). lra. Qed.
imports: QArith Qpower Qabs Qround Lia Lqa PosExtra