proposition: Lemma lrel3ON4 (p1 p2 p3 p4 : peg 3) : p1 != p2 -> p1 != p3 -> p2 != p3 -> lrel p1 p2 -> lrel p1 p3 -> lrel p3 p4 -> p4 = p1.
proof: Proof. have D p5 p6 : (p5 == p6) = (val p5 == val p6). by apply/eqP/idP => /val_eqP. by case: (peg3E p1) => ->; case: (peg3E p2) => ->; case: (peg3E p3) => ->; case: (peg3E p4) => ->; rewrite !D /lrel /= ?inordK. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)