proposition: Lemma splits_guard (A : UU0) (s : seq A) : splits s = splits s >>= (fun x => guard (size x.1 + size x.2 == size s) >> Ret x) :> M _.
proof: Proof. elim: s => [|h t ih]; first by rewrite bindretf addn0 eqxx guardT bindskipf. rewrite /= {1}ih !bindA; bind_ext => -[a b] /=. by rewrite alt_bindDl !bindretf /= bindA bindretf alt_bindDr addSn addnS eqSS. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)