proposition: Lemma pE4 (p1 p2 p3 : peg 4) p : p1 != p2 -> p1 != p3 -> p2 != p3 -> p1 != p0 -> p2 != p0 -> p3 != p0 -> [\/ p = p0, p = p1, p = p2 | p = p3].
proof: Proof. rewrite /p0. by case: (peg4E p1) => ->; rewrite ?eqxx //; case: (peg4E p2) => ->; rewrite ?eqxx //; case: (peg4E p3) => ->; rewrite ?eqxx //; case: (peg4E p) => ->; rewrite ?eqxx // => *; try ((by apply: Or41) || (by apply: Or42) || (by apply: Or43) || (by apply: Or44)). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)