strictly between squares --> not a square?

Stream: Is there code for X?

[Michael Stoll]

Do we have something like this?

lemma not_sq_of_between_squares (a b : ℤ) (h₁ : b ^ 2 < a) (h₂ : a < (b + 1) ^ 2) : ¬ is_square a := sorry

[Yaël Dillies]

We do, but it's stated for monotone functions

[Yaël Dillies]

... with the caveat that in the specific case of ^2 and \Z, you don't actually need the function to be monotone

[Yaël Dillies]

The correct generality is docs#succ_order, but we don't yet have it there

[Yaël Dillies]

... with the caveat that in the specific case of ^2 and \Z, you don't actually need the function to be monotone

[Floris van Doorn]

specifically, docs#monotone.ne_of_lt_of_lt_nat is roughly what you want

[Floris van Doorn]

oh wait, it's on int

[Michael Stoll]

It looks like I still have to distinguish cases according to the sign of b and then I'll have to provide proof that squaring is monotone (which it isn't on int ...).

[Michael Stoll]

Not sure this will give something much shorter than

import tactic
import algebra.parity

lemma not_sq_of_between_squares (a b : ℤ) (h₁ : b ^ 2 < a) (h₂ : a < (b + 1) ^ 2) :
 ¬ is_square a :=
begin
  rintros ⟨s, h⟩,
  rw ← pow_two at h,
  rw h at h₁ h₂,
  have h₁' := abs_lt_abs_of_sq_lt_sq h₁,
  have h₂' := abs_lt_abs_of_sq_lt_sq h₂,
  by_cases hb : 0 ≤ b,
  { rw abs_eq_self.mpr hb at h₁',
    rw abs_eq_self.mpr (int.le_add_one hb) at h₂',
    linarith, },
  { rw abs_eq_neg_self.mpr (le_of_not_le hb) at h₁',
    have hb'' : b + 1 ≤ 0 := lt_of_not_le hb,
    rw abs_eq_neg_self.mpr hb'' at h₂',
    linarith, },
end

[Yaël Dillies]

You can generalize to even functions monotone on Ici 0

[Michael Stoll]

Yes, but I want it for squares and on all of ℤ. :smile:

[Michael Stoll]

The question is rather whether what is in mathlib leads to a simpler proof than doing it directly.

[Yaël Dillies]

My point is that if you generalize, you will notice that we're missing monotone_on.ne_of_lt_of_lt_int which is a valuable addition.