English
The predicate Nonnegg(c,d)(a,b) encodes the sign condition a√c + b√d ≥ 0 by a case-split on the signs of a and b.
Русский
Предикат Nonnegg(c,d)(a,b) кодирует условие a√c + b√d ≥ 0 через разбиение по знакам a и b.
LaTeX
$$$\mathrm{Nonnegg}(c,d)(a,b) = \begin{cases} \text{True}, & a \ge 0 \text{ и } b \ge 0; \\ \mathrm{SqLe}((b+1),c,a,d), & a \ge 0, b < 0 \text{ с } b = -(m+1); \\ \mathrm{SqLe}((a+1),d,b,c), & a < 0, b \ge 0; \\ \text{False}, & a < 0, b < 0. \end{cases}$$$
Lean4
/-- "Generalized" `nonneg`. `nonnegg c d x y` means `a √c + b √d ≥ 0`;
we are interested in the case `c = 1` but this is more symmetric -/
def Nonnegg (c d : ℕ) : ℤ → ℤ → Prop
| (a : ℕ), (b : ℕ) => True
| (a : ℕ), -[b+1] => SqLe (b + 1) c a d
| -[a+1], (b : ℕ) => SqLe (a + 1) d b c
| -[_+1], -[_+1] => False
