proposition: Lemma uint2N_sub_succ m n : ltsb m n -> uint2N (sub n m) = (uint2N (sub n (Uint63.succ m))).+1.
proof: Proof. move/ltsb_sub_neq0 => mn. by rewrite sub_succ_pred uint2N_pred. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63