proposition: Lemma peg4comp3 p1 p2 p3 : p1 != p2 -> p1 != p3 -> p2 != p3 -> exists p4, [/\ p4 != p3, p4 != p2 & p4 != p1] /\ (forall p, [\/ p = p1, p = p2, p = p3 | p = p4]).
proof: Proof. case: (peg4E p1)=>->; case: (peg4E p2)=>->; case: (peg4E p3)=>->; rewrite ?eqxx // => _ _ _; (comp3_tac peg0 || comp3_tac peg1 || comp3_tac peg2 || comp3_tac peg3). Qed.
imports: mathcomp(all_ssreflect) hanoi(ghanoi gdist)