proposition: Lemma size_partition p (s : seq T) : size (partition p s).1 + size (partition p s).2 = size s.
proof: Proof. elim: s p => //= x xs ih p; have {ih} := ih p. move H : (partition p xs) => h; case: h H => a b ab /= abxs. by case: ifPn => xp; rewrite !(addSn,addnS) abxs. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)