proposition: Lemma VeltkampN_aux: forall x p q hx:float, Fnormal radix b x -> Fcanonic radix b p -> Fcanonic radix b q -> (Closest b radix (x*((powerRZ radix s)+1))%R p) -> (Closest b radix (x-p)%R q) -> (Closest b radix (q+p)%R hx) -> (Rabs (x-hx) <= (powerRZ radix (s+Fexp x)) /2)%R /\ (exists hx':float, (FtoRradix hx'=hx) /\ (Closest b' radix x hx') /\ (s+Fexp x <= Fexp hx')%Z).
proof: Proof. intros x p q hx Nx Cp Cq; intros. case (Rle_or_lt 0%R x); intros H2. case H2; clear H2; intros H2. apply Veltkamp_pos with p q; auto. absurd (is_Fzero x). apply FnormalNotZero with radix b; auto. apply is_Fzero_rep2 with radix; auto with real. elim Veltkamp_pos with (Fopp x) (Fopp p) (Fopp q) (Fopp hx). intros H3 T; elim T; intros v T'; elim T'; intros H4 T''; elim T''; intros ; clear T T' T''. split. unfold FtoRradix in H3; repeat rewrite Fopp_correct in H3. rewrite <- Rabs_Ropp. replace (-(x-hx))%R with (-x-(-hx))%R;[unfold FtoRradix; apply Rle_trans with (1:=H3)|ring]. unfold Fopp; auto with real. exists (Fopp v); split. unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix; rewrite H4. unfold FtoRradix; rewrite Fopp_correct; ring. split. replace (FtoRradix x) with (-(Fopp x))%R. apply ClosestOpp; auto. unfold FtoRradix; rewrite Fopp_correct; ring. unfold Fopp; unfold Fopp in H6; auto with zarith. apply FnormalFop; auto. apply FcanonicFopp; auto. apply FcanonicFopp; auto. unfold FtoRradix; rewrite Fopp_correct; auto with real. replace (Fopp x * (powerRZ radix s + 1))%R with (-(x * (powerRZ radix s + 1)))%R. apply ClosestOpp; auto. unfold FtoRradix; rewrite Fopp_correct; ring. replace (Fopp x - Fopp p)%R with (-(x-p))%R;[apply ClosestOpp; auto|idtac]. unfold FtoRradix; repeat rewrite Fopp_correct; ring. replace (Fopp q + Fopp p)%R with (-(q+p))%R;[apply ClosestOpp; auto|idtac]. unfold FtoRradix; repeat rewrite Fopp_correct; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz