proposition: Lemma Boundedt4_aux: (exists x':float, (FtoRradix x'=r-x1*y1-x1*y2-x2*y1-x2*y2)%R /\ (Fbounded b x') /\ (Fexp x'=Fexp x+Fexp y)%Z).
proof: Proof. elim errorBoundedMult with b radix t (Closest b radix) x y r; auto with zarith. 2: apply ClosestRoundedModeP with t; auto with zarith. 2: elim Nx; auto. 2: elim Ny; auto. intros g T; elim T; intros H1 T'; elim T'; intros; clear T T'. exists (Fopp g); split. unfold FtoRradix;rewrite Fopp_correct; rewrite H1; fold FtoRradix. rewrite Xeq; rewrite Yeq; ring. split;[apply oppBounded; auto|simpl; auto]. Qed.
imports: Reals ZArith List PeanoNat Psatz