Quelle  sub.pvs

sub: THEORY

  BEGIN
  IMPORTING add
  IMPORTING neg

  cx,cy: VAR cauchy_real
  x,y:   VAR real
  p:     VAR nat

  cauchy_sub(cx,cy:cauchy_real):cauchy_real
    = cauchy_add(cx,cauchy_neg(cy))

  sub_lemma: LEMMA cauchy_prop(x,cx) AND cauchy_prop(y,cy)
                   => cauchy_prop(x-y, cauchy_sub(cx,cy))

  END sub