proposition: Lemma Qlowbound_ltabs_ZExp2_inv: forall q : Q, q > 0 -> Qlowbound_ltabs_ZExp2 q = (- Qbound_ltabs_ZExp2 (/q))%Z.
proof: Proof. intros q Hqgt0. destruct q as [n d]. unfold Qlowbound_ltabs_ZExp2, Qbound_ltabs_ZExp2, Qbound_lt_ZExp2, Qnum. destruct n. - inversion Hqgt0. - unfold Qabs, Z.abs, Qinv, Qnum, Qden. rewrite -> Z.pos_sub_opp. do 2 rewrite <- Pos2Z.add_pos_neg. lia. - inversion Hqgt0. Qed.
imports: QArith Qpower Qabs Qround Lia Lqa PosExtra