proposition: Lemma Qminus_antitone : forall a : Q, Qantitone (fun x => a - x).
proof: Proof. change (forall a x y : Q, x <= y -> a + - y <= a + - x). intros. apply Qplus_le_compat; firstorder using Qle_refl, Qopp_le_compat. Qed.
imports: Coq.QArith.QArith_base CoRN.order.TotalOrder