proposition: Theorem eqExpMax : forall (b : Fbound) (p q : float), Fbounded b p -> Fbounded b q -> (Fabs p <= q)%R -> exists r : float, Fbounded b r /\ r = p :>R /\ (Fexp r <= Fexp q)%Z.
proof: Proof. intros b p q H' H'0 H'1; case (Zle_or_lt (Fexp p) (Fexp q)); intros Rl0. exists p; auto. cut ((Fexp p - Z.abs_nat (Fexp p - Fexp q))%Z = Fexp q); [ intros Eq1 | idtac ]. exists (Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p); split; split; auto. apply Z.le_lt_trans with (Fnum q); try apply H'0. replace (Z.abs (Fnum (Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p))) with (Fnum (Fabs (Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p))); auto. apply (Rle_Fexp_eq_Zle radix); auto with arith. rewrite Fabs_correct; auto with arith; rewrite FshiftCorrect; auto with arith; rewrite <- (Fabs_correct radix); auto with zarith. rewrite <- (Z.abs_eq (Fnum q)); try apply H'0; auto with zarith. apply (LeR0Fnum radix); auto. apply Rle_trans with (2 := H'1); auto with real. rewrite (Fabs_correct radix); auto with real zarith. apply Rabs_pos. unfold Fshift in |- *; simpl in |- *; rewrite Eq1; auto with zarith. apply H'0. unfold FtoRradix in |- *; apply FshiftCorrect; auto. unfold Fshift in |- *; simpl in |- *. rewrite Eq1; auto with zarith. rewrite inj_abs; auto with zarith; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz