skaller wrote:
> The reason may be because the equality of integers
> isn't the same as algebraic equality of the data structures:

Indeed, but this is not about maintaining an invariant. Because of the
representation of Big_int.big_int as a pair (sign,absolute value), the
polymorphic comparison would give (-1) < (-2) if the custom comparison
were used for Nat.nat.

-- Alain