proposition: Lemma Qplus_lt_r (x y: Q) : x < y -> forall z, z + x < z + y.
proof: Proof. intros E z. do 2 rewrite (Qplus_comm z). apply Qplus_lt_l. assumption. 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