[STATEMENT]
lemma real_less_sum_gt_zero: "(w < s) \<Longrightarrow> (0 < s + (-w::real))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w < s \<Longrightarrow> 0 < s + - w
[PROOF STEP]
by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of s])