Integers.v: add unsigned_inj

[jbaum98]

I've found useful the property that for integers, unsigned is injective:

Lemma unsigned_inj : forall x y : int,
    unsigned x = unsigned y -> x = y.