calc
  step n ≤ _ := lt_step_le.mp ‹n < m›
  m      ≤ _ := le_from_lt lt_step
  step m ≤ _ := lt_step_le.mp ‹m < k›
  k      ≤ _ := Rel.refl
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ step n ≤ k
no goals