English
If a ≠ ⊥ and b ≠ ⊥ in WithBot α, then a*b ≠ ⊥. Non-bottom elements remain non-bottom under multiplication.
Русский
Если a ≠ ⊥ и b ≠ ⊥ в WithBot α, то a*b ≠ ⊥. Элементы не нижнего предела сохраняются при умножении.
LaTeX
$$$ (a \neq \bot) \land (b \neq \bot) \Rightarrow a*b \neq \bot $$$
Lean4
instance [MulZeroClass α] [Preorder α] [MulPosMono α] : MulPosMono (WithBot α) where
elim := by
intro ⟨x, x0⟩ a b h
simp only
rcases eq_or_ne x 0 with rfl | x0'
· simp
lift x to α
· rintro rfl
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0
cases a
· simp_rw [bot_mul x0', bot_le]
cases b
· exact absurd h (bot_lt_coe _).not_ge
simp only [← coe_mul, coe_le_coe] at *
norm_cast at x0
exact mul_le_mul_of_nonneg_right h x0
