Zulip Chat Archive

Stream: mathlib4

Topic: Nat.lt_add_left


Anatole Dedecker (Jan 03 2023 at 10:35):

In [Std/Data/Nat/Lemmas]https://github.com/leanprover/std4/blob/2919713bde15d55e3ea3625a03546531283bcb54/Std/Data/Nat/Lemmas.lean#L74-L75 we have docs4#Nat.lt_add_right but there is no analog of docs#nat.lt_add_left :sweat_smile:
I'm going to add it in Data/Nat/Basic for now, but we probably want this to be in Std too @Mario Carneiro

Mario Carneiro (Jan 03 2023 at 10:38):

I'll do another pass over Data.Nat.{Defs, Basic} later to port everything to std so either way is fine


Last updated: Dec 20 2023 at 11:08 UTC