In our code we use non byte numbers(deranged and arbitrary int crates), symmetric signed, ordered floats, new num type pattern, our const and categorical num traits(num-traits crate sucks), static assertions, prop tests, easy cast crate(sound as). We have custom decimals. And newtypes of u64 * u64 = u128.
Looking into lean4 provers integrated into rust).
Can your crate compose somewhat with above?