fact: Fixpoint partl p (s : (seq E * seq E)%type) (xs : seq E) : (seq E * seq E)%type := if xs is x :: xs then (if x <= p then partl p (rcons s.1 x, s.2) xs else partl p (s.1, rcons s.2 x) xs) else s.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)