Theorem: ENat.lt_trans (GMLInit/Data/Nat/Extended/Order.lean)

State before:
x y z : ENat
⊢ x < y → y < z → x < z
Tactic:
intro hxy hyz
State after:
x y z : ENat
hxy : x < y
hyz : y < z
⊢ x < z

State before:
x y z : ENat
hxy : x < y
hyz : y < z
⊢ x < z
Tactic:
exact lt_of_lt_of_le hxy (le_of_lt hyz)
State after:
no goals