proposition: Lemma so2_cor p1 p2 : 0 < m -> [/\ so2 p1 p2 != p0, so2 p1 p2 != p1 & so2 p1 p2 != p2].
proof: Proof. move=> m_gt0. rewrite /so2; case: (p1 =P _) => [->|/eqP p1D1]; rewrite /so2; case: (p2 =P _) => [->|/eqP p2D]. - by split; apply/eqP/val_eqP; rewrite /= !inordK. - by split; try (by rewrite eq_sym); apply/eqP/val_eqP; rewrite /= !inordK. - case: (p1 =P _) => [->|/eqP p1D2]. by split; apply/eqP/val_eqP; rewrite /= !inordK. by split; try (by rewrite eq_sym); apply/eqP/val_eqP; rewrite /= !inordK. by split; try (by rewrite eq_sym); apply/eqP/val_eqP; rewrite /= !inordK. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi)