English
If a is nonnegative in Z√d, then sqrtd · a is nonnegative.
Русский
Если a неотрицательно в Z√d, то sqrtd · a неотрицательно.
LaTeX
$$$$\forall d, a \in \mathbb{Z}\sqrt{d},\; a \ge 0 \Rightarrow (\sqrt{d} \cdot a) \ge 0.$$$$
Lean4
theorem nonneg_muld {a : ℤ√d} (ha : Nonneg a) : Nonneg (sqrtd * a) :=
match a, nonneg_cases ha, ha with
| _, ⟨_, _, Or.inl rfl⟩, _ => trivial
| _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ha => by
simp only [muld_val, mul_neg]
apply nonnegg_neg_pos.2
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)
| _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ha => by
simp only [muld_val]
apply nonnegg_pos_neg.2
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)
