proposition: Lemma lesb_sub_bounded m n : lesb m n -> (0 <= Sint63.to_Z n - Sint63.to_Z m < Uint63.wB)%Z.
proof: Proof. move/Sint63.lebP => mn. split. by apply Zle_minus_le_0. apply (Z.le_lt_trans _ (Sint63.to_Z Sint63.max_int - Sint63.to_Z Sint63.min_int))%Z. apply leZ_sub. by case: (Sint63.to_Z_bounded n). by case: (Sint63.to_Z_bounded m). done. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63