proposition: Lemma maxL_cat a u b v : maxL a (u ++ b :: v) = Order.max (maxL a u) (maxL b v).
proof: Proof. Proof using. elim: u a => [| u0 u IHu]/= a; first by rewrite maxXL. exact: IHu. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools