proposition: Lemma size_lhanoi3E n (c1 c2 : _ _ n) : size_lhanoi3 c1 c2 = size (lhanoi3 c1 c2).
proof: Proof. elim: n c1 c2 => //= n IH c1 c2. case: eqP => [lc1Elc2|/eqP lc1Dlc2]. by rewrite size_map IH. case: (boolP (lrel _ _)) => [lc1Rlc2|lc1NRlc2]. by rewrite size_cat /= !size_map !IH addnS. rewrite size_cat /= size_cat /= !size_map size_app_lhanoi3_p lsym (negPf lc1NRlc2). by rewrite eq_sym (negPf lc1Dlc2) muln1 !addnS addnA !IH. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)