proposition: Lemma Boundedt3: (exists x':float, (FtoRradix x'=r-x1*y1-x1*y2-x2*y1)%R /\ (Fbounded b x') /\ (Fexp x'=s+Fexp x+Fexp y)%Z).
proof: Proof. elim Boundedt2; intros t2 T; elim T; intros H1 T'; elim T'; intros H2 H3; clear T T'. unfold FtoRradix; apply BoundedL with t (Fminus radix t2 (Fmult x2 y1)); 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-x2*y1)%R with ((-e)+x2*y2)%R. 2: apply trans_eq with (-e+x*y-(x+0)*y+x2*y2)%R;[ring|idtac]. 2: rewrite eeq; rewrite Xeq; rewrite Yeq; ring. apply Rle_lt_trans with ((Rabs e) + (Rabs (x2 * y2)))%R. apply Rle_trans with (1:= Rabs_triang (-e) (x2 * y2)%R). rewrite Rabs_Ropp; right; ring. generalize eLe; generalize x2y2Le; intros. apply Rle_lt_trans with (powerRZ radix (t + Fexp x + Fexp y) / 2+powerRZ radix (2 * s + Fexp x + Fexp y) / 4)%R; auto with real. apply Rlt_le_trans with (powerRZ radix (t + Fexp x + Fexp y) + powerRZ radix (2 * s + Fexp x + Fexp y) / 4)%R. apply Rplus_lt_compat_r. apply Rlt_le_trans with (powerRZ radix (t + Fexp x + Fexp y)*1)%R;[idtac|right; ring]. unfold Rdiv; apply Rmult_lt_compat_l; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rlt_le_trans with (/1)%R; auto with real. apply Rle_trans with (powerRZ radix (t+1 + Fexp x + Fexp y) + powerRZ radix (2 * s + Fexp x + Fexp y))%R;[apply Rplus_le_compat|idtac]. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. apply Rle_trans with (powerRZ radix (2*s + Fexp x + Fexp y)*1)%R;[idtac|right; ring]. unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. assert (0 < 4)%R;[apply Rlt_le_trans with 2%R; auto with real|idtac]. apply Rmult_le_reg_l with 4%R; auto with real. apply Rle_trans with 1%R;[right; field|ring_simplify (4*1)%R]; auto with real. apply Rle_trans with (powerRZ radix (t + 1 + Fexp x + Fexp y+1)). apply powerRZSumRle; auto with zarith. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz