Naming and golfing competition

Stream: general

[Anne Baanen]

I'm sure there is a better way than this:

lemma nat.foo {a b c : ℕ} (hab : a ≤ b) (hbc : b < a + (c - a)) : b < c :=
begin
  have : a < a + (c - a) := lt_of_le_of_lt hab hbc,
  have : 0 < c - a := (lt_add_iff_pos_right a).mp this,
  have : a ≤ c := le_of_lt (nat.lt_of_sub_pos this),
  rwa nat.add_sub_cancel' this at hbc,
end

[Yakov Pechersky]

(deleted)

[Alex J. Best]

by omega?