proposition: Theorem Qcmp_plus_minus_cmp_r : ∀ x y z, (x ?= y + z) = (x - z ?= y).
proof: Proof. intros x y z. rewrite Qplus_cmp_compat_r with (z := - z). rewrite <- Qplus_assoc. rewrite Qplus_opp_r, Qplus_0_r. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz