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