proposition: Theorem Underf_Err2: forall (r:R) (x1:float), vNum b=vNum b' -> (dExp b <= dExp b')%Z -> (Closest b radix r x1) -> (exists x2:float, (Underf_Err x1 x2 r (3/4)%R) /\ (Closest b' radix r x2)).
proof: Proof. intros. elim Underf_Err2_aux with r (Fnormalize radix b p x1); auto with zarith. unfold Underf_Err; intros x2 tmp; elim tmp; intros T Z; elim T; intros V1 T'; elim T'; intros V2 T''; elim T''; intros V3 V4; clear T T' T'' tmp. exists x2; split; auto. split; auto. split; auto. split; auto. replace (x1-x2)%R with (Fnormalize radix b p x1 - x2)%R; auto with real. unfold FtoRradix; rewrite FnormalizeCorrect; auto. intros; apply trans_eq with (FtoRradix (Fnormalize radix b p x1)). unfold FtoRradix; rewrite FnormalizeCorrect; auto. apply V4; auto. apply FnormalizeCanonic; auto with zarith; elim H1; auto. apply ClosestCompatible with (1:=H1); auto. rewrite <- FnormalizeCorrect with radix b p x1; auto. apply FnormalizeBounded; auto with zarith; elim H1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz