calc
  step n + k'   ≃ _ := step_add
  step (n + k') ≃ _ := Rel.symm add_step
  n + step k'   ≃ _ := AA.substR ‹step k' ≃ k›
  n + k         ≃ _ := Rel.symm ‹m ≃ n + k›
  m             ≃ _ := Rel.refl
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ step n + k' ≃ m
no goals