proposition: Lemma lesb_ltsbS_eq m n : lesb m n -> ltsb n (Uint63.succ m) -> m = n.
proof: Proof. move/Sint63.lebP => mn /Sint63.ltbP nSm. move: (nSm). rewrite Sint63.succ_of_Z -Sint63.is_int; last first. split. apply Z.le_le_succ_r. by case: (Sint63.to_Z_bounded m). apply Zlt_le_succ, (Z.le_lt_trans _ _ _ mn), (Z.lt_le_trans _ _ _ nSm). by case: (Sint63.to_Z_bounded (Uint63.succ m)). move/Zlt_le_succ/Zsucc_le_reg => nm. by apply Sint63.to_Z_inj, Zle_antisym. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63