Theorem: mul_geq_zero (Pdl/MultisetOrder.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
⊢ ∀ (M : Multiset α), M ≥ 0
Tactic:
intro M
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
⊢ M ≥ 0

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
⊢ M ≥ 0
Tactic:
simp_all only [Multiset.quot_mk_to_coe'', ge_iff_le, zero_le]
State after:
no goals