`BookProof.ChapterF6.mg_lower` (k : ℕ) (s : List α) (y : α) : s.count y ≤ (mg k s) y + mgD k 0 s

Initializing...

`BookProof.ChapterF6.mg_lower` (k : ℕ) (s : List α) (y : α) : s.count y ≤ (mg k s) y + mgD k 0 s · Prove2Me