Decompose a natural into perfect square

Stream: Is there code for X?

[Pedro Minicz]

Is there some variant of the following in mathlib?

import tactic.linarith

example (n : ℕ) : ∃ N m, n = N^2 + m ∧ m < 2*N + 1 :=
begin
  induction n with n ih,
  { exact ⟨0, 0, rfl, nat.succ_pos _⟩ },
  { rcases ih with ⟨N, m, hn, hm⟩,
    by_cases h : m + 1 < 2*N + 1,
    { exact ⟨N, m.succ, by rw hn, h⟩ },
    { have h : m + 1 = 2*N + 1,
      { by_contra h', exact h (lt_of_le_of_ne hm h') },
      refine ⟨N + 1, 0, _, nat.succ_pos _⟩,
      calc n + 1 = N^2 + m + 1   : by rw hn
      ...        = N^2 + 2*N + 1 : by linarith [h]
      ...        = (N + 1)^2     : by ring } }
end

[Pedro Minicz]

Also, I would like to know if there is a better way of writing this proof/realizing the result (∃ N m, n = N^2 + m ∧ m < 2*N + 1 is fine, but there may be better ways).

[Reid Barton]

There is nat.sqrt already in core, with a good selection of lemmas

[Mario Carneiro]

s/core/mathlib/