proposition: Lemma so1_cor p : so1 p != p0 /\ so1 p != p.
proof: Proof. rewrite /so1; case: (p =P _) => [->|/eqP pD1]; split. - by apply/eqP/val_eqP; rewrite /= !inordK. - by apply/eqP/val_eqP; rewrite /= !inordK. - by apply/eqP/val_eqP; rewrite /= !inordK. by rewrite eq_sym. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi)