chore(data/finsupp/basic): more lemmas about `α →₀ ℕ` (#5362)
* define `canonically_ordered_add_monoid` instance;
* add a few simp lemmas;
* more lemmas about product over `finsupp.antidiagonal n`;
* define `finsupp.Iic_finset`, use it for `finite_le_nat`.
