proposition: Lemma last_rm_rep (A : eqType) (a : A) s : last a (rm_rep a s) = last a s.
proof: Proof. by elim: s a => //= b l IH a; case: (_ =P _) => /= [->|_]; apply: IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)