proposition: Lemma last_lhanoi3 n (c1 c2 : _ _ n) (cs := lhanoi3 c1 c2) : last c1 cs = c2.
proof: Proof. have HH := @lirr 3. rewrite /cs; elim: n c1 c2 {cs} => /= [c1 c2| n IH c1 c2]. by apply/ffunP=> [] []. case: eqP => [Ho|/eqP Do]. by rewrite -{1}[c1](cunliftrK) Ho last_map IH // cunliftrK. set p1 := _ ldisk; set p2 := opeg _ _. set cp2 := `c[_]; set cp := `c[_]; set cp1 := `c[_]. case: (boolP (lrel _ _)) => [Hrel|Hrel]. by rewrite last_cat /= last_map IH cunliftrK. by rewrite last_cat /= last_cat /= last_map IH cunliftrK. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)