proposition: Lemma opeg3Kl p p1 p2 : p1 != p2 -> `p[`p[p1, p2], p1] = p2.
proof: Proof. move=> p1Dp2; apply/eqP. by rewrite !opeg3E ?(eqxx, p1Dp2) // [in p2 != p1]eq_sym p1Dp2. Qed.
imports: mathcomp(all_ssreflect) hanoi(ghanoi gdist)