proposition: Lemma ltsb_subr m : m.+1 < n -> ltsb (N2int (n - m.+1)) (N2int n).
proof: Proof. move=> Smn. apply/Sint63.ltbP. have Hm : n - m.+1 < n. rewrite ltn_subLR. by rewrite addSn ltnS leq_addl. by apply ltnW. rewrite /N2int -!Sint63.is_int //. - by apply/inj_lt/ltP. - move/ltP/inj_lt in Hm. by split; apply N2int_bounded, Z.lt_le_incl, (Z.lt_trans _ _ _ Hm). Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63