English
As in 27604, (a*b).unbotD 0 = a.unbotD 0 * b.unbotD 0 for all a,b ∈ WithBot α; the same compatibility holds identically.
Русский
Как и в 27604, справедливость: (a*b).unbotD 0 = a.unbotD 0 * b.unbotD 0 для всех a,b ∈ WithBot α.
LaTeX
$$$ (a*b).unbotD 0 = a.unbotD 0 * b.unbotD 0 $$$
Lean4
instance [MulZeroClass α] [Preorder α] [PosMulMono α] : PosMulMono (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 [mul_bot 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_left h x0
