proposition: Theorem Qlt_minus_plus_lt_r : ∀ x y z, x < y - z → x + z < y.
proof: Proof. intros x y z H. apply Qplus_lt_compat_r with (z := z) in H. rewrite <- Qplus_minus_swap in H. rewrite <- Qplus_minus_assoc in H. unfold Qminus in H. rewrite Qplus_opp_r, Qplus_0_r in H. assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz