proposition: Theorem EvenClosestTotal : TotalP EvenClosest.
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'); auto ]. cut (r <= max)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'0) ]. case (Rle_or_lt (r - min) (max - r)); intros H'1. case H'1; intros H'2; auto. exists min; split. apply ClosestMin with (max := max); auto. replace (2 * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ]. apply Rminus_le; auto. replace (r + r - (min + max))%R with (r - min - (max - r))%R; [ idtac | simpl in |- *; ring ]. apply Rle_minus; auto. right; intros q H'3. apply ClosestMinEq with (r := r) (max := max); auto. replace (2 * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ]. apply Rminus_lt; auto. replace (r + r - (min + max))%R with (r - min - (max - r))%R; [ idtac | simpl in |- *; ring ]. apply Rlt_minus; auto. case (FNevenOrFNodd b radix precision min); intros Ev0. exists min; split; auto. apply ClosestMin with (max := max); auto. replace (2 * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ]. apply Rminus_le; auto. replace (r + r - (min + max))%R with (r - min - (max - r))%R; [ idtac | simpl in |- *; ring ]. apply Rle_minus; auto. exists max; split; auto. apply ClosestMax with (min := min); auto. replace (2 * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ]. apply Rminus_le; auto. replace (min + max - (r + r))%R with (max - r - (r - min))%R; [ idtac | simpl in |- *; ring ]. apply Rle_minus; auto. rewrite H'2; auto with real. case (Req_dec min max); intros H'5. right; intros q H'3. case (ClosestMinOrMax _ _ H'3); intros isM0. rewrite <- H'5. apply MinEq with (1 := isM0); auto. apply MaxEq with (1 := isM0); auto. left. apply FNevenEq with (f1 := FNSucc b radix precision min); auto. apply FcanonicBound with (radix := radix). apply FNSuccCanonic; auto with zarith. case H'; auto. case H'0; auto. apply MaxEq with (b := b) (r := r); auto. apply MinMax; auto with zarith. contradict H'5; auto. fold FtoRradix in H'5; rewrite H'5 in H'2. replace (FtoRradix max) with (min + (max - min))%R; [ rewrite <- H'2 | idtac ]; ring. apply FNoddSuc; auto. case H'; auto. exists max; split; auto. apply ClosestMax with (min := min); auto. replace (2 * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ]. apply Rminus_le; auto. replace (min + max - (r + r))%R with (max - r - (r - min))%R; [ idtac | simpl in |- *; ring ]. apply Rle_minus; auto with real. right; intros q H'2. apply ClosestMaxEq with (r := r) (min := min); auto. replace (2 * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ]. apply Rminus_lt; auto. replace (min + max - (r + r))%R with (max - r - (r - min))%R; [ idtac | simpl in |- *; ring ]. apply Rlt_minus; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz