Zulip Chat Archive

Stream: Is there code for X?

Topic: Decompose a natural into perfect square


view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Reid Barton (Jun 23 2020 at 23:13):

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

view this post on Zulip Mario Carneiro (Jun 23 2020 at 23:36):

s/core/mathlib/


Last updated: May 16 2021 at 05:21 UTC