proposition: Lemma sorted_in_leq_last A a : sorted ltn A -> a \in A -> a <= last 0 A.
proof: Proof. Proof using. elim: A a => // A0 A IHA a /= Hpart. rewrite inE => /orP[/eqP |] Ha. - subst a => {IHA}. elim: A A0 Hpart => // A1 A IHA A0 /= /andP[/ltnW H01 {}/IHA]. exact: leq_trans H01. - move/(_ _ (path_sorted Hpart) Ha): IHA => {Hpart}. by case: A Ha. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure