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