proposition: Lemma allLeq_rconsK b u a : allLeq (rcons u b) a -> allLeq u a.
proof: Proof. Proof using. rewrite -allLeq_rev rev_rcons => /allLeq_consK. by rewrite allLeq_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools