proposition: Lemma size_cut_tuc (c : configuration _ _) cs : path (move rel) c cs -> size cs = (size (rm_rep (ccut c) [seq (ccut i) | i <- cs]) + size (rm_rep (ctuc c) [seq (ctuc i) | i <- cs]))%nat.
proof: Proof. elim: cs c => //= c1 cs IH c /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 [tLd|dLt] := leqP t d; last first. rewrite ifN /= ?addSn; last first. apply/eqP => /ffunP /(_ (Ordinal dLt)). by rewrite !ffunE ordinalK => /eqP; rewrite (negPf cdDc1d). rewrite ifT; last first. apply/eqP/ffunP=> i; rewrite !ffunE dH2 //=. apply/eqP => /val_eqP. by rewrite /= eqn_leq [_ <= d]leqNgt (leq_trans dLt) ?andbF // leq_addl. by congr (_.+1); apply: IH. rewrite ifT; last first. apply/eqP/ffunP=> i; rewrite !ffunE dH2 //. by apply/eqP => /val_eqP; rewrite /= eqn_leq leqNgt (leq_trans (ltn_ord _)). rewrite ifN /= ?addSn; last first. apply/eqP => /ffunP /(_ (otuc tLd)) /eqP. by rewrite !ffunE otucK (negPf cdDc1d). by rewrite addnS; congr (_.+1); apply: IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)