proposition: Lemma path_rhanoi3 n (c1 c2 : _ _ n) (cs := rhanoi3 c1 c2) : path rmove c1 cs.
proof: Proof. have HHr := @rirr 3. rewrite {}/cs. elim: n c1 c2 => //= n IH c1 c2. 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 path_liftr. case: leqP => _; rewrite !cat_path /=; apply/and3P; split. - by rewrite -{1}[c1]cunliftrK path_liftr // path_rpeg. - rewrite -{1}[c1]cunliftrK last_map last_rpeg. apply/moveP; exists ldisk. split => // [|d dmDd||]. - by rewrite !cliftr_ldisk. - rewrite !ffunE; case: tsplitP => [j|j jE]; first by rewrite !ffunE. by case/eqP: dmDd; apply/val_eqP; rewrite /= jE; case: (j) => [] []. - apply/on_topP=> d; rewrite !cliftr_ldisk !ffunE. case: tsplitP => [j _ /eqP|j jE]. by rewrite !ffunE -/p1 eq_sym (negPf (opegDl _ _)). by rewrite /= !ffunE jE /= leq_addl. apply/on_topP=> d; rewrite /= !cliftr_ldisk !ffunE. case: tsplitP => [j _ /eqP|j ->]; last by case: j => [] []. by rewrite !ffunE eq_sym (negPf (opegDr _ _)). - by rewrite -[c3]cunliftrK !cliftr_ldisk /= path_liftr // cliftrK path_lpeg. - by rewrite -{1}[c1]cunliftrK path_liftr // path_rpeg. - rewrite -{1}[c1]cunliftrK last_map last_rpeg. apply/moveP; exists ldisk; split => // [|d2||]; rewrite ?cliftr_ldisk ?ffunE //=. - by rewrite /rrel /= eq_sym opegDl. - case: tsplitP => //= j d2E /eqP[]. by apply/val_eqP; rewrite /= d2E; case: (j) => [] []. - apply/on_topP=> d2. rewrite cliftr_ldisk /= !ffunE. case: tsplitP => [k _ /eqP | [[]] // j -> //]. by rewrite ?ffunE (negPf p1Dp2). apply/on_topP=> d2. rewrite cliftr_ldisk /= !ffunE. case: tsplitP => [k _ /eqP | [[]] // j -> //]. by rewrite !ffunE (negPf (opegDr _ _)). rewrite cat_path /=; apply/and3P; split => //. - rewrite -[c4]cunliftrK cliftr_ldisk -/p path_liftr // cliftrK // path_ppeg //. by rewrite eq_sym. - rewrite -[c4]cunliftrK cliftr_ldisk -/p last_map cliftrK // last_ppeg //. apply/moveP; exists ldisk; split => // [|d2||]; rewrite ?cliftr_ldisk ?ffunE /=. - by rewrite /rrel /= opegDr. - case: tsplitP => [j | j d2E /eqP[]] //=. by apply/val_eqP => /=; rewrite d2E; case: (j) => [] []. - apply/on_topP=> d2. rewrite cliftr_ldisk /= !ffunE. case: tsplitP => [k _ /eqP | [[]] // j -> //]. by rewrite !ffunE (negPf (opegDl _ _)). apply/on_topP=> d2. rewrite cliftr_ldisk /= !ffunE. case: tsplitP => [k _ /eqP | [[]] // j -> //]. by rewrite !ffunE eq_sym (negPf p1Dp2). by rewrite path_liftr // path_lpeg. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)