proposition: Lemma refin_qperm_partl a b p xs : qperm_partl (M := M) p a b xs `<=` apply_pair_snd qperm (partl p (a, b) xs).
proof: Proof. apply: refin_trans; last exact: refin_qperm_partl_helper. rewrite kleisliE apply_triple_sndE. rewrite -[X in X `<=` _](bindretf b (qperm_partl p a ^~ xs)). exact/refin_bindr/refin_qperm_ret. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)