proposition: Lemma gdist_liftr_perfect q n (hrel : rel (peg q)) p1 p2 p3 : irreflexive hrel -> hrel p1 p2 -> p1 != p3 -> p2 != p3 -> `d[↑[perfect p3 : configuration q n]_p1, ↑[perfect p3]_p2]_(move hrel) = 1.
proof: Proof. move=> hirr p1Rp2 p1Dp3 p2Dp3. apply/eqP; rewrite eqn_leq; apply/andP; split. rewrite -[1]/(size [:: cliftr p2 `c[p3, n]]). apply: gdist_path_le => //=. by rewrite move_liftr_perfect. case E : gdist => //. move/eqP: E; rewrite gdist_eq0 => /eqP E. have := cliftr_ldisk p1 `c[p3, n]. rewrite E cliftr_ldisk => p2Ep1. by have := hirr p1; rewrite -{2}p2Ep1 p1Rp2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)