proposition: Lemma allLtnConsE u a b : allLtn (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 gt_max -IHu /= !andbA [(u0 < a) && (b < a)]andbC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools