proposition: Theorem Rplus_le_mono_l : forall n m p : R, n <= m <-> p + n <= p + m.
proof: Proof. intros n m p; split. - apply (SORplus_le_mono_l sor). - intro H. apply ((SORplus_le_mono_l sor) (p + n) (p + m) (- p)) in H. setoid_replace (- p + (p + n)) with n in H by ring. setoid_replace (- p + (p + m)) with m in H by ring. assumption. Qed.
imports: Setoid Ring