proposition: Lemma Qabs_gt: forall r s : Q, r < s -> r < Qabs s.
proof: Proof. intros r s Hrlts. apply Qabs_case; intros Hs. - exact Hrlts. - pose proof Qlt_le_trans _ _ _ Hrlts Hs as Hr. apply Qopp_le_compat in Hs. exact (Qlt_le_trans _ _ _ Hr Hs). Qed.
imports: QArith Qreduction