proposition: Lemma ltsbS_lesb m n : ltsb m (Uint63.succ n) -> lesb m n.
proof: Proof. rewrite -[lesb _ _]negbK -ltsbNlesb => nSm; apply/negP => /[dup] /ltsbW nm. by rewrite (lesb_ltsbS_eq n m) // => /Sint63.ltbP /Z.lt_irrefl. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63