proposition: Theorem RoundedModeMult : forall P, RoundedModeP b radix P -> forall (r : R) (q q' : float), P r q -> Fbounded b q' -> (r <= radix * q')%R -> (q <= radix * q')%R.
proof: Proof. intros P H' r q q' H'0 H'1. replace (radix * q')%R with (FtoRradix (Float (Fnum q') (Fexp q' + 1%nat))). intros H'2; case H'2. intros H'3; case H'; intros H'4 H'5; elim H'5; intros H'6 H'7; elim H'7; intros H'8 H'9; apply H'9 with (1 := H'3); clear H'7 H'5; auto. apply RoundedModeProjectorIdem; auto. apply FBoundedScale; auto. intros H'3. replace (FtoRradix q) with (FtoRradix (Float (Fnum q') (Fexp q' + 1%nat))); auto with real. apply (RoundedProjector _ _ P H'); auto. apply FBoundedScale; auto. case H'. intros H'4 H'5; elim H'5; intros H'6 H'7; clear H'5. apply (H'6 r (Float (Fnum q') (Fexp q' + 1)) q); auto. apply RoundedModeBounded with (P := P) (r := r); auto. rewrite (FvalScale _ radixMoreThanOne b). rewrite powerRZ_1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz