[Agda] Constructors are injective -- standard proof?

[Nils Anders Danielsson]

On 2014-06-05 16:20, Jacques Carette wrote:
> Related specific question: Is there a reason why all those useful
> little lemmas are all private in Data.Nat.Properties?

If they weren't private there would (in many cases) be two different
names for the same property. For instance,

   ⊔-assoc

and

   IsCommutativeSemiringWithoutOne.+-assoc
     ⊔-⊓-0-isCommutativeSemiringWithoutOne

would refer to the same thing. The style I've (mostly?) followed is to
avoid exporting ad-hoc names for values that can be accessed via a
record.

> I've had to reprove some of them because of that.

I guess you refer to m+1+n≡1+m+n and m*1+n≡m+mn. These properties can be
proved using the semiring solver, so I didn't want to pollute the name
space with these names.

-- 
/NAD