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