number_fields_sq: THEORY
BEGIN

  IMPORTING number_fields_bis

  a,b : VAR numfield
  d,nz: VAR nznum

  sq(a): numfield = a*a

  sq_nz_pos         : JUDGEMENT sq(nz) HAS_TYPE nznum
  sq_rew            : LEMMA a*a = sq(a) 
  sq_neg            : LEMMA sq(-a) = sq(a)
  sq_times          : LEMMA sq(a*b) = sq(a) * sq(b)
  sq_plus           : LEMMA sq(a+b) = sq(a) + 2*a*b + sq(b)
  sq_minus          : LEMMA sq(a-b) = sq(a) - 2*a*b + sq(b)
  sq_neg_minus      : LEMMA sq(a-b) = sq(b-a)
  sq_0              : LEMMA sq(0) = 0
  sq_1              : LEMMA sq(1) = 1
  sq_eq_0           : LEMMA sq(a) = 0 IFF a = 0
  sq_div            : LEMMA sq(a/nz) = sq(a)/sq(nz)

  AUTO_REWRITE-     sq_neg_minus   

END number_fields_sq