d x y z w : ℕ
xy : Nonneg { re := ↑x, im := -↑y }
zw : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := subNatNat x z, im := subNatNat w y }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w })
d x y z w : ℕ
xy : Nonneg { re := ↑x, im := -↑y }
zw : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w })
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.2 (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)
d x y z w : ℕ
xy : Nonneg { re := ↑x, im := -↑y }
zw : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := subNatNat x z, im := subNatNat w y }
⊢ Nonneg { re := ↑x + -↑z, im := ↑w - ↑y }
d x y z w : ℕ
xy : Nonneg { re := ↑x, im := -↑y }
zw : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := subNatNat x z, im := subNatNat w y }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w })
rw [add_def, neg_add_eq_sub]
no goals
d x y z w : ℕ
xy : Nonneg { re := ↑x, im := -↑y }
zw : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := subNatNat x z, im := subNatNat w y }
⊢ Nonneg { re := ↑x + -↑z, im := ↑w - ↑y }
rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this
no goals
d x y z w : ℕ
xy✝ : Nonneg { re := ↑x, im := -↑y }
zw✝ : Nonneg { re := -↑z, im := ↑w }
j k m n : ℕ
xy : SqLe (n + m + 1) d k 1
zw : SqLe (k + j + 1) 1 n d
t : 1 * (k + j + 1) * (k + j + 1) ≤ 1 * k * k := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
⊢ (k + j + 1) * (k + j + 1) ≤ k * k
simpa [one_mul] using t