proposition: Theorem EvenClosestSymmetric : SymmetricP EvenClosest.
proof: Proof. red in |- *; intros r p H'; case H'; clear H'. intros H' H'0; case H'0; clear H'0; intros H'0. split; auto. apply (ClosestSymmetric r p); auto. left. apply FNevenFop; auto. split; auto. apply (ClosestSymmetric r p); auto. right. intros q H'1. cut (Fopp q = p :>R). intros H'2; unfold FtoRradix in |- *; rewrite Fopp_correct. unfold FtoRradix in H'2; rewrite <- H'2. rewrite Fopp_correct; ring. apply H'0; auto. replace r with (- - r)%R; [ idtac | ring ]. apply (ClosestSymmetric (- r)%R q); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz