proposition: Lemma ltsb_neq m n : ltsb m n -> m <> n.
proof: Proof. by move/Sint63.ltbP/[swap]/(f_equal Sint63.to_Z)-> =>/Z.lt_irrefl. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63