Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_compat_natural (Lean4Axiomatic/Integer/Impl/Difference/Addition.lean)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n + m)——0 ≃ n——0 + m——0
Tactic:
show (n + m)——0 ≃ (n + m)——(0 + 0)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n + m)——0 ≃ (n + m)——(0 + 0)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n + m)——0 ≃ (n + m)——(0 + 0)
Tactic:
show (n + m) + (0 + 0) ≃ (n + m) + 0
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n + m + (0 + 0) ≃ n + m + 0

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n + m + (0 + 0) ≃ n + m + 0
Tactic:
exact AA.substR AA.identR
State after:
no goals