mathlib3

25718c26 - feat(data/nat/basic): Add two lemmas two nat/basic which are necessary for the count PR (#10001)

feat(data/nat/basic): Add two lemmas two nat/basic which are necessary for the count PR (#10001) Add two lemmas proved by refl to data/nat/basic. They are needed for the count PR, and are changing a file low enogh in the import hierarchy to be a separate PR. Co-authored-by: SymmetryUnbroken <64909175+SymmetryUnbroken@users.noreply.github.com>