feat(data/nat/lattice): add ```Inf_add``` lemma (#10008)
Adds a lemma about Inf on natural numbers. It will be needed for the count PR.
Co-authored-by: Vladimir Goryachev <64909175+SymmetryUnbroken@users.noreply.github.com>
Co-authored-by: YaelDillies <yael.dillies@gmail.com>
