Cryptographic systems are actually somewhat of an awkward thing to build with lean actually because many of the things that we assume to be true with them are either straight up not true (like lack of collisions in important hashes) or beyond the capabilities of our current math knowledge.