proposition: Lemma rembig_subseq s : subseq (rembig s) s.
proof: Proof. Proof using. elim: s => //= s0 s IHs. case: allLtn; last by rewrite eq_refl. case: s {IHs} => [//| s1 s]. by case: eqP => _; [apply: subseq_cons | apply: subseq_refl]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools