proposition: Lemma ltsb_sub_neq0 m n : ltsb m n -> sub n m <> 0%int63.
proof: Proof. move=> mn. rewrite Sint63.sub_of_Z => /(f_equal Uint63.to_Z). rewrite Uint63.of_Z_spec. move/Sint63.ltbP in mn. rewrite Zmod_small. rewrite Z.sub_move_r /= => nm. rewrite nm in mn. by move/Z.lt_irrefl in mn. by apply /lesb_sub_bounded /Sint63.lebP /Z.lt_le_incl. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63