apply Subtype.eq
case mk.mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ } =
    valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ (valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ }).val =
    (valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }).val