proposition: Lemma mem_rm_rep (A : eqType) (a b: A) s : b != a -> b \in s -> b \in rm_rep a s.
proof: Proof. elim: s a => //= c s IH a bDa; rewrite inE. case: (boolP (b == c)) => /= [/eqP<- _|bDc bIs]. by rewrite eq_sym (negPf bDa) inE eqxx. by have := IH _ bDc bIs; case: (_ == _); rewrite // inE orbC => ->. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)