proposition: Lemma Qlowbound_ltabs_ZExp2_spec : forall (q : Q) (Hqgt0 : ~ q == 0), (2^(Qlowbound_ltabs_ZExp2 q) < Qabs q)%Q.
proof: Proof. intros q Hqgt0. destruct (Q_dec 0 q) as [[H|H]|H]. - rewrite Qabs_pos by lra. apply Qlowbound_lt_ZExp2_spec, H. - rewrite Qabs_neg by lra. rewrite Qlowbound_ltabs_ZExp2_opp. apply Qlowbound_lt_ZExp2_spec. lra. - lra. Qed.
imports: QArith Qpower Qabs Qround Lia Lqa PosExtra