English
If SqLe y d x c and SqLe (x + z) c (y + w) d, then SqLe z c w d.
Русский
Если SqLe y d x c и SqLe (x+z) c (y+w) d, тогда SqLe z c w d.
LaTeX
$$$\mathrm{SqLe}(y,d,x,c) \rightarrow \mathrm{SqLe}(x+z,c,y+w,d) \rightarrow \mathrm{SqLe}(z,c,w,d)$$$
Lean4
theorem sqLe_cancel {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 :=
by
apply le_of_not_gt
intro l
refine not_le_of_gt ?_ h
simp only [mul_add, mul_comm, mul_left_comm, add_assoc]
have hm := sqLe_add_mixed zw (le_of_lt l)
simp only [SqLe, mul_assoc] at l zw
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)) _)
