proposition: Lemma maxLPt a u : allLeq u (maxL a u).
proof: Proof. Proof using. rewrite/allLeq; apply/allP => x Hx. elim: u Hx a => //= u0 u IHu; rewrite inE => /orP[/eqP-> | /IHu Hx] a. - by rewrite maxC -maxXL le_max lexx. - exact: Hx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools