proposition: Theorem errorBoundedMultPos : forall P, RoundedModeP b radix P -> forall p q f : float, Fbounded b p -> Fbounded b q -> (0 <= p)%R -> (0 <= q)%R -> (- dExp b <= Fexp p + Fexp q)%Z -> P (p * q)%R f -> exists r : float, r = (p * q - f)%R :>R /\ Fbounded b r /\ Fexp r = (Fexp p + Fexp q)%Z.
proof: Proof. intros P H p q f H0 H1 H2 H3 H4 H5. generalize errorBoundedMultMin errorBoundedMultMax; intros H6 H7. cut (MinOrMaxP b radix P); [ intros | case H; intros H'1 (H'2, (H'3, H'4)); auto ]. case (H8 (p * q)%R f); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz