proposition: Lemma allLeqP u a : reflect (maxL a u = a) (allLeq u a).
proof: Proof. Proof using. apply: (iffP idP); first exact: allLeqE. rewrite/allLeq; elim: u a => //= u0 u IHu a. rewrite maxC -maxXL => Hmax. have Hu : maxL a u = a. by apply le_anti; rewrite maxLb andbT -{2}Hmax le_max lexx orbT. by rewrite -{1}Hmax le_max lexx /= IHu. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools