proposition: Lemma ipartlE p i n : ipartl p i 0 0 n = fmap (fun x => (dipartlT1 x, dipartlT2 x)) (dipartl p i 0 0 n).
proof: Proof. rewrite fmapE /dipartl bindA ipartl_guard bindA; bind_ext => -[a b]. rewrite bindA; apply: bind_ext_guard => /andP[na nb]. rewrite bindretf /dassert /=. case: Bool.bool_dec => [nanb|/negP]; first by rewrite bindretf. by rewrite negb_and => /orP[|] /negP. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)