proposition: Lemma tick_fusion n : rep n tick = get >>= (put \o addn n).
proof: Proof. elim: n => [|n ih]; first by rewrite /= -getputskip. rewrite /= /tick ih. rewrite bindA. bind_ext => m. rewrite -bindA. rewrite putget. rewrite bindA. rewrite bindretf. rewrite putput. by rewrite /= addSnnS. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib