proposition: Lemma Qbound_le_ZExp2_spec : forall (q : Q), (q <= 2^(Qbound_le_ZExp2 q))%Q.
proof: Proof. intros q. destruct q as [num den]; unfold Qbound_le_ZExp2, Qnum; destruct num. - intros contra; inversion contra. - rewrite Qpower_minus by lra. apply Qle_shift_div_l. + apply Qpower_0_lt; lra. + do 2 rewrite Qpower_decomp_pos, Pos_pow_1_r. unfold Qle, Qmult, Qnum, Qden. rewrite Pos.mul_1_r, Z.mul_1_r. pose proof Pos_log2ceil_plus1_spec p as Hnom. pose proof Pos_log2floor_plus1_spec den as Hden. apply (Zmult_le_reg_r _ _ 2). * lia. * replace (Z.pos p * 2 ^ Z.pos (Pos_log2floor_plus1 den) * 2)%Z with ((Z.pos p * 2) * 2 ^ Z.pos (Pos_log2floor_plus1 den))%Z by ring. replace (2 ^ Z.pos (Pos_log2ceil_plus1 p) * Z.pos den * 2)%Z with (2 ^ Z.pos (Pos_log2ceil_plus1 p) * (Z.pos den * 2))%Z by ring. apply Z.mul_le_mono_nonneg; lia. - intros contra; inversion contra. Qed.
imports: QArith Qpower Qabs Qround Lia Lqa PosExtra