proposition: Lemma rep_addn m n mx : rep (m + n) mx = rep m mx >> rep n mx.
proof: Proof. elim: m n => [|m IH /=] n; by [rewrite bindskipf add0n | rewrite -addnE IH bindA]. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy