proposition: Theorem Qminus_eq_eq_plus_r : ∀ x y z, x - y == z → x == z + y.
proof: Proof. intros. rewrite <- H. rewrite <- Qplus_minus_swap, <- Qplus_minus_assoc. rewrite Qminus_diag, Qplus_0_r. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz