proposition: Theorem Veltkampb': forall (f pf qf hf tf:float), (dExp b < dExp b')%Z -> (Fbounded b f) -> Closest b radix (f * (powerRZ radix s + 1)) pf -> Closest b radix (f - pf) qf -> Closest b radix (qf + pf) hf -> Closest b radix (f - hf) tf -> Closest b' radix (f * (powerRZ radix s + 1)) pf /\ Closest b' radix (f - pf) qf /\ Closest b' radix (qf + pf) hf /\ Closest b' radix (f - hf) tf.
proof: Proof. intros. split. assert (f*(powerRZ radix s + 1)= (FtoRradix (Fplus radix (Fmult f (Float 1 s)) f)))%R. unfold FtoRradix; rewrite Fplus_correct; auto; rewrite Fmult_correct; auto. unfold FtoR; simpl; ring. rewrite H5; unfold FtoRradix; apply Closestbbext with b t; auto with zarith. simpl; rewrite Z.min_r; auto with zarith; apply H0. fold FtoRradix; rewrite <- H5; auto. split. unfold FtoRradix; rewrite <- Fminus_correct; auto. apply Closestbbext with b t; auto with zarith. simpl; apply Zmin_Zle; auto with zarith; try apply H0. apply H1. rewrite Fminus_correct; auto. split. unfold FtoRradix; rewrite <- Fplus_correct; auto. apply Closestbbext with b t; auto with zarith. simpl; apply Zmin_Zle; try apply H1; apply H2. rewrite Fplus_correct; auto. unfold FtoRradix; rewrite <- Fminus_correct; auto. apply Closestbbext with b t; auto with zarith. simpl; apply Zmin_Zle; try apply H3; apply H0. rewrite Fminus_correct; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz