English
If a is nonnegative in Z√d and n is a natural number, then the product (n)·a is nonnegative.
Русский
Если a неотрицательно в Z√d и n ∈ ℕ, то произведение n·a неотрицательно.
LaTeX
$$$$\forall d, a \in \mathbb{Z}\sqrt{d}, n \in \mathbb{N},\; a \ge 0 \Rightarrow (n \cdot a) \ge 0.$$$$
Lean4
theorem nonneg_smul {a : ℤ√d} {n : ℕ} (ha : Nonneg a) : Nonneg ((n : ℤ√d) * a) :=
by
rw [← Int.cast_natCast n]
exact
match a, nonneg_cases ha, ha with
| _, ⟨x, y, Or.inl rfl⟩, _ => by rw [smul_val]; trivial
| _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ha => by rw [smul_val];
simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)
| _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ha => by rw [smul_val];
simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)
