proposition: Theorem RoundedModeMultAbs : forall P, RoundedModeP b radix P -> forall (r : R) (q q' : float), P r q -> Fbounded b q' -> (Rabs r <= radix * q')%R -> (Rabs q <= radix * q')%R.
proof: Proof. intros P H' r q q' H'0 H'1 H'2. case (Rle_or_lt 0 r); intros Rl0. rewrite Rabs_right; auto. apply RoundedModeMult with (P := P) (r := r); auto. rewrite <- (Rabs_right r); auto with real. apply Rle_ge; apply RleRoundedR0 with (P := P) (r := r); auto. rewrite Rabs_left1; auto. replace (radix * q')%R with (- (radix * - q'))%R; [ apply Ropp_le_contravar | ring ]. rewrite <- (Fopp_correct radix). apply RoundedModeMultLess with (P := P) (r := r); auto. apply oppBounded; auto. unfold FtoRradix in |- *; rewrite Fopp_correct. rewrite <- (Ropp_involutive r). replace (radix * - FtoR radix q')%R with (- (radix * q'))%R; [ apply Ropp_le_contravar | fold FtoRradix;ring ]; auto. rewrite <- (Rabs_left1 r); auto. apply Rlt_le; auto. apply RleRoundedLessR0 with (P := P) (r := r); auto. apply Rlt_le; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz