ClosestMult.v

(****************************************************************************                                                                                         IEEE754  :  FroundMult                                                                                                                                          Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export FroundMult.
Require Export ClosestProp.
Section FRoundP.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

Theorem closestLessMultPos:
  (p:float) (r:R) (Closest b radix r p) -> (Rle R0 r) ->(Rle p (Rmult (2) r)).

Theorem closestLessMultNeg:
  (p:float) (r:R) (Closest b radix r p) -> (Rle r R0) ->(Rle (Rmult (2) r) p).

Theorem closestLessMultAbs:
  (p:float) (r:R) (Closest b radix r p) ->
  (Rle (Rabsolu p) (Rmult (2) (Rabsolu r))).
End FRoundP.

30/05/01, 17:25