Theory Multiset_Order_Extra

theory Multiset_Order_Extra
  imports "HOL-Library.Multiset_Order"
begin

lemma strict_subset_implies_multp⇩H⇩O: "A ⊂# B ⟹ multp⇩H⇩O r A B"
  unfolding multp⇩H⇩O_def
  by (simp add: leD mset_subset_eq_count)

end