proposition: Theorem Rlt_lt_minus : forall n m : R, n < m <-> 0 < m - n.
proof: Proof. intros n m. rewrite (@Rplus_lt_mono_r n m (- n)). setoid_replace (n + - n) with 0 by ring. now setoid_replace (m + - n) with (m - n) by ring. Qed.
imports: Setoid Ring