proposition: Lemma maxL_LbR a v L b R : a :: v = L ++ b :: R -> allLeq L b -> allLeq R b -> maxL a v = b.
proof: Proof. Proof using. rewrite /allLeq /maxL => Heq HL Hr. apply/eqP; rewrite eq_le; apply/andP; split. - have: all (<= b) (a :: v) by rewrite Heq all_cat HL /= lexx Hr. by move/allP => Hallv; apply: Hallv; exact: in_maxL. - have:= maxLP a v => /allP; rewrite Heq; apply. by rewrite mem_cat inE eq_refl /= orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools