proposition: Theorem Rle_le_minus : forall n m : R, n <= m <-> 0 <= m - n.
proof: Proof. intros n m. rewrite (@Rplus_le_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