α : Type ?u.188122
m n : ℕ
this : ∀ {n : ℕ}, ofNat' (Nat.succ n) = ofNat' n + 1
⊢ ofNat' (m + n) = ofNat' m + ofNat' n
α : Type ?u.188122
m n : ℕ
⊢ ofNat' (m + n) = ofNat' m + ofNat' n
have : ∀ {n}, ofNat' n.succ = ofNat' n + 1 := ofNat'_succ
no goals
α : Type ?u.188122
m n : ℕ
this : ∀ {n : ℕ}, ofNat' (Nat.succ n) = ofNat' n + 1
⊢ ofNat' (m + n) = ofNat' m + ofNat' n
induction n <;> simp [Nat.add_zero, this, add_zero, Nat.add_succ, add_one, add_succ, *]