proposition: Lemma is_partition_consL p x (ys zs : seq T) : is_partition p (x :: ys, zs) = (x <= p) && is_partition p (ys, zs).
proof: Proof. by rewrite /is_partition andbA. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)