proposition: Lemma opeg_sym n (p1 p2 : peg n) : opeg p1 p2 = opeg p2 p1.
proof: Proof. rewrite /opeg; case: ltngtP => H; try by congr odflt; apply: eq_pick => p; rewrite andbC. suff -> : p1 = p2 by []. by apply/val_eqP/eqP. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)