theorem Multiset.replicate_lt_replicate {α : Type u_1} (a : α) {k n : ℕ} : replicate k a < replicate n a ↔ k < n