lt add

Stream: Is there code for X?

[Marcus Rossel]

Does anything exist for this?:

example (i n m : nat) (h : i < n + m) : i < n := sorry

[Yaël Dillies]

Why would this be true? 1 < 1 + 1 but we don't have 1 < 1.

[Marcus Rossel]

Oh right :big_smile::face_palm:

[Anne Baanen]

I was thinking about the converse. Which I think is neatest as assume h : i < n, show i < n + m, from h.trans_le (nat.le_add_right n m) for what it's worth.

[Yaël Dillies]

docs#le_add_left