Typo page 56: incorrect Definition

[usr345]

trafficstars

On page 56 the Definition says: Definition leq n m := m - n == 0.

It should be: Definition leq m n := m - n == 0.

It references to page 26 of Chapter 1, which has the correct definition:

Definition leq m n := m - n == 0.

[gares]

Thanks

[usr345]

@gares On page 119 no need to put "@" before Pack:

Definition nat_eqType : eqType := @Pack nat eqn. And before eq_op:

Check (@eq_op nat_eqType 3 4).