proposition: Lemma opeg3E p p1 p2 : p1 != p2 -> (`p[p1, p2] == p) = ((p1 != p) && (p2 != p)).
proof: Proof. move=> p1Dp2. have D p3 p4 : (p3 == p4) = (val p3 == val p4). by apply/eqP/idP => /val_eqP. move: p1Dp2 (opegDl p1 p2) (opegDr p1 p2). by case: (peg3E (opeg p1 p2)) => ->; case: (peg3E p1) => ->; case: (peg3E p2) => ->; case: (peg3E p) => ->; rewrite !D /peg1 /peg2 /peg3 /= ?inordK. Qed.
imports: mathcomp(all_ssreflect) hanoi(ghanoi gdist)