Functions for bitwise operations/machine integer manip

Stream: new members

[O Bel]

Hello, I'm a lean begginer and I'm trying to use lean4 for formal verification of simple functions.
I'm working on bitwise operations and modular computation (on machine integers) proofs; and I was wondering what were the most appropriate functions/parts of mathlib4, and if there was material/example out there on such use of lean4.
I'm trying to model machine integers with ZMod, I'm trying proofs with Int.land/lor etc. for bitwise operations that I've found parsing the mathlib4 documentation. But these might not be the right functions for building the best proofs, and I haven't found much theorems.
Thank you!