proposition: Lemma iqsort_cons i (n : nat) : iqsort (i, n.+1) = aget i >>= (fun p => dipartl p i.+1 0 0 n >>= (fun nynz => let ny := dipartlT1 nynz in let nz := dipartlT2 nynz in aswap i (i + ny) >> iqsort (i, ny) >> iqsort (i + ny.+1, nz))).
proof: Proof. by rewrite [in LHS]/iqsort Fix_eq //=; exact: iqsort'_Fix. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)