feat: add BitVec.cons_eliminator

[tobiasgrosser]

This PR introduces two induction principles for bitvectors, based on the concat and cons operations. We show how this principle can be useful to reason about bitvectors by refactoring the population count lemmas as follows:

move cpopNatRec_cons_of_le and cpopNatRec_cons_of_lt earlier in the popcount section (they are the building blocks enabling us to take advantage of the new induction principle)
refactor (and shorten) the following proofs: cpopNatRec_zero_le
So far I could only refactor that one lemma, for the others I could not find a way to benefit particularly from induction, but I will continue to look into it

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-22 10:57:44)
• ✅ Reference manual branch lean-pr-testing-11767 has successfully built against this PR. (2026-01-08 17:22:20) View Log
• 🟡 Reference manual branch lean-pr-testing-11767 build against this PR didn't complete normally. (2026-01-08 17:23:24) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-11767 has successfully built against this PR. (2025-12-22 12:34:38) View Log
• ✅ Mathlib branch lean-pr-testing-11767 has successfully built against this PR. (2026-01-08 18:23:29) View Log

[luisacicolini]

changelog-library