proposition: Lemma shanoi_connect n (c1 c2 : configuration m.+3 n) : c1 `-->* c2.
proof: Proof. apply: connect_trans (shanoi_connect_perfect _ p0) _. rewrite (connect_sym (@ssym m.+3)). apply: shanoi_connect_perfect. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi)