proposition: Lemma VeltkampN: forall x p q hx:float, Fnormal radix b x -> (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. generalize VeltkampN_aux; intros T. elim T with x (Fnormalize radix b t p) (Fnormalize radix b t q) hx; auto; clear T. apply FnormalizeCanonic; auto with zarith; elim H0; auto. apply FnormalizeCanonic; auto with zarith; elim H1; auto. apply ClosestCompatible with (1 := H0); auto. rewrite FnormalizeCorrect; auto with real zarith. apply FnormalizeBounded; auto with zarith; elim H0; auto. apply ClosestCompatible with (1 := H1); auto. unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith. rewrite FnormalizeCorrect; auto with real zarith. apply FnormalizeBounded; auto with zarith; elim H1; auto. unfold FtoRradix; repeat rewrite FnormalizeCorrect; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz