The order of subgoals in proof of eqnP.

[akr]

I found that the eqnP proof on p. 103 of the book version 1.0.2 differs from the actual Coq result.

The book describes the result after apply: (iffP idP). as follows.

n : nat
m : nat
===================
 m = n -> eqn m n

subgoal 2 is:
 eqn m n -> m = n

But Coq actually shows as follows.

  n, m : nat
  ============================
  eqn n m -> n = m

goal 2 is:
 n = m -> eqn n m

The order of subgoals is reversed.

[gares]

Thanks for sumitting the issue!