(* Title : NthRoot.thy Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Description : Existence of nth root. Adapted from http://www.math.unl.edu/~webnotes *) NthRoot = SEQ + ExtraThms2