proposition: Lemma sgdistE n (p2 : peg 4) (u v : configuration 4 n.+1) (p1 := u ldisk) (p3 := v ldisk): p1 != p2 -> p1 != p3 -> p2 != p3 -> p1 != p0 -> p2 != p0 -> p3 != p0 -> [/\ codom (sgdist1 p2 u v) \subset [:: p2; p3], codom (sgdist2 p2 u v) \subset [:: p1; p2] & `d[u, v]_smove = D[[:: ↓[u]; sgdist1 p2 u v; sgdist2 p2 u v; ↓[v]]].+2].
proof: Proof. move=> p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0. by rewrite /sgdist1 /sgdist2; case: sgdist_pair => [] [x y] []. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)