basic): add lemmas about `nat.bit_cases_on` (#14481)

Commit

3 years ago

feat(data/nat/basic): add lemmas about `nat.bit_cases_on` (#14481) Also drop `nat.bit_cases` (was the same definition with a different order of arguments).

Author

urkud

Parents

ade30c34

mathlib3 1a1895cd - feat(data/nat/basic): add lemmas about `nat.bit_cases_on` (#14481)

mathlib3
1a1895cd - feat(data/nat/basic): add lemmas about `nat.bit_cases_on` (#14481)