is this something `nlinarith` should be able to do?

Stream: new members

[Chris M]

import data.real.basic
import tactic

open function

theorem aux {x y : ℝ} (h : x^2 + y^2 = 0) : x = 0 :=
begin
  have h' : x^2 = 0,
  { nlinarith },
  exact pow_eq_zero h'
end

example (x y : ℝ) : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 :=
begin
    split,
    { intros, split, {
        apply aux a},{
        rw add_comm at a, apply aux a}},{
      intros, cases a,
nlinarith
    }
end

This doesn't work, because nlinarith gives an error, it doesn't work if I replace it with norm_num either, and only works when I replace it with

have h:x^2=0, {exact tactic.ring_exp.pow_p_pf_zero a_left rfl},
      have h2:y^2=0, {exact tactic.ring_exp.pow_p_pf_zero a_right rfl},
      finish

I'm curious: is this something that we would want nlinarith or norm_num to know about or am I misunderstanding what they should be able to do?

[Mario Carneiro]

I don't think linarith does case splits