proposition: Lemma last_rhanoi3 n (c1 c2 : _ _ n) (cs := rhanoi3 c1 c2) : last c1 cs = c2.
proof: Proof. have HHr := @rirr 3. rewrite {}/cs. elim: n c1 c2 => /= [c1 c2 |n IH c1 c2]; first by apply/ffunP=> [] []. set p1 := _ ldisk; set p2 := _ ldisk. set c3 := cliftr _ _; set c4 := cliftr _ _; set c5 := cliftr _ _. set p := `p[_, _]. case: eqP => [p1Ep2|/eqP p1Dp2]. by rewrite -{1}[c1]cunliftrK last_map IH [c1 _]p1Ep2 cunliftrK. case: leqP => _; first by rewrite last_cat /= last_map last_lpeg cunliftrK. by rewrite last_cat /= last_cat /= last_map last_lpeg cunliftrK. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)