Commit 2021-10-27 15:13 25718c26
View on Github →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.