proposition: Theorem ClosestMonotone : MonotoneP radix Closest.
proof: Proof. red in |- *; simpl in |- *. intros p q p' q' H' H'0 H'1. change (p' <= q')%R in |- *. case (Rle_or_lt p p'); intros Rl0. case (Rle_or_lt p q'); intros Rl1. apply Rplus_le_reg_l with (r := (- p)%R). cut (forall x y : R, (- y + x)%R = (- (y - x))%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ]. rewrite <- (Rabs_left1 (p - p')). rewrite <- (Rabs_left1 (p - q')). cut (forall x y : R, Rabs (x - y) = Rabs (y - x)); [ intros Eq0; repeat rewrite (Eq0 p); clear Eq0 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ]; auto. elim H'0; auto. intros H'2 H'3; apply H'3; auto. case H'1; auto. apply Rplus_le_reg_l with (r := FtoR radix q'). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rplus_le_reg_l with (r := FtoR radix p'). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. case (Rle_or_lt p' q); intros Rl2. apply Rplus_le_reg_l with (r := (- q)%R). cut (forall x y : R, (- y + x)%R = (- (y - x))%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ]. rewrite <- (Rabs_right (q - p')). 2: apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix p'). 2: repeat rewrite Rplus_minus; auto. 2: rewrite Rplus_0_r; auto. rewrite <- (Rabs_right (q - q')). 2: apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix q'). 2: repeat rewrite Rplus_minus; auto. 2: rewrite Rplus_0_r; auto. 2: apply Rle_trans with (1 := Rlt_le _ _ Rl1); apply Rlt_le; auto. cut (forall x y : R, Rabs (x - y) = Rabs (y - x)); [ intros Eq0; repeat rewrite (Eq0 q); clear Eq0 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ]; auto. apply Ropp_le_contravar. elim H'1; auto. intros H'2 H'3; apply H'3; auto. case H'0; auto. case (Rle_or_lt (p - q') (p' - q)); intros Rl3. absurd (Rabs (p' - p) <= Rabs (q' - p))%R. apply Rgt_not_le. rewrite (Rabs_left1 (q' - p)). 2: apply Rplus_le_reg_l with (r := p). 2: repeat rewrite Rplus_minus; auto. 2: rewrite Rplus_0_r; apply Rlt_le; auto. rewrite (Rabs_right (p' - p)). 2: apply Rle_ge; apply Rplus_le_reg_l with (r := p). 2: rewrite Rplus_0_r; auto. cut (forall x y : R, (- (y - x))%R = (x - y)%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ]. red in |- *; apply Rle_lt_trans with (1 := Rl3). replace (p' - p)%R with (p' - q + (q - p))%R. pattern (p' - q)%R at 1 in |- *; replace (p' - q)%R with (p' - q + 0)%R. apply Rplus_lt_compat_l; auto. apply Rplus_lt_reg_l with (r := p). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. rewrite Rplus_0_r; auto. ring. replace (p + (p' - p))%R with (FtoRradix p'); auto; ring. case H'0; intros H'2 H'3; apply H'3; auto. case H'1; auto. absurd (Rabs (q' - q) <= Rabs (p' - q))%R. apply Rgt_not_le. rewrite (Rabs_left1 (q' - q)). 2: apply Rplus_le_reg_l with (r := q). 2: repeat rewrite Rplus_minus; auto. 2: rewrite Rplus_0_r; apply Rlt_le; auto. 2: apply Rlt_trans with (1 := Rl1); auto. rewrite (Rabs_right (p' - q)). 2: apply Rle_ge; apply Rplus_le_reg_l with (r := q). 2: rewrite Rplus_0_r; apply Rlt_le; auto. cut (forall x y : R, (- (y - x))%R = (x - y)%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ]. red in |- *; apply Rlt_trans with (1 := Rl3). replace (q - q')%R with (p - q' + (q - p))%R. pattern (p - q')%R at 1 in |- *; replace (p - q')%R with (p - q' + 0)%R. apply Rplus_lt_compat_l; auto. apply Rplus_lt_reg_l with (r := p). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. rewrite Rplus_0_r; auto. ring. replace (q + (p' - q))%R with (FtoRradix p'); auto; ring. case H'1; intros H'2 H'3; apply H'3; auto. case H'0; auto. case (Rle_or_lt p q'); intros Rl1. apply Rle_trans with p; auto. apply Rlt_le; auto. apply Rplus_le_reg_l with (r := (- q)%R). cut (forall x y : R, (- y + x)%R = (- (y - x))%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ]. rewrite <- (Rabs_right (q - p')). rewrite <- (Rabs_right (q - q')). apply Ropp_le_contravar. cut (forall x y : R, Rabs (x - y) = Rabs (y - x)); [ intros Eq0; repeat rewrite (Eq0 q); clear Eq0 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ]; auto. elim H'1; auto. intros H'2 H'3; apply H'3; auto. case H'0; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix q'). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rlt_le; apply Rlt_trans with (1 := Rl1); auto. apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix p'). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rlt_le; apply Rlt_trans with (1 := Rl0); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz