proposition: Lemma Qplus_le_l (z x y : Q): x + z <= y + z <-> x <= y.
proof: Proof. Proof with auto with *. split; intros. setoid_replace x with (x + z + -z) by (simpl; ring). setoid_replace y with (y + z + -z) by (simpl; ring). apply Qplus_le_compat... apply Qplus_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