proposition: Theorem ClosestTotal : TotalP Closest.
proof: Proof. red in |- *; intros r. case MinEx with (r := r) (3 := pGivesBound); auto with zarith. intros min H'. case MaxEx with (r := r) (3 := pGivesBound); auto with zarith. intros max H'0. cut (min <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H') ]. cut (r <= max)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'0) ]. case (Rle_or_lt (Rabs (min - r)) (Rabs (max - r))); intros H'1. exists min; split. case H'; auto. intros f H'2. case (Rle_or_lt f r); intros H'3. repeat rewrite Rabs_left1. apply Ropp_le_contravar; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. elim H'; auto. intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rle_trans with (1 := H'1). repeat rewrite Rabs_right. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. elim 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. apply Rlt_le; auto. repeat rewrite Rplus_minus; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. exists max; split. case H'0; auto. intros f H'2. case (Rle_or_lt f r); intros H'3. apply Rle_trans with (1 := Rlt_le _ _ H'1). repeat rewrite Rabs_left1. apply Ropp_le_contravar; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. elim H'; auto. intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. repeat rewrite Rabs_right; auto with real. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. elim 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. Qed.
imports: Reals ZArith List PeanoNat Psatz