induction h1 with
| zero =>
  intro h
  simp_arith
  assumption
| succSucc x xh ih =>
  intro h
  simp_arith
  constructor
  simp_arith
  apply ih
  assumption
n m : Nat
h1 : Even n
⊢ Even m → Even (n + m)
no goals