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