proposition: Lemma iteri_bind {M : monad} n (f : nat -> M unit) (m1 m2 : M unit) : iteri n (fun i (m : M unit) => m >> f i) (m1 >> m2) = m1 >> iteri n (fun i (m : M unit) => m >> f i) m2.
proof: Proof. by elim: n m2 => // n IH m2; rewrite iteriS IH !bindA. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy