proposition: Lemma lrel3B (p1 p2 : peg 3) : p1 != p2 -> ~~ [&& lrel p1 p2, lrel p1 `p[p1, p2] & lrel p2 `p[p1, p2]].
proof: Proof. have D p3 p4 : (p3 == p4) = (val p3 == val p4). by apply/eqP/idP => /val_eqP. move: (opegDl p1 p2) (opegDr p1 p2). by case: (peg3E `p[p1, p2]) => ->; case: (peg3E p1) => ->; case: (peg3E p2) => ->; rewrite !D /lrel /= ?inordK. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)