proposition: Theorem div2IsBetween : forall p min max : float, Fbounded b p -> isMin b radix (/ 2 * p) min -> isMax b radix (/ 2 * p) max -> p = (min + max)%R :>R.
proof: Proof. intros p min max H' H'0 H'1; case (Rle_or_lt 0 p); intros H'2. apply div2IsBetweenPos; auto. cut (forall x y : R, (- x)%R = (- y)%R -> x = y); [ intros H'3; apply H'3; clear H'3 | idtac ]. replace (- (min + max))%R with (- max + - min)%R; [ idtac | ring ]. repeat rewrite <- (Fopp_correct radix); auto with zarith. apply div2IsBetweenPos; auto with zarith. rewrite (Fopp_correct radix); auto. replace 0%R with (-0)%R; try apply Rlt_le; auto with real. now apply oppBounded. replace (/ 2 * Fopp p)%R with (- (/ 2 * p))%R. apply MaxOppMin; easy. rewrite (Fopp_correct radix); auto; fold FtoRradix; ring. replace (/ 2 * Fopp p)%R with (- (/ 2 * p))%R. apply MinOppMax; easy. rewrite (Fopp_correct radix); auto; fold FtoRradix;ring. intros x y H'3; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); rewrite H'3; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz