proposition: Lemma opegDr n (p1 p2 : peg n.+3) : opeg p1 p2 != p2.
proof: Proof. rewrite /opeg; case: pickP => [x /andP[]//| HD]. have D (p3 p4 : peg n.+3) : (p3 == p4) = (val p3 == val p4). by apply/eqP/idP => /val_eqP. have := HD sdisk; have := HD (inord 1); have := HD (inord 2). rewrite !D /= !inordK //. by case: {HD}p1 => [] [|[|[|p1 Hp1]]] /=; case: p2 => [] [|[|[|p2 Hp2]]]. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)