lt_le_trans?

Stream: new members

[Marcus Rossel]

Is there a theorem along the lines of:

theorem lt_le_trans {a b c : ℕ} (lt : a < b) (le : b ≤ c) : a < c

I haven't been able to find one. Thanks :pray:🏻

[Bryan Gin-ge Chen]

docs#lt_of_lt_of_le

[Eric Wieser]

If you've already gone as far as writing out the lemma statement as you have there, try := by library_search to find the lemma

[Damiano Testa]

There is also its companion lt_of_le_of_lt

[Floris van Doorn]

There is also nice projection notation:

theorem lt_le_trans {a b c : ℕ} (lt : a < b) (le : b ≤ c) : a < c := lt.trans_le le