proposition: Theorem tBounded: exists v:float, Fbounded bo v /\ (FtoRradix v=uh-z)%R.
proof: Proof. case Nuh; intros I1. case Nz; intros I2. case Nph; intros I3. case (Rle_or_lt 0 (a*x+b)); intros H. unfold FtoRradix; apply tBounded_aux with p a x b ph pl; auto. elim tBounded_aux with bo radix p (Fopp a) x (Fopp b) (Fopp ph) (Fopp pl) (Fopp uh) (Fopp z); auto with zarith. fold FtoRradix; intros v T; elim T; intros; clear T. exists (Fopp v); split;[apply oppBounded; auto|idtac]. unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix; rewrite H1; unfold FtoRradix; repeat rewrite Fopp_correct; ring. apply oppBounded; auto. apply oppBounded; auto. apply FcanonicFopp; auto. apply FnormalFop; auto. apply FnormalFop; auto. apply FnormalFop; auto. replace (FtoR radix (Fopp a) * FtoR radix x + FtoR radix (Fopp b))%R with (-(a*x+b))%R; [apply ClosestOpp; auto|repeat rewrite Fopp_correct; fold FtoRradix;ring]. replace (FtoR radix (Fopp a) * FtoR radix x )%R with (-(a*x))%R; [apply ClosestOpp; auto|unfold FtoRradix; repeat rewrite Fopp_correct; ring]. repeat rewrite Fopp_correct; fold FtoRradix; rewrite plDef; ring. replace (FtoR radix (Fopp ph) + FtoR radix (Fopp b) )%R with (-(ph+b))%R; [apply ClosestOpp; auto|unfold FtoRradix; repeat rewrite Fopp_correct; ring]. apply Rle_trans with (-(a*x+b))%R; auto with real. right; unfold FtoRradix; repeat rewrite Fopp_correct; ring. assert (a*x=0)%R. apply ClosestZero1 with bo radix p ph (Fmult a x); auto with zarith. rewrite Fmult_correct; fold FtoRradix; auto. exists (Fzero (-(dExp bo))); split. apply FboundedFzero; auto. unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix. replace (FtoRradix uh) with (FtoRradix b). replace (FtoRradix z) with (FtoRradix b);[ring|idtac]. unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix b) with (a*x+b)%R; auto; rewrite H; auto with real. unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix b) with (ph+b)%R; auto; rewrite I3; auto with real. exists uh; split. elim uhDef; auto. rewrite I2; simpl; ring. exists (Fopp z); split. apply oppBounded; elim zDef; auto. rewrite I1; unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix;simpl ; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz