proposition: Lemma N2int_bounded n : (Z.of_nat n <= Sint63.to_Z Sint63.max_int)%Z -> (Sint63.to_Z Sint63.min_int <= Z.of_nat n <= Sint63.to_Z Sint63.max_int)%Z.
proof: Proof. split => //. apply (Z.le_trans _ 0). rewrite -[0%Z]/(Sint63.to_Z 0). by case: (Sint63.to_Z_bounded 0). by apply Zle_0_nat. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63