English
The bottom-extended structure inherits PosMulMono from α, meaning multiplication by a positive element preserves order: a ≤ b implies a c ≤ b c for c > 0.
Русский
Расширение снизу наследует PosMulMono: если a ≤ b, то a·c ≤ b·c для всех c > 0.
LaTeX
$$$\forall {a,b,c : WithBot α}, a ≤ b \Rightarrow a*c ≤ b*c \text{ for } c>0$$$
Lean4
instance [MulZeroClass α] [Preorder α] [PosMulReflectLT α] : PosMulReflectLT (WithBot α) where
elim := by
intro ⟨x, x0⟩ a b h
simp only at h
rcases eq_or_ne x 0 with rfl | x0'
· simp at h
lift x to α
· rintro rfl
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0
cases b
· rw [mul_bot x0'] at h
exact absurd h bot_le.not_gt
cases a
· exact WithBot.bot_lt_coe _
simp only [← coe_mul, coe_lt_coe] at *
norm_cast at x0
exact lt_of_mul_lt_mul_left h x0
