proposition: Lemma Qminus_less (x y : Q) : 0 <= y -> x - y <= x.
proof: Proof. intro H. rewrite <- (Qplus_0_r x) at 2. apply Qplus_le_r. change 0 with (-0). now apply Qopp_le_compat. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List