feat: add hard theorems from Isabelle

[bollu]

This file contains bitvector theorems that stress Isabelle automation. We port the file to Lean for comparison.

[bollu]

turns out the statement of mask_split_left (resp. mask_split_right) was stronger than necessary, and the theorem isn't about masks at all. For sanity, we prove variants where the symbols are treated as uninterpreted.

[bollu]

@shigoel all comments resolved.

[shigoel]

@bollu Shall we close this PR?

[bollu]

Yep, closing.