proposition: Lemma size_cset2 (c : configuration _ _) cs : all (cvalid sd sp1) (c :: cs) -> all (cvalid (~: sd) sp2) (c :: cs) -> path (move rel1) c cs -> size cs = (size (rm_rep (cset2 sd p1Isp1 c) [seq (cset2 sd p1Isp1 i) | i <- cs]) + size (rm_rep (cset2 (~: sd) p2Isp2 c) [seq (cset2 (~: sd) p2Isp2 i) | i <- cs]))%nat.
proof: Proof. elim: cs c => //= c1 cs IH c /and3P[c1V1 c2V1 c3V1] /and3P[c1V2 c2V2 c3V2] /andP[/moveP[d [dH1 dH2 dH3 dH4]] c1Pcs]. have cdDc1d : c d != c1 d. by have /idP/negP := irH (c d); apply: contra => /eqP {2}->. have [dIsd|dNIsd] := boolP (d \in sd). rewrite ifN /= ?addSn; last first. apply/eqP => /ffunP /(_ (enum_rank_in dIsd d)). rewrite !ffunE enum_rankK_in // => /enum_rank_in_inj => H. case/eqP : cdDc1d; apply: H; first by have /cvalidP := c1V1; apply. by have /cvalidP := c2V1; apply. rewrite ifT; last first. apply/eqP/ffunP=> i; rewrite !ffunE dH2 //. have := enum_valP i; rewrite inE. by apply: contra => /eqP<-. by congr (_.+1); apply: IH; rewrite ?c2V1 ?c2V2. rewrite ifT; last first. apply/eqP/ffunP=> i; rewrite !ffunE dH2 //. apply: contra dNIsd => /eqP->. by have := enum_valP i. have dd : d \in ~: sd by rewrite inE. rewrite ifN /= ?addSn; last first. apply/eqP => /ffunP /(_ (enum_rank_in dd d)). rewrite !ffunE enum_rankK_in // => /enum_rank_in_inj => H. case/eqP : cdDc1d; apply: H. by have /cvalidP := c1V2; apply. by have /cvalidP := c2V2; apply. by rewrite addnS; congr (_.+1); apply: IH; rewrite ?c2V1 ?c2V2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)