Closest2Prop.v

Require Export ClosestProp.
Section F2.
Variable b:Fbound.
Variable precision:nat.

Local FtoRradix := (FtoR (2)).
Coercion FtoRradix : float >-> R.

Theorem TwoMoreThanOne: (lt (S O) (2)).
Hypothesis precisionNotZero:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp (2) precision) (1)).

Theorem FevenNormMin: (Even (nNormMin (2) precision)).

Theorem EvenFNSuccFNSuccMid:
  (p:float) (Fbounded b p) -> (FNeven b (2) precision p) ->
  <R>
    (Fminus
       (2) (FNSucc b (2) precision (FNSucc b (2) precision p))
       (FNSucc b (2) precision p))==(Fminus (2) (FNSucc b (2) precision p) p).

Theorem AScal2:
  (p:float)<R> (Float (Fnum p) (Zplus (Fexp p) (1)))==(Rmult (2) p).
End F2.
Hints Resolve FevenNormMin :float.

30/05/01, 17:24