proposition: Lemma allLeqConsE u a b : allLeq (b :: u) a = (maxL b u <= a).
proof: Proof. Proof using. elim: u b => [| u0 u IHu]/= b; first by rewrite andbT. by rewrite maxC -maxXL ge_max -IHu /= !andbA [(u0 <= a) && (b <= a)]andbC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools