Stream: Is there code for X?

Topic: Decompose a natural into perfect square

Pedro Minicz (Jun 23 2020 at 22:54):

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 (Jun 23 2020 at 22:54):

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 (Jun 23 2020 at 23:13):

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

Mario Carneiro (Jun 23 2020 at 23:36):

s/core/mathlib/

Last updated: May 16 2021 at 05:21 UTC