proposition: Lemma connect_sym n : connect_sym (@move n).
proof: Proof. move=> c1 c2. apply/connectP/connectP=> [] [p H1 H2]. exists (rev (belast c1 p)); first by rewrite H2 path_move_rev. by case: (p) H2 => [->//|c3 p1 _]; rewrite rev_cons last_rcons. exists (rev (belast c2 p)); first by rewrite H2 path_move_rev. by case: (p) H2 => [->//|c3 p1 _]; rewrite rev_cons last_rcons. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)