proposition: Lemma lpeg_min n (c : configuration 3 n) p cs : path rmove `c[p] cs -> last `c[p] cs = c -> size_rpeg c p <= size cs ?= iff (cs == lpeg p c).
proof: Proof. move=> pPcs lccsEc. have HHs := @rsym 3. have cPr : path rmove c (rev (belast `c[p] cs)). by rewrite -{1}lccsEc path_move_rev. have lcrEp : last c (rev (belast `c[p] cs)) = `c[p]. rewrite -lccsEc; case: (cs)=> //= c3 cs1. by rewrite rev_cons last_rcons. have := rpeg_min cPr lcrEp. rewrite /lpeg size_rev size_belast. set u := rev _ ; set v := rpeg _ _. have -> : (u == v) = (rev (c :: u) == rev (c :: v)). rewrite !rev_cons eqseq_rcons eqxx andbT. apply/eqP/eqP=> [->//|]. by rewrite -{2}[u]revK => ->; rewrite revK. rewrite [c :: v]lastI -/v rev_rcons. rewrite rev_cons revK -{2}lccsEc -lastI eqseq_cons andbC. case: eqP=> //; case: eqP => // pDl Hcs; case: pDl. by rewrite last_rpeg. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)