proposition: Lemma in_maxL a u : (maxL a u) \in a :: u.
proof: Proof. Proof using. elim: u a => [| u0 u IHu]//= a; first by rewrite mem_seq1. case (leP a u0) => H. + by have:= H => /max_idPr ->; rewrite in_cons IHu orbT. + have:= ltW H => /max_idPl ->; rewrite !in_cons. by rewrite orbA [(_ == _) || (_ == _) ]orbC -orbA -in_cons IHu orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools