mathlib

89a80e67 - feat(data/nat/parity): `nat.bit1_div_bit0` (#15268)

feat(data/nat/parity): `nat.bit1_div_bit0` (#15268) This PR adds `nat.bit1_div_bit0` and related lemmas. This came up when working with the power series of sin. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>