proposition: Lemma forloopS m n (f : nat -> M unit) : m <= n -> forloop m n f = f m >> forloop m.+1 n f.
proof: Proof. rewrite /forloop => mn. rewrite ltnNge mn /= subSS subSn // iteriSr bindskipf. rewrite -[f _]bindmskip iteri_bind addn0 ltnS -subn_eq0. case: (n-m) => //= k. rewrite addSnnS; apply eq_bind => _; congr bind. apply eq_iteri => i x; by rewrite addSnnS. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy