proposition: Lemma subseq_rm_rep (A : eqType) (a : A) s : subseq (rm_rep a s) s.
proof: Proof. elim: s a => // b s IH a. rewrite [rm_rep _ _]/=; case: (a == b). by apply: subseq_trans (IH _) (subseq_cons _ _). by rewrite /= eqxx IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)