proposition: Lemma Boundedt1: (exists x':float, (FtoRradix x'=r-x1*y1)%R /\ (Fbounded b x') /\ (Fexp x'=t-1+Fexp x+Fexp y)%Z).
proof: Proof. unfold FtoRradix; apply BoundedL with t (Fminus radix r (Fmult x1 y1)); auto with zarith. unfold Fminus, Fopp, Fplus, Fmult; simpl. apply Zmin_Zle; auto with zarith. apply rExp. rewrite Fminus_correct; auto with zarith; rewrite Fmult_correct; auto with real zarith. fold FtoRradix. replace (r-x1*y1)%R with ((-e)+x1*y2+x2*y1+x2*y2)%R. 2: apply trans_eq with (-e+x*y-(x+0)*y+x1*y2+x2*y1+x2*y2)%R;[ring|idtac]. 2: rewrite eeq; rewrite Xeq; rewrite Yeq; ring. apply Rle_lt_trans with ((Rabs e)+(Rabs (x1 * y2)) + (Rabs (x2 * y1)) + (Rabs (x2 * y2)))%R. apply Rle_trans with (1:= Rabs_triang (-e+ x1 * y2 + x2 * y1) (x2 * y2)%R). apply Rplus_le_compat_r. apply Rle_trans with (1:= Rabs_triang (-e+ x1 * y2) (x2 * y1)%R). apply Rplus_le_compat_r. apply Rle_trans with (1:= Rabs_triang (-e) (x1 * y2)%R). rewrite Rabs_Ropp; right; ring. generalize eLe; generalize x1y2Le; generalize x2y1Le; generalize x2y2Le; intros. apply Rlt_le_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 (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 Rlt_le_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 (t + s + Fexp x + Fexp y) / 2 + powerRZ radix (2 * s + Fexp x + Fexp y) / 4) + Rabs (x2 * y2))%R; auto with real. apply Rplus_lt_compat_r. apply Rle_lt_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) + Rabs (x2 * y1))%R; auto with real. apply Rle_trans with (powerRZ radix (t + s + Fexp x + Fexp y)+ powerRZ radix (t + Fexp x + Fexp y) / 2 +3*powerRZ radix (2 * s + Fexp x + Fexp y) / 4)%R; [right; field; auto with real|idtac]. assert (0 < 8)%R; auto with real. apply Rle_trans with (powerRZ radix (t + s + Fexp x + Fexp y) + powerRZ radix (t + Fexp x + Fexp y) + powerRZ radix (2 * s + Fexp x + Fexp y))%R; [apply Rplus_le_compat; try apply Rplus_le_compat_l |idtac]. unfold Rdiv; apply Rle_trans with (powerRZ radix (t + Fexp x + Fexp y)*1)%R;[idtac|right; ring]. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (/1)%R; auto with real. unfold Rdiv; apply Rle_trans with (powerRZ radix (2*s + Fexp x + Fexp y)*1)%R;[idtac|right; ring]. apply Rle_trans with (powerRZ radix (2*s + Fexp x + Fexp y)*(3*/4))%R;[right; ring|idtac]. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. assert (0<4)%R. auto with real. apply Rmult_le_reg_l with (4%R); auto with real. apply Rle_trans with 3%R;[right; field|idtac]; auto with real. apply Rle_trans with 4%R; auto with real. apply Rle_trans with (powerRZ radix (t + s + Fexp x + Fexp y) + powerRZ radix (t +1+ Fexp x + Fexp y) + powerRZ radix (2 * s + Fexp x + Fexp y))%R. apply Rplus_le_compat_r; apply Rplus_le_compat_l. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. apply Rle_trans with (powerRZ radix (t + s + Fexp x + Fexp y) + powerRZ radix (t+1 + Fexp x + Fexp y+1))%R. rewrite Rplus_assoc; apply Rplus_le_compat_l. apply powerRZSumRle; auto with zarith. apply Rle_trans with (powerRZ radix (t + s + Fexp x + Fexp y+1)). apply powerRZSumRle; auto with zarith. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz