proposition: Lemma size_rhanoi3E n (c1 c2 : _ _ n) : size_rhanoi3 c1 c2 = size (rhanoi3 c1 c2).
proof: Proof. elim: n c1 c2 => //= n IH c1 c2. case: eqP => [E|/eqP NE]. by rewrite size_map; apply: IH. set p := `p[_, _]. set x := size_rpeg _ _; set y := size_rpeg _ _. set z := size_rpeg _ _; set t := size_rpeg _ _. rewrite fun_if. rewrite size_cat /= size_cat /= size_cat /= !size_map. rewrite -!(size_rpegE, size_lpegE) /=. rewrite -/x -/y -/z -/t. rewrite size_ppeg -[_ + t.+1]addSnnS prednK ?expn_gt0 //. rewrite !addnS. rewrite /minn !addnA. case: leqP => LL1; case: leqP => LL2 //. by congr (_.+1); apply/eqP; rewrite eqn_leq LL1. by congr (_.+1); apply/eqP; rewrite eqn_leq ltnW // ltnW. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)