proposition: Lemma ltsbNlesb m n : ltsb m n = ~~ lesb n m.
proof: Proof. case/boolP: (lesb n m) => /Sint63.lebP nm; apply/Sint63.ltbP => /=; by [apply Z.le_ngt | apply Z.nle_gt]. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63