proposition: Lemma allLeq_consK b u a : allLeq (b :: u) a -> allLeq u a.
proof: Proof. Proof using. move/allP => Hall; apply/allP => x Hx; apply: Hall. by rewrite inE Hx orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools