proposition: Theorem EvenClosestFabs : forall (f : float) (r : R), (Fcanonic radix bo f) -> EvenClosest bo radix precision r f -> EvenClosest bo radix precision (Rabs r) (Fabs f).
proof: Proof. intros. case (Rle_or_lt 0%R r); intros. rewrite Rabs_right; auto with real. unfold Fabs; rewrite Z.abs_eq; auto with zarith. apply LeR0Fnum with (radix := radix); auto with zarith. apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) r; auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. rewrite Rabs_left; auto with real. replace (Fabs f) with (Fopp f). generalize EvenClosestSymmetric; unfold SymmetricP; auto. unfold Fabs, Fopp; rewrite <- Zabs_Zopp; rewrite Z.abs_eq; auto. assert (Fnum f <= 0)%Z; auto with zarith. apply R0LeFnum with (radix:=radix); auto with zarith. apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) r; auto with zarith real. apply EvenClosestRoundedModeP; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz