proposition: Theorem ClosestSymmetric : SymmetricP Closest.
proof: Proof. red in |- *; intros r p H'; case H'; clear H'. intros H' H'0; split. apply oppBounded; auto. intros f H'1. replace (Rabs (Fopp p - - r)) with (Rabs (p - r)). replace (Rabs (f - - r)) with (Rabs (Fopp f - r)). apply H'0; auto. apply oppBounded; auto. unfold FtoRradix in |- *; rewrite Fopp_correct. pattern r at 1 in |- *; replace r with (- - r)%R; [ idtac | ring ]. replace (- FtoR radix f - - - r)%R with (- (FtoR radix f - - r))%R; [ idtac | ring ]. apply Rabs_Ropp; auto. unfold FtoRradix in |- *; rewrite Fopp_correct. replace (- FtoR radix p - - r)%R with (- (FtoR radix p - r))%R; [ idtac | ring ]. apply sym_eq; apply Rabs_Ropp. Qed.
imports: Reals ZArith List PeanoNat Psatz