proposition: Theorem Qeq_plus_minus_eq_r : ∀ x y z, x == y + z → x - z == y.
proof: Proof. intros. apply Qeq_alt in H; apply Qeq_alt. rewrite <- H; symmetry; apply Qcmp_plus_minus_cmp_r. Qed.
imports: Utf8 QArith NPeano Sorted Psatz