fact: Definition so2 p1 p2 : (peg m.+3) := if (p1 == inord 1) then if (p2 == inord 2) then inord 3 else inord 2 else if (p2 == inord 1) then if (p1 == inord 2) then inord 3 else inord 2 else inord 1.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi)