proposition: Theorem plusExpMin : forall P, RoundedModeP b radix P -> forall p q pq : float, P (p + q)%R pq -> exists s : float, Fbounded b s /\ s = pq :>R /\ (Z.min (Fexp p) (Fexp q) <= Fexp s)%Z.
proof: Proof. intros P H' p q pq H'0. case (RoundedModeRep b radix precision) with (p := Fplus radix p q) (q := pq) (P := P); auto with zarith arith. rewrite Fplus_correct; auto with arith. simpl in |- *; intros x H'1. case (eqExpLess _ radixMoreThanOne b) with (p := pq) (q := Float x (Fexp (Fplus radix p q))); auto. apply (RoundedModeBounded b radix) with (P := P) (r := (p + q)%R); auto. simpl in |- *; intros x0 H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6; clear H'4 H'2. exists x0; split; [ idtac | split ]; auto. unfold FtoRradix in |- *; rewrite H'5; auto. apply le_IZR; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz