constructor
case h.h.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y ↔ MultisetLT X Y
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLt X Y → MultisetLT X Y

case h.h.a.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
⊢ MultisetLT X Y → MultisetLt X Y