proposition: Lemma xLe2y_aux1: (Rabs b <= Rabs a)%R -> (powerRZ radix (Fexp b) = Rabs (a+b))%R -> (Rabs x <= 2*Rabs y)%R.
proof: Proof. intros. apply Rle_trans with (Rabs (a+b));[right|idtac]. rewrite <- H0; unfold FtoRradix; rewrite <- Fabs_correct; auto. apply trans_eq with (FtoRradix (Float 1 (Fexp b))); [apply sym_eq |unfold FtoRradix, FtoR; simpl; ring]. apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. split; simpl. apply vNumbMoreThanOne with radix p; auto with zarith. assert (Fbounded bo b); auto with zarith. apply FcanonicBound with radix; auto. replace (FtoR radix (Float 1 (Fexp b))) with (Rabs (a+b)). apply ClosestFabs with p; auto with zarith. rewrite <- H0; unfold FtoR; simpl; ring. rewrite <- H0; apply Rmult_le_reg_l with (/2)%R; auto with real. apply Rle_trans with (Rabs y);[idtac|right; field; auto with real]. elim Evenradix; intros n Hn. apply Rle_trans with (FtoRradix (Float n ((Fexp b)-1))). right; unfold FtoRradix, FtoR; simpl. unfold Zminus; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real zarith. apply IZR_neq; auto with zarith. unfold FtoRradix; apply RoundAbsMonotonel with bo p (Closest bo radix) (a+b+e)%R; auto with real zarith. apply ClosestRoundedModeP with p; auto with zarith. split; simpl; auto with zarith. rewrite pGivesBound; apply Z.lt_trans with (Zpower_nat radix 1); auto with zarith. unfold Zpower_nat; simpl; rewrite Z.abs_eq; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. replace (a+b+e)%R with ((a+b)-(-e))%R;[idtac|ring]. apply Rle_trans with (Rabs (a+b)-Rabs (-e))%R;[idtac|apply Rabs_triang_inv]. apply Rle_trans with (powerRZ radix (Fexp b)-/2*(powerRZ radix (Fexp b)))%R. right; unfold FtoRradix, FtoR; simpl. unfold Zminus; rewrite powerRZ_add; try apply IZR_neq;auto with real zarith; simpl. ring_simplify (radix*1)%R; rewrite Hn; repeat rewrite mult_IZR; simpl; field; auto with real zarith. apply IZR_neq; auto with zarith. unfold Rminus; apply Rplus_le_compat; auto with real. apply Ropp_le_contravar; rewrite Rabs_Ropp. apply Rle_trans with (1:=eLeb); right. unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real. Qed.
imports: Reals ZArith List PeanoNat Psatz