proposition: Lemma allLeq_posbig l s : allLeq (take (posbig (l :: s)) (l :: s)) (maxL l s).
proof: Proof. Proof using. have:= maxLP l s; rewrite -{1}[l :: s](cat_take_drop (posbig (l :: s))). by rewrite allLeq_catE => /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools