proposition: Lemma Qminus_eq (x y: Q): (x - y == 0 <-> x == y)%Q.
proof: Proof. rewrite <- (Qplus_injective_l (-y) x y). rewrite Qplus_opp_r. reflexivity. 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