proposition: Lemma forloop63S m n (f : int -> M unit) : ltsb m n -> forloop63 m n f = f m >> forloop63 (Uint63.succ m) n f.
proof: Proof. rewrite /forloop63 => mn. rewrite ltsbNlesb (ltsbW _ _ mn) /=. case: ifPn => nSm. by move: mn; rewrite ltsbNlesb => /negP; elim; apply ltsbS_lesb. rewrite ltsbNlesb negbK in nSm. rewrite uint2N_sub_succ //. by rewrite iterSr bindretf !bindA iter_bind !bindA. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63