File size: 80 Bytes
1b6fcc6
 
 
 
1
2
3
4
5
import Mathlib

theorem nat_add_zero_identity (n : ℕ) : n + 0 = n := by
  rfl