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