proposition: Lemma well_founded_lt2 : well_founded (fun x y : nat * nat => (x.2 < y.2)%coq_nat).
proof: Proof. by apply: (@Wf_nat.well_founded_lt_compat _ _) => -[x1 x2] [y1 y2]; exact. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)