proposition: Theorem plusExpBound : forall P, RoundedModeP b radix P -> forall p q pq : float, P (p + q)%R pq -> Fbounded b p -> Fbounded b q -> exists r : float, Fbounded b r /\ r = pq :>R /\ (Z.min (Fexp p) (Fexp q) <= Fexp r)%Z /\ (Fexp r <= Z.succ (Zmax (Fexp p) (Fexp q)))%Z.
proof: Proof. intros P H' p q pq H'0 H'1 H'2. case (plusExpMin P H' _ _ _ H'0). intros r' H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7; clear H'5 H'3. case (Zle_or_lt (Fexp r') (Z.succ (Zmax (Fexp p) (Fexp q)))); intros Zl1. exists r'; repeat (split; auto). case (plusExpUpperBound P H' _ _ _ H'0); auto. intros r'' H'3; elim H'3; intros H'5 H'8; elim H'8; intros H'9 H'10; clear H'8 H'3. exists (Fshift radix (Z.abs_nat (Fexp r' - Z.succ (Zmax (Fexp p) (Fexp q)))) r'); split. apply FboundedShiftLess with (n := Z.abs_nat (Fexp r' - Fexp r'')); auto. apply ZleLe; auto. repeat rewrite <- Zabs_absolu. repeat rewrite Z.abs_eq; auto with zarith. rewrite FshiftCorrectInv; auto. apply trans_eq with (FtoRradix pq); auto. apply Z.le_trans with (1 := H'10); auto with zarith. split. unfold FtoRradix in |- *; rewrite FshiftCorrect; auto. split. simpl in |- *. repeat rewrite inj_abs; auto with zarith arith. apply Z.le_trans with (Zmax (Fexp p) (Fexp q)); auto with zarith. apply Zmin_Zmax; auto. simpl in |- *. repeat rewrite inj_abs; auto with zarith arith. Qed.
imports: Reals ZArith List PeanoNat Psatz