Theorem: Lean4Axiomatic.Natural.trans_lt_eqv_lt (Lean4Axiomatic/Natural/Order.lean)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
⊢ n < m → m ≃ k → n < k
Tactic:
intro (_ : n < m) (_ : m ≃ k)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≃ k
⊢ n < k

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m ≃ k
⊢ n < k
Tactic:
exact lt_eqv_subst ‹m ≃ k› ‹n < m›
State after:
no goals