proposition: Lemma Qplus_injective_l (z: Q): forall x y, (x + z == y + z <-> x == y)%Q.
proof: Proof. Proof with intuition. split; intro E. setoid_replace x with (x + z - z)%Q by (simpl; ring). setoid_replace y with (y + z - z)%Q by (simpl; ring). rewrite E... rewrite E... 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