proposition: Lemma Boundedt2: (exists x':float, (FtoRradix x'=r-x1*y1-x1*y2)%R /\ (Fbounded b x') /\ (Fexp x'=s+Fexp x+Fexp y)%Z).
proof: Proof. elim Boundedt1; intros t1 T; elim T; intros H1 T'; elim T'; intros H2 H3; clear T T'. unfold FtoRradix; apply BoundedL with t (Fminus radix t1 (Fmult x1 y2)); auto with zarith. unfold Fminus, Fopp, Fplus, Fmult; simpl. apply Zmin_Zle; auto with zarith. rewrite Fminus_correct; auto with zarith; rewrite Fmult_correct; auto with real zarith. fold FtoRradix; rewrite H1; ring. fold FtoRradix; replace (r-x1*y1-x1*y2)%R with ((-e)+x2*y1+x2*y2)%R. 2: apply trans_eq with (-e+x*y-(x+0)*y+x2*y1+x2*y2)%R;[ring|idtac]. 2: rewrite eeq; rewrite Xeq; rewrite Yeq; ring. apply Rle_lt_trans with ((Rabs e) + (Rabs (x2 * y1)) + (Rabs (x2 * y2)))%R. apply Rle_trans with (1:= Rabs_triang (-e + x2 * y1) (x2 * y2)%R). apply Rplus_le_compat_r. apply Rle_trans with (1:= Rabs_triang (-e) (x2 * y1)%R). rewrite Rabs_Ropp; right; ring. generalize eLe; generalize x2y1Le; generalize x2y2Le; intros. apply Rle_lt_trans with ( (Rabs e + Rabs (x2 * y1)+ (powerRZ radix (2 * s + Fexp x + Fexp y) / 4)))%R; auto with real. apply Rlt_le_trans with (Rabs e + (powerRZ radix (t + s + Fexp x + Fexp y) / 2 + powerRZ radix (2 * s + Fexp x + Fexp y) / 4)+powerRZ radix (2 * s + Fexp x + Fexp y) / 4)%R; auto with real. apply Rle_trans with (powerRZ radix (t + Fexp x + Fexp y) / 2+ (powerRZ radix (t + s + Fexp x + Fexp y) / 2 + powerRZ radix (2 * s + Fexp x + Fexp y) / 4) + powerRZ radix (2 * s + Fexp x + Fexp y) / 4)%R; auto with real. replace (s + Fexp x + Fexp y + t)%Z with (t+s+Fexp x+Fexp y)%Z;[idtac|ring]. apply Rplus_le_reg_l with (-((powerRZ radix (t + s + Fexp x + Fexp y) / 2)))%R. apply Rle_trans with (/2* (powerRZ radix (t + Fexp x + Fexp y)+ powerRZ radix (2 * s + Fexp x + Fexp y)))%R; [right; field; auto with real|idtac]. apply Rle_trans with (/2* powerRZ radix (t + s + Fexp x + Fexp y))%R;[idtac|right; field; auto with real]. apply Rmult_le_compat_l; auto with real. apply Rle_trans with (powerRZ radix (t+1 + Fexp x + Fexp y) + powerRZ radix (2 * s + Fexp x + Fexp y))%R; auto with real zarith. apply Rplus_le_compat_r. apply Rle_powerRZ; try apply IZR_le; auto with zarith. apply Rle_trans with (powerRZ radix (t+1 + Fexp x + Fexp y+1)). apply powerRZSumRle; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz