Zulip Chat Archive

Stream: general

Topic: Naming and golfing competition


view this post on Zulip Anne Baanen (Oct 22 2020 at 13:59):

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

view this post on Zulip Yakov Pechersky (Oct 22 2020 at 14:02):

(deleted)

view this post on Zulip Alex J. Best (Oct 22 2020 at 14:11):

by omega?


Last updated: May 11 2021 at 00:31 UTC