proposition: Lemma path_lhanoi3 n (c1 c2 : _ _ n) (cs := lhanoi3 c1 c2) : path lmove c1 cs.
proof: Proof. have HH := @lirr 3. rewrite /cs; elim: n c1 c2 {cs} => //= n IH c1 c2. case: eqP => [Ho|/eqP Do]. by rewrite -{1}[c1](cunliftrK) Ho path_liftr. set p1 := _ ldisk; set p2 := opeg _ _. set cp2 := `c[_]; set cp := `c[_]; set cp1 := `c[_]. case: (boolP (lrel _ _)) => [Hrel|Hrel]. rewrite cat_path /=; apply/and3P; repeat split. - by rewrite -{1}[c1]cunliftrK path_liftr. - rewrite -{1}[c1]cunliftrK last_map last_lhanoi3. by apply: move_liftr_perfect; rewrite // eq_sym (opegDl, opegDr). by rewrite path_liftr. rewrite cat_path /= cat_path /=; apply/and5P; split. - by rewrite -{1}[c1]cunliftrK /= path_liftr. - rewrite -{1}[c1]cunliftrK /= last_map last_lhanoi3. - apply: move_liftr_perfect => //; first by apply: lrel3O. by rewrite opegDr. - by rewrite path_liftr. - rewrite last_map last_lhanoi3. apply: move_liftr_perfect => //. - rewrite /p2 opeg_sym lsym lrel3O ?opegDl //; first by rewrite eq_sym. by rewrite lsym. - by rewrite opegDl. by rewrite eq_sym. by rewrite path_liftr. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)