case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ ¬c * z * z > d * w * w
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ SqLe z c w d
apply le_of_not_gt
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ False
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ ¬c * z * z > d * w * w
intro l
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ c * (x + z) * (x + z) > d * (y + w) * (y + w)
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ False
refine' not_le_of_gt _ h
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ c * (x + z) * (x + z) > d * (y + w) * (y + w)
simp only [SqLe, mul_add, mul_comm, mul_left_comm, add_assoc, gt_iff_lt]
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
hm : d * (y * w) ≤ c * (x * z)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
have hm := sqLe_add_mixed zw (le_of_lt l)
case a
d✝ : ℤ
c d x y z w : ℕ
h : SqLe (x + z) c (y + w) d
hm : d * (y * w) ≤ c * (x * z)
l : d * (w * w) < c * (z * z)
zw : d * (y * y) ≤ c * (x * x)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
hm : d * (y * w) ≤ c * (x * z)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
simp only [SqLe, mul_assoc, gt_iff_lt] at l zw
no goals
case a
d✝ : ℤ
c d x y z w : ℕ
h : SqLe (x + z) c (y + w) d
hm : d * (y * w) ≤ c * (x * z)
l : d * (w * w) < c * (z * z)
zw : d * (y * y) ≤ c * (x * x)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
exact
  lt_of_le_of_lt (add_le_add_right zw _)
    (add_lt_add_left (add_lt_add_of_le_of_lt hm (add_lt_add_of_le_of_lt hm l)) _)