proposition: Lemma x2y1Le: (Rabs (x2*y1) < (powerRZ radix (t+s+Fexp x+Fexp y)) /2 + (powerRZ radix (2*s+Fexp x+Fexp y)) /4)%R.
proof: Proof. replace (x2*y1)%R with (x2*y+(-(x2*y2)))%R;[idtac|rewrite Yeq; ring]. apply Rle_lt_trans with (1:=Rabs_triang (x2*y)%R (-(x2*y2))%R). rewrite Rabs_Ropp. cut ((Rabs (x2 * y) < powerRZ radix (t + s + Fexp x + Fexp y) / 2))%R;[intros I1|idtac]. generalize x2y2Le; auto with real. rewrite Rabs_mult. apply Rlt_le_trans with ((powerRZ radix (s + Fexp x) / 2)*powerRZ radix (t+Fexp y))%R. cut (Rabs y <powerRZ radix (t + Fexp y))%R; auto with real zarith. intros I; apply Rle_lt_trans with (powerRZ radix (s + Fexp x) / 2 *Rabs y)%R; auto with real. apply Rmult_le_compat; try apply Rabs_pos; auto with real. apply Rmult_lt_compat_l; auto with real zarith. unfold Rdiv; apply Rmult_lt_0_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith. unfold FtoR, Fabs; simpl; rewrite powerRZ_add. apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. elim Ny; intros I1 I2; elim I1; intros. apply Rlt_le_trans with (IZR (Zpos (vNum b))); try apply IZR_lt; auto with real zarith. right; rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto with real. apply IZR_neq; lia. repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. unfold Rdiv; right; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz