α : Type u_1
β : Type ?u.96069
γ : Type ?u.96072
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b : α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s
α : Type u_1
β : Type ?u.96069
γ : Type ?u.96072
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b : α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ erase s a
rw [erase_of_not_mem h]
no goals
α : Type u_1
β : Type ?u.96069
γ : Type ?u.96072
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b : α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s
apply le_cons_self