proposition: Lemma Qplus_inj_r (x y z: Q): x + z == y + z <-> x == y.
proof: Proof. split; intro E. - rewrite <- (Qplus_0_r x), <- (Qplus_0_r y). rewrite <- (Qplus_opp_r z); auto. do 2 rewrite Qplus_assoc. rewrite E. reflexivity. - rewrite E. reflexivity. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool