proposition: Theorem EvenClosestUniqueP : UniqueP radix EvenClosest.
proof: Proof. red in |- *; simpl in |- *. intros r p q H' H'0. inversion H'; inversion H'0; case H0; case H2; auto. intros H'1 H'2; case (EvenClosestMinOrMax r p); case (EvenClosestMinOrMax r q); auto. intros H'3 H'4; apply (MinUniqueP b radix r); auto. intros H'3 H'4; case (Req_dec p q); auto; intros H'5. contradict H'1; auto. apply FnOddNEven; auto. apply FNoddEq with (f1 := FNSucc b radix precision p); auto. apply FcanonicBound with (radix := radix); auto. apply FNSuccCanonic; auto with zarith. case H'4; auto. case H'3; auto. apply (MaxUniqueP b radix r); auto. apply MinMax; auto with zarith. contradict H'5; auto. apply (RoundedProjector b radix _ (MaxRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne pGivesBound)); auto. case H'4; auto. rewrite <- H'5; auto. apply FNevenSuc; auto. case H'4; auto. intros H'3 H'4; case (Req_dec p q); auto; intros H'5. contradict H'2; auto. apply FnOddNEven; auto. apply FNoddEq with (f1 := FNSucc b radix precision q); auto. apply FcanonicBound with (radix := radix); auto. apply FNSuccCanonic; auto with zarith. case H'3; auto. case H'4; auto. apply (MaxUniqueP b radix r); auto. apply MinMax; auto with zarith. contradict H'5; auto. apply sym_eq; apply (RoundedProjector b radix _ (MaxRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne pGivesBound)); auto. case H'3; auto. rewrite <- H'5; auto. apply FNevenSuc; auto. case H'3; auto. intros H'3 H'4; apply (MaxUniqueP b radix r); auto. intros H'1 H'2; apply sym_eq; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz