α : Type u_1
β : Type ?u.89059
γ : Type ?u.89062
δ : Type ?u.89065
inst✝ : LT α
a✝ b : α
a : WithTop α
⊢ ¬↑WithTop.toDual a < ↑WithTop.toDual none
α : Type u_1
β : Type ?u.89059
γ : Type ?u.89062
δ : Type ?u.89065
inst✝ : LT α
a✝ b : α
a : WithTop α
⊢ ¬none < a
rw [← toDual_lt_toDual_iff]
no goals
α : Type u_1
β : Type ?u.89059
γ : Type ?u.89062
δ : Type ?u.89065
inst✝ : LT α
a✝ b : α
a : WithTop α
⊢ ¬↑WithTop.toDual a < ↑WithTop.toDual none
exact WithBot.not_lt_none _