proposition: Lemma uint63_max n : (Uint63.to_Z n < Uint63.wB)%Z.
proof: Proof. by case: (Uint63.to_Z_bounded n). Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63