proposition: Lemma forloop631 m (f : int -> M unit) : forloop63 m m f = f m.
proof: Proof. rewrite /forloop63. case: (Sint63.ltbP m m) => [/Z.lt_irrefl // | _]. rewrite /= bindA. rewrite /uint2N Uint63.sub_spec Z.sub_diag Zmod_0_l /=. by rewrite !(bindretf,bindA) bindmskip. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63