proposition: Lemma allLtnCons b u a : b < a -> allLtn u a -> allLtn (b :: u) a.
proof: Proof. Proof using. move=> Hb /allP Hall; apply/allP => x. by rewrite inE => /orP[/eqP-> //|] /Hall. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools