have : step (n + k') ≃ step m' := calc
  step (n + k') ≃ _ := Rel.symm add_step
  n + step k'   ≃ _ := ‹n + step k' ≃ step m'›
  step m'       ≃ _ := Rel.refl
n m' k' : Nat
h✝ : n + step k' ≃ step m'
⊢ n ≤ step m'
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this : step (n + k') ≃ step m'
⊢ n ≤ step m'