proposition: Lemma allLtn_rconsK b u a : allLtn (rcons u b) a -> allLtn u a.
proof: Proof. Proof using. rewrite -allLtn_rev rev_rcons => /allLtn_consK. by rewrite allLtn_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools