sqLe_add — Mathlib

English

If SqLe x c y d and SqLe z c w d, then SqLe (x + z) c (y + w) d.

Русский

Если SqLe x c y d и SqLe z c w d, то SqLe (x+z) c (y+w) d.

LaTeX

$$$\mathrm{SqLe}(x,c,y,d) \rightarrow \mathrm{SqLe}(z,c,w,d) \rightarrow \mathrm{SqLe}(x+z,c,y+w,d)$$$

Lean4

theorem sqLe_add {c d x y z w : ℕ} (xy : SqLe x c y d) (zw : SqLe z c w d) : SqLe (x + z) c (y + w) d :=
  by
  have xz := sqLe_add_mixed xy zw
  simp only [SqLe, mul_assoc] at xy zw
  simp [SqLe, mul_add, mul_comm, mul_left_comm, add_le_add, *]

Похожие утверждения