fact: Definition uint2N (n : int) : nat := if Uint63.to_Z n is Zpos pos then Pos.to_nat pos else 0.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63