proposition: Lemma ltsb_succ : ltsb (N2int n) (Uint63.succ (N2int n)).
proof: Proof. apply/Sint63.ltbP. rewrite Sint63.succ_spec Sint63.cmod_small. by apply/Zle_lt_succ/Z.le_refl. split. apply leZ_addr => //; by case: (Sint63.to_Z_bounded (N2int n)). apply Z.lt_add_lt_sub_r; by rewrite -Sint63.is_int. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63