proposition: Lemma peg4E p : [\/ p = peg0, p = peg1, p = peg2 | p = peg3].
proof: Proof. by case: p => [] [|[|[|[|]]]] // H; [apply: Or41|apply: Or42|apply: Or43|apply: Or44]; apply/val_eqP; rewrite //= inordK. Qed.
imports: mathcomp(all_ssreflect) hanoi(ghanoi gdist)