proposition: Theorem VeltkampEven: forall x p q hx:float, (Fbounded b x) -> (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p) -> (EvenClosest b radix t (x-p)%R q) -> (EvenClosest b radix t (q+p)%R hx) -> (exists hx':float, (FtoRradix hx'=hx) /\ (EvenClosest b' radix (t-s) x hx')).
proof: Proof. intros. cut (Fcanonic radix b (Fnormalize radix b t x)); [intros C|apply FnormalizeCanonic; auto with zarith]. case C; clear C; intros. generalize VeltkampEvenN; intros T. elim T with radix b s t (Fnormalize radix b t x) p q hx; auto. intros v T'; elim T'; intros ; clear T T'. rewrite FnormalizeCorrect in H5; auto. exists v; split; auto with zarith. rewrite FnormalizeCorrect; auto with real. rewrite FnormalizeCorrect; auto with real. generalize VeltkampEvenS; intros T. elim T with radix b s t (Fnormalize radix b t x) p q hx; auto; clear T. intros v T'; elim T'; intros ; clear T'. rewrite FnormalizeCorrect in H5; auto. exists v; split; auto with zarith. rewrite FnormalizeCorrect; auto with real. rewrite FnormalizeCorrect; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz