proposition: Lemma maxLb a u : a <= maxL a u.
proof: Proof. Proof using. elim: u a => //= u0 u IHu a. apply: (@le_trans _ _ (Order.max a u0)); last exact: IHu. by rewrite le_max lexx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools