proposition: Theorem Ropp_lt_mono : forall n m : R, n < m <-> - m < - n.
proof: Proof. intros n m. split; intro H. - apply -> (@Rplus_lt_mono_l n m (- n - m)) in H. setoid_replace (- n - m + n) with (- m) in H by ring. now setoid_replace (- n - m + m) with (- n) in H by ring. - apply -> (@Rplus_lt_mono_l (- m) (- n) (n + m)) in H. setoid_replace (n + m + - m) with n in H by ring. now setoid_replace (n + m + - n) with m in H by ring. Qed.
imports: Setoid Ring