proposition: Lemma rem_subseq s : subseq (rem s) s.
proof: Proof. elim: s => //= y s IHs; rewrite eq_sym. by case: ifP => _; [apply: subseq_cons | rewrite eqxx]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)