fact: Fixpoint ipartl p i ny nz nx : M (nat * nat)%type := if nx is k.+1 then aget (i + (ny + nz)) >>= (fun x => if x <= p then aswap (i + ny) (i + ny + nz) >> ipartl p i ny.+1 nz k else ipartl p i ny nz.+1 k) else Ret (ny, nz).
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)