[Agda] Integer lemmata

[Sergei Meshveliani]

On Thu, 2014-01-09 at 01:03 +0000, Arseniy Alekseyev wrote:

> It looks like the -* and *- lemmata correspond to
> Algebra.Props.Ring.-‿*-distribˡ and Algebra.Props.Ring.-‿*-distribʳ.


Indeed! Thank you.

------
Sergei
 

> On 8 January 2014 21:51, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > People,
> >
> > this is on  Standard library lib-0.7.
> >
> > I need to use 15-20 trivial lemmata for  Integer,  like these:
> >
> >        x * (+ 0) ≡ + 0
> >        x * (- y) ≡ - (x * y)
> >
> > For this, I use  Data.Integer.Properties.commutativeRing,
> > and still write the code shown below.
> >
> > I suspect that I write for this too much code of my own.
> > Consider, for example,  `-*' below.
> > Can this be simplified? (may be, by taking something from library).
> >
[..]