proposition: Lemma size_rm_rep_subset (A : finType) (a : A) (s1 : {set A}) (s2 : seq A) : {subset s1 <= s2} -> a \notin s1 -> #|s1| <= size (rm_rep a s2).
proof: Proof. elim: s2 s1 a => /= [s1 a aS _|b s2 IH s1 a s1S aNIs1]. rewrite leqn0 cards_eq0; apply/eqP/setP=> i. by rewrite inE; apply/idP => /aS. case: eqP=> [aEb|aDb]. rewrite -aEb; apply: IH => //. move=> i is1; have := is1; have := s1S _ is1; rewrite inE. by case/orP=> [/eqP->|//]; rewrite -aEb => aIs1; case/negP: aNIs1. have [bIs1|bNIs1]/= := boolP (b \in s1); last first. apply: leq_trans (IH _ _ _ bNIs1) _ => //. move=> i is1; have := is1; have := s1S _ is1; rewrite inE. by case/orP=> [/eqP->|//] => bIs1; case/negP: bNIs1. rewrite (cardsD1 b) bIs1 ltnS. apply: IH => [i|]. by rewrite !inE => /andP[iDb1 /s1S]; rewrite inE (negPf iDb1). by rewrite !inE eqxx. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)