proposition: Lemma uint63_min n : (0 <= Uint63.to_Z n)%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