[Agda] Constructors are injective -- standard proof?

[Jacques Carette]

General question:  Is there a proof in the standard library that 
constructors for inductive types are injective?  Or is this something 
that must be proven for every single data type?

Specific question: Is the proof that 'suc' is injective in the standard 
library?  I searched for it, and could not find it.  [Of course it is 
trivial, but it seems silly to rewrite this over and over again, which 
is what a 'standard' library is for].

Related specific question: Is there a reason why all those useful little 
lemmas are all private in Data.Nat.Properties?  I've had to reprove some 
of them because of that.  Which seems silly.

Jacques