proposition: Lemma Qlowbound_ltabs_ZExp2_opp: forall q : Q, (Qlowbound_ltabs_ZExp2 q = Qlowbound_ltabs_ZExp2 (-q))%Z.
proof: Proof. intros q. destruct q as [[|n|n] d]; reflexivity. Qed.
imports: QArith Qpower Qabs Qround Lia Lqa PosExtra