Theorem: Lean4Axiomatic.Natural.add_one_step (Lean4Axiomatic/Natural/Addition.lean)

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ n + 1 ≃ step n
Tactic:
calc
  n + 1        ≃ _ := AA.substR Literals.literal_step
  n + step 0   ≃ _ := add_step
  step (n + 0) ≃ _ := AA.subst₁ add_zero
  step n       ≃ _ := Rel.refl
State after:
no goals