proposition: Lemma path_shift m n (c : configuration (m + n)) cs : path move c cs -> size cs = (size (rm_rep (clshift c) [seq (clshift i) | i <- cs]) + size(rm_rep (crshift c) [seq (crshift i) | i <- cs]))%nat.
proof: Proof. elim: cs c => //= c1 cs IH c /andP[/moveP[d [d2H d2H1 d2H2 d2H3]] c1Pcs]. case: (tsplitP d) => [j dE | k dE]. rewrite ifT; last first. apply/eqP/ffunP=> i; rewrite !ffunE. apply: d2H1; apply/eqP => /val_eqP /=. by rewrite dE eqn_leq andbC leqNgt (leq_trans (ltn_ord _)) ?leq_addl. rewrite ifN /=; last first. apply/eqP => /ffunP /(_ j); rewrite !ffunE => cE. move: d2H; rewrite (_ : c d = c1 d) ?(irH) //. by rewrite (_ : d = (trshift m j)) //=; apply/val_eqP/eqP. rewrite addnS; congr _.+1. by apply: IH. rewrite ifN /=; last first. apply/eqP => /ffunP /(_ k); rewrite !ffunE => cE. move: d2H; rewrite (_ : c d = c1 d) ?(irH) //. by rewrite (_ : d = (tlshift n k)) //=; apply/val_eqP/eqP. rewrite ifT; last first. apply/eqP/ffunP=> i; rewrite !ffunE. apply: d2H1; apply/eqP => /val_eqP /=. by rewrite dE eqn_leq leqNgt (leq_trans (ltn_ord _)) ?leq_addl. congr _.+1. by apply: IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)