proposition: Lemma peg3E p : [\/ p = peg1, p = peg2 | p = peg3].
proof: Proof. by case: p => [] [|[|[|]]] // H; [apply: Or31|apply: Or32|apply: Or33]; apply/val_eqP; rewrite //= inordK. Qed.
imports: mathcomp(all_ssreflect) hanoi(ghanoi gdist)