intros M N P LTNM LTPN
α : Type u_1
pre : Preorder α
dec : DecidableEq α
⊢ ∀ (M N P : Multiset α), MultisetLT N M → MultisetLT P N → MultisetLT P M
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
LTNM : MultisetLT N M
LTPN : MultisetLT P N
⊢ MultisetLT P M