proposition: Lemma iter_bind {M : monad} (T : UU0) n (f : T -> M T) (m1 : M unit) m2 : iter n (fun (m : M T) => m >>= f) (m1 >> m2) = m1 >> iter n (fun (m : M T) => m >>= f) m2.
proof: Proof. by elim: n m2 => // n IH m2; rewrite iterS IH !bindA. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy