Solving arbitrary polynomial equations

Stream: new members

[z battleman]

This is quite a noobish question, but I'm trying to formalize some old homework problems, and one of them is $n^2 +(n+1)^2 = (n+2)^2 \implies n=3$. Trying to formalize it, I wrote it as:

theorem one_a (n : ℕ) : (n^2 + (n+1)^2 = (n+2)^2 → n = 3) :=
  begin
    intro h,
  end

but I don't know how to work with arbitrary polynomials like this. Any advice would be really appreciated!

[Johan Commelin]

@z battleman Here's a proof:

theorem one_a (n : ℕ) : (n^2 + (n+1)^2 = (n+2)^2 → n = 3) :=
begin
  intro h,
  zify at h ⊢,
  rw ← sub_eq_zero at h,
  have : ((n:ℤ) - 3) * (n + 1) = 0,
  { rw ← h, ring_exp, },
  rw [mul_eq_zero, sub_eq_zero] at this,
  apply this.resolve_right,
  rw [add_eq_zero_iff_eq_neg],
  apply int.no_confusion,
end

[z battleman]

oh, thanks so much!