lean-standard-prover-qwen3-8b-grpo/example_proof.lean

import Mathlib


theorem demo (n : ℕ) : n + 0 = n := by 
  
  induction n with
  
  | zero => rfl
  
  | succ n ih => simp_all