proposition: Theorem div2IsBetweenPos : forall p min max : float, (0 <= p)%R -> 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 P H' H'0 H'1; apply Rle_antisym. apply Rplus_le_reg_l with (r := (- max)%R). replace (- max + p)%R with (p - max)%R; [ idtac | ring ]. replace (- max + (min + max))%R with (FtoRradix min); [ idtac | ring ]. rewrite <- (Fminus_correct radix); auto with arith. case H'0. intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3; auto. apply Sterbenz; auto. case H'1; auto. apply Rle_trans with (FtoRradix max); auto. apply Rmult_le_reg_l with (r := 2); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l; auto with real. apply Rledouble; auto. apply Rle_trans with (FtoRradix min); auto. apply RleMinR0 with (r := (/ 2 * p)%R); auto. apply Rmult_le_reg_l with (r := 2); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l; rewrite Rmult_0_r; auto with real. apply Rle_trans with (/ 2 * p)%R; auto; apply isMax_inv1 with (1 := H'1). case H'1. intros H'3 H'6; elim H'6; intros H'7 H'8; apply H'8; clear H'6; auto. apply Rmult_le_reg_l with (r := 2%R); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l; auto with real. apply Rmult_le_reg_l with (r := (/ 2)%R); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; rewrite Rmult_1_l; auto with real. apply isMax_inv1 with (1 := H'1). rewrite Fminus_correct; auto with arith. apply Rplus_le_reg_l with (r := FtoR radix max). replace (FtoR radix max + (FtoR radix p - FtoR radix max))%R with (FtoR radix p); [ idtac | ring ]. apply Rplus_le_reg_l with (r := (- (/ 2 * p))%R). replace (- (/ 2 * p) + FtoR radix p)%R with (/ 2 * p)%R. replace (- (/ 2 * p) + (FtoR radix max + / 2 * p))%R with (FtoR radix max); [ apply isMax_inv1 with (1 := H'1) | ring ]. replace (FtoR radix p) with (2 * (/ 2 * p))%R. simpl in |- *; ring. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real. apply Rplus_le_reg_l with (r := (- min)%R). replace (- min + p)%R with (p - min)%R; [ idtac | ring ]. replace (- min + (min + max))%R with (FtoRradix max); [ idtac | ring ]. case (PminPos p min); auto. intros x H'2; elim H'2; intros H'3 H'4; elim H'4; clear H'2. case H'1. intros H'2 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto. unfold FtoRradix in H'4; rewrite H'4; auto. fold FtoRradix in |- *; apply Rplus_le_reg_l with (r := FtoRradix min). replace (min + (p - min))%R with (FtoRradix p); [ idtac | ring ]. apply Rplus_le_reg_l with (r := (- (/ 2 * p))%R). replace (- (/ 2 * p) + p)%R with (/ 2 * p)%R by field. replace (- (/ 2 * p) + (min + / 2 * p))%R with (FtoRradix min); [ apply isMin_inv1 with (1 := H'0) | ring ]. Qed.
imports: Reals ZArith List PeanoNat Psatz