English
If a and b are nonnegative, then their sum a + b is nonnegative.
Русский
Если две величины неотрицательны, то их сумма неотрицательна.
LaTeX
$$Nonneg(a) ∧ Nonneg(b) ⇒ Nonneg(a + b)$$
Lean4
theorem nonneg_add_lem {x y z w : ℕ} (xy : Nonneg (⟨x, -y⟩ : ℤ√d)) (zw : Nonneg (⟨-z, w⟩ : ℤ√d)) :
Nonneg (⟨x, -y⟩ + ⟨-z, w⟩ : ℤ√d) :=
by
have : Nonneg ⟨Int.subNatNat x z, Int.subNatNat w y⟩ :=
Int.subNatNat_elim x z (fun m n i => SqLe y d m 1 → SqLe n 1 w d → Nonneg ⟨i, Int.subNatNat w y⟩)
(fun j k =>
Int.subNatNat_elim w y (fun m n i => SqLe n d (k + j) 1 → SqLe k 1 m d → Nonneg ⟨Int.ofNat j, i⟩)
(fun _ _ _ _ => trivial) fun m n xy zw => sqLe_cancel zw xy)
(fun j k =>
Int.subNatNat_elim w y (fun m n i => SqLe n d k 1 → SqLe (k + j + 1) 1 m d → Nonneg ⟨-[j+1], i⟩)
(fun m n xy zw => sqLe_cancel xy zw) fun m n xy zw =>
let t := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
have : k + j + 1 ≤ k := Nat.mul_self_le_mul_self_iff.1 (by simpa [one_mul] using t)
absurd this (not_le_of_gt <| Nat.succ_le_succ <| Nat.le_add_right _ _))
(nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw)
rw [add_def, neg_add_eq_sub]
rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this
