proposition: Theorem RoundAbsMonotoner : forall (P : R -> float -> Prop) (p : R) (q r : float), RoundedModeP b radix P -> Fbounded b r -> P p q -> (Rabs p <= r)%R -> (Rabs q <= r)%R.
proof: Proof. intros P p q r H' H'0 H'1 H'2. case (Rle_or_lt 0 p); intros Rl1. rewrite Rabs_right; auto with real. apply RleBoundRoundr with (P := P) (r := p); auto with real. rewrite <- (Rabs_right p); auto with real. apply Rle_ge; apply RleRoundedR0 with (P := P) (r := p); auto. rewrite Rabs_left1; auto. rewrite <- (Ropp_involutive r); apply Ropp_le_contravar. rewrite <- (Fopp_correct radix); auto. apply RleBoundRoundl with (P := P) (r := p); auto. apply oppBounded; easy. rewrite (Fopp_correct radix); rewrite <- (Ropp_involutive p); rewrite <- (Rabs_left1 p); auto with real; apply Rlt_le; auto. apply RleRoundedLessR0 with (P := P) (r := p); auto; apply Rlt_le; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz