proposition: Lemma sorted_cat_cons (x : T) (ys zs : seq T) : sorted (ys ++ x :: zs) = [&& sorted ys, sorted zs, all (<= x) ys & all (>= x) zs].
proof: Proof. apply/idP/idP => [|]. elim: ys => /= [|h t ih]; first by rewrite le_path_sortedE andbC. rewrite !le_path_sortedE all_cat. by move=> /andP[/andP[-> /= /andP[-> _]] hs]; move: (ih hs) => ->. case/and4P => ss ss' ps ps'; apply (@sorted_cat _) => // /=. by rewrite le_path_sortedE ss' ps'. move => a ain b bin; apply: le_trans. - by move: ps => /allP; apply. - by move: bin ps'; rewrite inE => /orP[/eqP ->//|] => /allP; apply. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)