proposition: Lemma subseq_rcons_neq s si w wn : si != wn -> subseq (rcons s si) (rcons w wn) = subseq (rcons s si) w.
proof: Proof. Proof using. move/negbTE => neq. by rewrite -subseq_rev !rev_rcons /= neq -rev_rcons subseq_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted