English
The lemma expresses a structured addition of two nonnegative elements in Z√d, preserving nonnegativity.
Русский
Лемма о сохранении неотрицательности при сложении двух неотрицательных элементов в Z√d.
LaTeX
$$Nonneg(a) ∧ Nonneg(b) ⇒ (a + b).Nonneg$$
Lean4
theorem add {a b : ℤ√d} (ha : Nonneg a) (hb : Nonneg b) : Nonneg (a + b) :=
by
rcases nonneg_cases ha with ⟨x, y, rfl | rfl | rfl⟩ <;> rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩
· trivial
· refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 hb)
· dsimp only at h
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro y (by simp [add_comm, *])))
· apply Nat.le_add_left
· refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 hb)
· dsimp only at h
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro x (by simp [add_comm, *])))
· apply Nat.le_add_left
· refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 ha)
· dsimp only at h
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro w (by simp [*])))
· apply Nat.le_add_right
· have : Nonneg ⟨_, _⟩ := nonnegg_pos_neg.2 (sqLe_add (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))
rw [Nat.cast_add, Nat.cast_add, neg_add] at this
rwa [add_def]
· exact nonneg_add_lem ha hb
· refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 ha)
· dsimp only at h
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro _ h))
· apply Nat.le_add_right
· dsimp
rw [add_comm, add_comm (y : ℤ)]
exact nonneg_add_lem hb ha
· have : Nonneg ⟨_, _⟩ := nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
rw [Nat.cast_add, Nat.cast_add, neg_add] at this
rwa [add_def]
