cases a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
a b : valType
⊢ valAdd a b = valAdd b a
case mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
b : valType
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝, property := property✝ } b = valAdd b { val := val✝, property := property✝ }