src/HOL/Integ/Lagrange.thy

New theorem priK_inj_eq, injectivity of priK

(*  Title:      HOL/Integ/Lagrange.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1996 TU Muenchen


This theory only contains a single thm, which is a lemma in Lagrange's proof
that every natural number is the sum of 4 squares.  It's sole purpose is to
demonstrate ordered rewriting for commutative rings.

The enterprising reader might consider proving all of Lagrange's thm.
*)
Lagrange = Ring +

constdefs sq :: 'a::times => 'a
         "sq x == x*x"

end