proposition: Lemma Qbound_leabs_ZExp2_spec : forall (q : Q), (Qabs q <= 2^(Qbound_leabs_ZExp2 q))%Q.
proof: Proof. intros q. unfold Qbound_leabs_ZExp2; apply Qabs_case; intros. 1,2: apply Qbound_le_ZExp2_spec. Qed.
imports: QArith Qpower Qabs Qround Lia Lqa PosExtra