proposition: Lemma yLe2x_aux : (Rabs b <= Rabs a)%R -> ~(FtoRradix x=0)%R -> (Rabs y <= 2*Rabs x)%R.
proof: Proof. intros. assert ((a+b=0)%R \/ (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; right. apply Rle_trans with (1%Z*(powerRZ radix (Fexp b)))%R;[right; simpl; ring|idtac]. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply IZR_le; generalize H1; simpl; lia. intros; 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 H1;intros H2; clear H1. absurd (FtoRradix x=0)%R; auto with real. apply sym_eq; 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 H2; unfold FtoR; simpl; ring. generalize UnMoinsPos; intros U1. apply Rle_trans with ((Rabs (a+b+e))/Unmoins)%R. apply ClosestRoundeLeNormal; auto. apply Rmult_le_reg_l with Unmoins; auto with real. apply Rle_trans with (Rabs (a+b+e));[right; field; auto with real|idtac]. apply Rle_trans with (Rabs (a + b) * 3 / 2)%R. apply Rle_trans with (Rabs (a+b)+Rabs e)%R;[apply Rabs_triang|idtac]. apply Rle_trans with (Rabs (a + b) + Rabs (a + b) /2)%R; [apply Rplus_le_compat_l|right; field; auto with real]. apply Rle_trans with (1:=eLeb); unfold Rdiv; rewrite Rmult_comm. apply Rmult_le_compat_r; auto with real. unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real. assert (0 <3)%R; [apply Rlt_trans with 2%R; auto with real|idtac]. apply Rmult_le_reg_l with (2/3)%R; [unfold Rdiv; apply Rmult_lt_0_compat; auto with real|idtac]. apply Rle_trans with (Rabs (a+b));[right; field; apply prod_neq_R0; auto with real|idtac]. apply Rle_trans with ((Rabs x)*Unplus)%R. apply ClosestRoundeGeNormal; auto. apply Rle_trans with (Rabs x *(2/3*2*Unmoins))%R;[idtac|right; ring]. apply Rmult_le_compat_l; auto with real. apply Rabs_pos. apply Rmult_le_reg_l with 3%R; auto with real. apply Rle_trans with (4*Unmoins)%R;[idtac|right; field; auto with real]. unfold Unplus, Unmoins. apply Rplus_le_reg_l with (-3+4* (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; auto with zarith real]. apply Rle_trans with ((7/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 7%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; auto with real zarith. simpl; right; field. apply IZR_neq; lia. apply IZR_neq; lia. apply IZR_le; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz