proposition: Lemma cat_rm_rep (A : eqType) (a : A) s1 s2 : rm_rep a (s1 ++ s2) = rm_rep a s1 ++ rm_rep (last a s1) s2.
proof: Proof. elim: s1 s2 a => //= b s1 IH s2 a. case: eqP => [aEb|aDb] /=; first by apply: IH. by congr (_ :: _); apply: IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)