Theorem: AnalysisI.Ch2.one_plus_m (Lean4Analysis/Ch2.lean)

State before:
m : ℕ
⊢ 1 + m ≃ step m
Tactic:
calc
  _ ≃ 1 + m        := Rel.refl
  _ ≃ step 0 + m   := AA.substL Rel.refl
  _ ≃ step (0 + m) := Natural.step_add
  _ ≃ step m       := AA.subst₁ Natural.zero_add
State after:
no goals