proposition: Theorem ClosestMax : forall (r : R) (min max : float), isMin b radix r min -> isMax b radix r max -> (min + max <= 2 * r)%R -> Closest r max.
proof: Proof. intros r min max H' H'0 H'1; split. case H'0; auto. intros f H'2. case (Rle_or_lt f r); intros H'3. rewrite (Rabs_right (max - r)). rewrite (Rabs_left1 (f - r)). apply Rle_trans with (r - min)%R. apply Rplus_le_reg_l with (r := FtoRradix min). repeat rewrite Rplus_minus; auto. apply Rplus_le_reg_l with (r := r). replace (r + (min + (max - r)))%R with (min + max)%R. replace (r + r)%R with (2 * r)%R; auto. simpl in |- *; ring. simpl in |- *; ring. replace (r - min)%R with (- (min - r))%R. apply Ropp_le_contravar. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. case H'; auto. intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto. simpl in |- *; ring. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply isMax_inv1 with (1 := H'0); auto. repeat rewrite Rabs_right. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. case H'0; auto. intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto. apply Rlt_le; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rlt_le; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply isMax_inv1 with (1 := H'0); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz