/-- Nat arithmetic benchmark: adding zero on the left is identity. -/
theorem pilot_zero_add_left (n : Nat) : 0 + n = n := by
{{PROOF}}