proposition: Lemma rdrop_add T m n (l : loc (ml_rlist T)) : rdrop (m+n) l = rdrop m l >>= rdrop n.
proof: Proof. elim: m l => /= [|m IH] l; first by rewrite bindretf. by rewrite bindA; apply eq_bind => l'. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib