proposition: Lemma sorted_leq_last A a : sorted ltn (a :: A) -> a <= last a A.
proof: Proof. Proof using. move=> /sorted_in_leq_last H. by have /H /= : a \in (a :: A) by rewrite inE eq_refl. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure