feat(data/nat/basic): add lemmas about `nat.bit_cases_on` (#14481)
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).







leanprover-community/mathlib,leanprover-community/mathlib