proposition: Lemma xLe2y_aux2 : (Rabs b <= Rabs a)%R -> (Rabs x <= 2*Rabs y)%R.
proof: Proof. intros. assert ((a+b=0)%R \/ (powerRZ radix (Fexp b) = Rabs (a+b))%R \/ (2*powerRZ radix (Fexp b) <= Rabs (a+b))%R). unfold FtoRradix; rewrite <- Fplus_correct; auto. rewrite <- Fabs_correct; auto. unfold FtoR. replace (Fexp (Fabs (Fplus radix a b))) with (Fexp (Fplus radix a b)); auto with zarith. replace (Fexp (Fplus radix a b)) with (Fexp b). case (Zle_lt_or_eq 0 (Z.abs (Fnum (Fplus radix a b)))); auto with zarith. intros; case (Zle_lt_or_eq 1 (Z.abs (Fnum (Fplus radix a b)))); auto with zarith. right; right. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply IZR_le; generalize H1; unfold Fabs; simpl; auto with zarith. intros; right; left. generalize H1; unfold Fabs; simpl; try lia. intros H2; rewrite <- H2; simpl; ring. left; replace (Fnum (Fplus radix a b)) with 0%Z;[simpl; ring|lia]. apply sym_eq; unfold Fplus; simpl; apply Z.min_r. apply Fcanonic_Rle_Zle with radix bo p; auto with zarith. case H0;intros H1;[idtac|case H1; clear H1; intros H1]; clear H0. replace (FtoRradix x) with 0%R. rewrite Rabs_R0; apply Rmult_le_pos; auto with real. apply Rabs_pos. apply trans_eq with (FtoRradix (Float 0 (-(dExp bo)))); [unfold FtoRradix, FtoR; simpl; ring|idtac]. apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. split; simpl; auto with zarith. replace (FtoR radix (Float 0 (- dExp bo))) with (a+b)%R; auto. rewrite H1; unfold FtoR; simpl; ring. apply xLe2y_aux1; auto. generalize UnMoinsPos; intros U1. apply Rle_trans with ((Rabs (a+b))/Unmoins)%R. apply ClosestRoundeLeNormal; auto. apply Rmult_le_reg_l with Unmoins; auto with real. apply Rle_trans with (Rabs (a+b));[right; field; auto with real|idtac]. apply Rle_trans with (Rabs (a + b + e) * 4 / 3)%R. apply abeLeab; auto. assert (0 <3)%R; [apply Rlt_trans with 2%R; auto with real|idtac]. assert (0 <4)%R; [apply Rlt_trans with 3%R; auto with real|idtac]. apply Rmult_le_reg_l with (3/4)%R; [unfold Rdiv; apply Rmult_lt_0_compat; auto with real|idtac]. apply Rle_trans with (Rabs (a+b+e));[right; field; auto with real|idtac]. apply Rle_trans with ((Rabs y)*Unplus)%R. apply ClosestRoundeGeNormal; auto. apply Rle_trans with (Rabs y *(3/4*2*Unmoins))%R;[idtac|right; ring]. apply Rmult_le_compat_l; auto with real. apply Rabs_pos. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (3*Unmoins)%R;[idtac|right; field; auto with real]. unfold Unplus, Unmoins. apply Rplus_le_reg_l with (-2+3* (powerRZ radix (Z.succ (- p)) / 2))%R. ring_simplify. apply Rle_trans with (powerRZ radix 0);[idtac|simpl; auto with real]. apply Rle_trans with (powerRZ radix (3-p)); [idtac|apply Rle_powerRZ; try apply IZR_le; auto with zarith real]. apply Rle_trans with ((5/2)*(powerRZ radix (Z.succ (-p))))%R;[right; field; auto with real|idtac]. apply Rle_trans with ((radix*radix)*(powerRZ radix (Z.succ (- p))))%R. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with 4%R; auto with real zarith. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with 5%R;[simpl; right; field; auto with real|idtac]. apply Rle_trans with 8%R; [auto with real zarith|simpl; right; ring]. rewrite <- mult_IZR; apply IZR_le. apply Z.le_trans with (2*2)%Z. auto with zarith. apply Zmult_le_compat; auto with zarith. unfold Z.succ, Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. simpl; right; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz