case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ { val := a, property := ha } < toNonneg b ↔ ↑{ val := a, property := ha } < b
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : { x // 0 ≤ x }
b : α
⊢ a < toNonneg b ↔ ↑a < b
cases' a with a ha
no goals
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ { val := a, property := ha } < toNonneg b ↔ ↑{ val := a, property := ha } < b
simp [toNonneg, ha.not_lt]