Require Export Reals.
Require Export ZArith.
Require Export Fcore_Zaux.

Section Rmissing.

Theorem Rle_0_minus :
  ∀ x y, (x ≤ y)%R → (0 ≤ y - x)%R.

Theorem Rabs_eq_Rabs :
  ∀ x y : R,
  Rabs x = Rabs y → x = y ∨ x = Ropp y.

Theorem Rabs_minus_le:
  ∀ x y : R,
  (0 ≤ y)%R → (y ≤ 2×x)%R →
  (Rabs (x-y) ≤ x)%R.

Theorem Rplus_eq_reg_r :
  ∀ r r1 r2 : R,
  (r1 + r = r2 + r)%R → (r1 = r2)%R.

Theorem Rplus_lt_reg_l :
  ∀ r r1 r2 : R,
  (r + r1 < r + r2)%R → (r1 < r2)%R.

Theorem Rplus_lt_reg_r :
  ∀ r r1 r2 : R,
  (r1 + r < r2 + r)%R → (r1 < r2)%R.

Theorem Rplus_le_reg_r :
  ∀ r r1 r2 : R,
  (r1 + r ≤ r2 + r)%R → (r1 ≤ r2)%R.

Theorem Rmult_lt_reg_r :
  ∀ r r1 r2 : R, (0 < r)%R →
  (r1 × r < r2 × r)%R → (r1 < r2)%R.

Theorem Rmult_le_reg_r :
  ∀ r r1 r2 : R, (0 < r)%R →
  (r1 × r ≤ r2 × r)%R → (r1 ≤ r2)%R.

Theorem Rmult_lt_compat :
  ∀ r1 r2 r3 r4,
  (0 ≤ r1)%R → (0 ≤ r3)%R → (r1 < r2)%R → (r3 < r4)%R →
  (r1 × r3 < r2 × r4)%R.

Theorem Rmult_eq_reg_r :
  ∀ r r1 r2 : R, (r1 × r)%R = (r2 × r)%R →
  r ≠ 0%R → r1 = r2.

Theorem Rmult_minus_distr_r :
  ∀ r r1 r2 : R,
  ((r1 - r2) × r = r1 × r - r2 × r)%R.

Lemma Rmult_neq_reg_r: ∀ r1 r2 r3:R, (r2 × r1 ≠ r3 × r1)%R → r2 ≠ r3.

Lemma Rmult_neq_compat_r: ∀ r1 r2 r3:R, (r1 ≠ 0)%R → (r2 ≠ r3)%R
   → (r2 ×r1 ≠ r3×r1)%R.

Theorem Rmult_min_distr_r :
  ∀ r r1 r2 : R,
  (0 ≤ r)%R →
  (Rmin r1 r2 × r)%R = Rmin (r1 × r) (r2 × r).

Theorem Rmult_min_distr_l :
  ∀ r r1 r2 : R,
  (0 ≤ r)%R →
  (r × Rmin r1 r2)%R = Rmin (r × r1) (r × r2).

Lemma Rmin_opp: ∀ x y, (Rmin (-x) (-y) = - Rmax x y)%R.

Lemma Rmax_opp: ∀ x y, (Rmax (-x) (-y) = - Rmin x y)%R.

Theorem exp_le :
  ∀ x y : R,
  (x ≤ y)%R → (exp x ≤ exp y)%R.

Theorem Rinv_lt :
  ∀ x y,
  (0 < x)%R → (x < y)%R → (/y < /x)%R.

Theorem Rinv_le :
  ∀ x y,
  (0 < x)%R → (x ≤ y)%R → (/y ≤ /x)%R.

Theorem sqrt_ge_0 :
  ∀ x : R,
  (0 ≤ sqrt x)%R.

Lemma sqrt_neg : ∀ x, (x ≤ 0)%R → (sqrt x = 0)%R.

Theorem Rabs_le :
  ∀ x y,
  (-y ≤ x ≤ y)%R → (Rabs x ≤ y)%R.

Theorem Rabs_le_inv :
  ∀ x y,
  (Rabs x ≤ y)%R → (-y ≤ x ≤ y)%R.

Theorem Rabs_ge :
  ∀ x y,
  (y ≤ -x ∨ x ≤ y)%R → (x ≤ Rabs y)%R.

Theorem Rabs_ge_inv :
  ∀ x y,
  (x ≤ Rabs y)%R → (y ≤ -x ∨ x ≤ y)%R.

Theorem Rabs_lt :
  ∀ x y,
  (-y < x < y)%R → (Rabs x < y)%R.

Theorem Rabs_lt_inv :
  ∀ x y,
  (Rabs x < y)%R → (-y < x < y)%R.

Theorem Rabs_gt :
  ∀ x y,
  (y < -x ∨ x < y)%R → (x < Rabs y)%R.

Theorem Rabs_gt_inv :
  ∀ x y,
  (x < Rabs y)%R → (y < -x ∨ x < y)%R.

End Rmissing.

Section Z2R.

Fixpoint P2R (p : positive) :=
  match p with
  | xH ⇒ 1%R
  | xO xH ⇒ 2%R
  | xO t ⇒ (2 × P2R t)%R
  | xI xH ⇒ 3%R
  | xI t ⇒ (1 + 2 × P2R t)%R
  end.

Definition Z2R n :=
  match n with
  | Zpos p ⇒ P2R p
  | Zneg p ⇒ Ropp (P2R p)
  | Z0 ⇒ R0
  end.

Theorem P2R_INR :
  ∀ n, P2R n = INR (nat_of_P n).

Theorem Z2R_IZR :
  ∀ n, Z2R n = IZR n.

Theorem Z2R_opp :
  ∀ n, Z2R (-n) = (- Z2R n)%R.

Theorem Z2R_plus :
  ∀ m n, (Z2R (m + n) = Z2R m + Z2R n)%R.

Theorem minus_IZR :
  ∀ n m : Z,
  IZR (n - m) = (IZR n - IZR m)%R.

Theorem Z2R_minus :
  ∀ m n, (Z2R (m - n) = Z2R m - Z2R n)%R.

Theorem Z2R_mult :
  ∀ m n, (Z2R (m × n) = Z2R m × Z2R n)%R.

Theorem le_Z2R :
  ∀ m n, (Z2R m ≤ Z2R n)%R → (m ≤ n)%Z.

Theorem Z2R_le :
  ∀ m n, (m ≤ n)%Z → (Z2R m ≤ Z2R n)%R.

Theorem lt_Z2R :
  ∀ m n, (Z2R m < Z2R n)%R → (m < n)%Z.

Theorem Z2R_lt :
  ∀ m n, (m < n)%Z → (Z2R m < Z2R n)%R.

Theorem Z2R_le_lt :
  ∀ m n p, (m ≤ n < p)%Z → (Z2R m ≤ Z2R n < Z2R p)%R.

Theorem le_lt_Z2R :
  ∀ m n p, (Z2R m ≤ Z2R n < Z2R p)%R → (m ≤ n < p)%Z.

Theorem eq_Z2R :
  ∀ m n, (Z2R m = Z2R n)%R → (m = n)%Z.

Theorem neq_Z2R :
  ∀ m n, (Z2R m ≠ Z2R n)%R → (m ≠ n)%Z.

Theorem Z2R_neq :
  ∀ m n, (m ≠ n)%Z → (Z2R m ≠ Z2R n)%R.

Theorem Z2R_abs :
  ∀ z, Z2R (Zabs z) = Rabs (Z2R z).

End Z2R.

Section Rcompare.

Definition Rcompare x y :=
  match total_order_T x y with
  | inleft (left _) ⇒ Lt
  | inleft (right _) ⇒ Eq
  | inright _ ⇒ Gt
  end.

Inductive Rcompare_prop (x y : R) : comparison → Prop :=
  | Rcompare_Lt_ : (x < y)%R → Rcompare_prop x y Lt
  | Rcompare_Eq_ : x = y → Rcompare_prop x y Eq
  | Rcompare_Gt_ : (y < x)%R → Rcompare_prop x y Gt.

Theorem Rcompare_spec :
  ∀ x y, Rcompare_prop x y (Rcompare x y).

Global Opaque Rcompare.

Theorem Rcompare_Lt :
  ∀ x y,
  (x < y)%R → Rcompare x y = Lt.

Theorem Rcompare_Lt_inv :
  ∀ x y,
  Rcompare x y = Lt → (x < y)%R.

Theorem Rcompare_not_Lt :
  ∀ x y,
  (y ≤ x)%R → Rcompare x y ≠ Lt.

Theorem Rcompare_not_Lt_inv :
  ∀ x y,
  Rcompare x y ≠ Lt → (y ≤ x)%R.

Theorem Rcompare_Eq :
  ∀ x y,
  x = y → Rcompare x y = Eq.

Theorem Rcompare_Eq_inv :
  ∀ x y,
  Rcompare x y = Eq → x = y.

Theorem Rcompare_Gt :
  ∀ x y,
  (y < x)%R → Rcompare x y = Gt.

Theorem Rcompare_Gt_inv :
  ∀ x y,
  Rcompare x y = Gt → (y < x)%R.

Theorem Rcompare_not_Gt :
  ∀ x y,
  (x ≤ y)%R → Rcompare x y ≠ Gt.

Theorem Rcompare_not_Gt_inv :
  ∀ x y,
  Rcompare x y ≠ Gt → (x ≤ y)%R.

Theorem Rcompare_Z2R :
  ∀ x y, Rcompare (Z2R x) (Z2R y) = Zcompare x y.

Theorem Rcompare_sym :
  ∀ x y,
  Rcompare x y = CompOpp (Rcompare y x).

Theorem Rcompare_plus_r :
  ∀ z x y,
  Rcompare (x + z) (y + z) = Rcompare x y.

Theorem Rcompare_plus_l :
  ∀ z x y,
  Rcompare (z + x) (z + y) = Rcompare x y.

Theorem Rcompare_mult_r :
  ∀ z x y,
  (0 < z)%R →
  Rcompare (x × z) (y × z) = Rcompare x y.

Theorem Rcompare_mult_l :
  ∀ z x y,
  (0 < z)%R →
  Rcompare (z × x) (z × y) = Rcompare x y.

Theorem Rcompare_middle :
  ∀ x d u,
  Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2).

Theorem Rcompare_half_l :
  ∀ x y, Rcompare (x / 2) y = Rcompare x (2 × y).

Theorem Rcompare_half_r :
  ∀ x y, Rcompare x (y / 2) = Rcompare (2 × x) y.

Theorem Rcompare_sqr :
  ∀ x y,
  (0 ≤ x)%R → (0 ≤ y)%R →
  Rcompare (x × x) (y × y) = Rcompare x y.

Theorem Rmin_compare :
  ∀ x y,
  Rmin x y = match Rcompare x y with Lt ⇒ x | Eq ⇒ x | Gt ⇒ y end.

End Rcompare.

Section Rle_bool.

Definition Rle_bool x y :=
  match Rcompare x y with
  | Gt ⇒ false
  | _ ⇒ true
  end.

Inductive Rle_bool_prop (x y : R) : bool → Prop :=
  | Rle_bool_true_ : (x ≤ y)%R → Rle_bool_prop x y true
  | Rle_bool_false_ : (y < x)%R → Rle_bool_prop x y false.

Theorem Rle_bool_spec :
  ∀ x y, Rle_bool_prop x y (Rle_bool x y).

Theorem Rle_bool_true :
  ∀ x y,
  (x ≤ y)%R → Rle_bool x y = true.

Theorem Rle_bool_false :
  ∀ x y,
  (y < x)%R → Rle_bool x y = false.

End Rle_bool.

Section Rlt_bool.

Definition Rlt_bool x y :=
  match Rcompare x y with
  | Lt ⇒ true
  | _ ⇒ false
  end.

Inductive Rlt_bool_prop (x y : R) : bool → Prop :=
  | Rlt_bool_true_ : (x < y)%R → Rlt_bool_prop x y true
  | Rlt_bool_false_ : (y ≤ x)%R → Rlt_bool_prop x y false.

Theorem Rlt_bool_spec :
  ∀ x y, Rlt_bool_prop x y (Rlt_bool x y).

Theorem negb_Rlt_bool :
  ∀ x y,
  negb (Rle_bool x y) = Rlt_bool y x.

Theorem negb_Rle_bool :
  ∀ x y,
  negb (Rlt_bool x y) = Rle_bool y x.

Theorem Rlt_bool_true :
  ∀ x y,
  (x < y)%R → Rlt_bool x y = true.

Theorem Rlt_bool_false :
  ∀ x y,
  (y ≤ x)%R → Rlt_bool x y = false.

End Rlt_bool.

Section Req_bool.

Definition Req_bool x y :=
  match Rcompare x y with
  | Eq ⇒ true
  | _ ⇒ false
  end.

Inductive Req_bool_prop (x y : R) : bool → Prop :=
  | Req_bool_true_ : (x = y)%R → Req_bool_prop x y true
  | Req_bool_false_ : (x ≠ y)%R → Req_bool_prop x y false.

Theorem Req_bool_spec :
  ∀ x y, Req_bool_prop x y (Req_bool x y).

Theorem Req_bool_true :
  ∀ x y,
  (x = y)%R → Req_bool x y = true.

Theorem Req_bool_false :
  ∀ x y,
  (x ≠ y)%R → Req_bool x y = false.

End Req_bool.

Section Floor_Ceil.

Definition Zfloor (x : R) := (up x - 1)%Z.

Theorem Zfloor_lb :
  ∀ x : R,
  (Z2R (Zfloor x) ≤ x)%R.

Theorem Zfloor_ub :
  ∀ x : R,
  (x < Z2R (Zfloor x) + 1)%R.

Theorem Zfloor_lub :
  ∀ n x,
  (Z2R n ≤ x)%R →
  (n ≤ Zfloor x)%Z.

Theorem Zfloor_imp :
  ∀ n x,
  (Z2R n ≤ x < Z2R (n + 1))%R →
  Zfloor x = n.

Theorem Zfloor_Z2R :
  ∀ n,
  Zfloor (Z2R n) = n.

Theorem Zfloor_le :
  ∀ x y, (x ≤ y)%R →
  (Zfloor x ≤ Zfloor y)%Z.

Definition Zceil (x : R) := (- Zfloor (- x))%Z.

Theorem Zceil_ub :
  ∀ x : R,
  (x ≤ Z2R (Zceil x))%R.

Theorem Zceil_glb :
  ∀ n x,
  (x ≤ Z2R n)%R →
  (Zceil x ≤ n)%Z.

Theorem Zceil_imp :
  ∀ n x,
  (Z2R (n - 1) < x ≤ Z2R n)%R →
  Zceil x = n.

Theorem Zceil_Z2R :
  ∀ n,
  Zceil (Z2R n) = n.

Theorem Zceil_le :
  ∀ x y, (x ≤ y)%R →
  (Zceil x ≤ Zceil y)%Z.

Theorem Zceil_floor_neq :
  ∀ x : R,
  (Z2R (Zfloor x) ≠ x)%R →
  (Zceil x = Zfloor x + 1)%Z.

Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x.

Theorem Ztrunc_Z2R :
  ∀ n,
  Ztrunc (Z2R n) = n.

Theorem Ztrunc_floor :
  ∀ x,
  (0 ≤ x)%R →
  Ztrunc x = Zfloor x.

Theorem Ztrunc_ceil :
  ∀ x,
  (x ≤ 0)%R →
  Ztrunc x = Zceil x.

Theorem Ztrunc_le :
  ∀ x y, (x ≤ y)%R →
  (Ztrunc x ≤ Ztrunc y)%Z.

Theorem Ztrunc_opp :
  ∀ x,
  Ztrunc (- x) = Zopp (Ztrunc x).

Theorem Ztrunc_abs :
  ∀ x,
  Ztrunc (Rabs x) = Zabs (Ztrunc x).

Theorem Ztrunc_lub :
  ∀ n x,
  (Z2R n ≤ Rabs x)%R →
  (n ≤ Zabs (Ztrunc x))%Z.

Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x.

Theorem Zaway_Z2R :
  ∀ n,
  Zaway (Z2R n) = n.

Theorem Zaway_ceil :
  ∀ x,
  (0 ≤ x)%R →
  Zaway x = Zceil x.

Theorem Zaway_floor :
  ∀ x,
  (x ≤ 0)%R →
  Zaway x = Zfloor x.

Theorem Zaway_le :
  ∀ x y, (x ≤ y)%R →
  (Zaway x ≤ Zaway y)%Z.

Theorem Zaway_opp :
  ∀ x,
  Zaway (- x) = Zopp (Zaway x).

Theorem Zaway_abs :
  ∀ x,
  Zaway (Rabs x) = Zabs (Zaway x).

End Floor_Ceil.

Section Zdiv_Rdiv.

Theorem Zfloor_div :
  ∀ x y,
  y ≠ Z0 →
  Zfloor (Z2R x / Z2R y) = (x / y)%Z.

End Zdiv_Rdiv.

Section pow.

Variable r : radix.

Theorem radix_pos : (0 < Z2R r)%R.

Definition bpow e :=
  match e with
  | Zpos p ⇒ Z2R (Zpower_pos r p)
  | Zneg p ⇒ Rinv (Z2R (Zpower_pos r p))
  | Z0 ⇒ R1
  end.

Theorem Z2R_Zpower_pos :
  ∀ n m,
  Z2R (Zpower_pos n m) = powerRZ (Z2R n) (Zpos m).

Theorem bpow_powerRZ :
  ∀ e,
  bpow e = powerRZ (Z2R r) e.

Theorem bpow_ge_0 :
  ∀ e : Z, (0 ≤ bpow e)%R.

Theorem bpow_gt_0 :
  ∀ e : Z, (0 < bpow e)%R.

Theorem bpow_plus :
  ∀ e1 e2 : Z, (bpow (e1 + e2) = bpow e1 × bpow e2)%R.

Theorem bpow_1 :
  bpow 1 = Z2R r.

Theorem bpow_plus1 :
  ∀ e : Z, (bpow (e + 1) = Z2R r × bpow e)%R.

Theorem bpow_opp :
  ∀ e : Z, (bpow (-e) = /bpow e)%R.

Theorem Z2R_Zpower_nat :
  ∀ e : nat,
  Z2R (Zpower_nat r e) = bpow (Z_of_nat e).

Theorem Z2R_Zpower :
  ∀ e : Z,
  (0 ≤ e)%Z →
  Z2R (Zpower r e) = bpow e.

Theorem bpow_lt :
  ∀ e1 e2 : Z,
  (e1 < e2)%Z → (bpow e1 < bpow e2)%R.

Theorem lt_bpow :
  ∀ e1 e2 : Z,
  (bpow e1 < bpow e2)%R → (e1 < e2)%Z.

Theorem bpow_le :
  ∀ e1 e2 : Z,
  (e1 ≤ e2)%Z → (bpow e1 ≤ bpow e2)%R.

Theorem le_bpow :
  ∀ e1 e2 : Z,
  (bpow e1 ≤ bpow e2)%R → (e1 ≤ e2)%Z.

Theorem bpow_inj :
  ∀ e1 e2 : Z,
  bpow e1 = bpow e2 → e1 = e2.

Theorem bpow_exp :
  ∀ e : Z,
  bpow e = exp (Z2R e × ln (Z2R r)).

Record ln_beta_prop x := {
  ln_beta_val :> Z ;
   _ : (x ≠ 0)%R → (bpow (ln_beta_val - 1)%Z ≤ Rabs x < bpow ln_beta_val)%R
}.

Definition ln_beta :
  ∀ x : R, ln_beta_prop x.

Theorem bpow_lt_bpow :
  ∀ e1 e2,
  (bpow (e1 - 1) < bpow e2)%R →
  (e1 ≤ e2)%Z.

Theorem bpow_unique :
  ∀ x e1 e2,
  (bpow (e1 - 1) ≤ x < bpow e1)%R →
  (bpow (e2 - 1) ≤ x < bpow e2)%R →
  e1 = e2.

Theorem ln_beta_unique :
  ∀ (x : R) (e : Z),
  (bpow (e - 1) ≤ Rabs x < bpow e)%R →
  ln_beta x = e :> Z.

Theorem ln_beta_opp :
  ∀ x,
  ln_beta (-x) = ln_beta x :> Z.

Theorem ln_beta_abs :
  ∀ x,
  ln_beta (Rabs x) = ln_beta x :> Z.

Theorem ln_beta_unique_pos :
  ∀ (x : R) (e : Z),
  (bpow (e - 1) ≤ x < bpow e)%R →
  ln_beta x = e :> Z.

Theorem ln_beta_le_abs :
  ∀ x y,
  (x ≠ 0)%R → (Rabs x ≤ Rabs y)%R →
  (ln_beta x ≤ ln_beta y)%Z.

Theorem ln_beta_le :
  ∀ x y,
  (0 < x)%R → (x ≤ y)%R →
  (ln_beta x ≤ ln_beta y)%Z.

Lemma ln_beta_lt_pos :
  ∀ x y,
  (0 < x)%R → (0 < y)%R →
  (ln_beta x < ln_beta y)%Z → (x < y)%R.

Theorem ln_beta_bpow :
  ∀ e, (ln_beta (bpow e) = e + 1 :> Z)%Z.

Theorem ln_beta_mult_bpow :
  ∀ x e, x ≠ R0 →
  (ln_beta (x × bpow e) = ln_beta x + e :>Z)%Z.

Theorem ln_beta_le_bpow :
  ∀ x e,
  x ≠ R0 →
  (Rabs x < bpow e)%R →
  (ln_beta x ≤ e)%Z.

Theorem ln_beta_gt_bpow :
  ∀ x e,
  (bpow e ≤ Rabs x)%R →
  (e < ln_beta x)%Z.

Theorem ln_beta_ge_bpow :
  ∀ x e,
  (bpow (e - 1) ≤ Rabs x)%R →
  (e ≤ ln_beta x)%Z.

Theorem bpow_ln_beta_gt :
  ∀ x,
  (Rabs x < bpow (ln_beta x))%R.

Theorem bpow_ln_beta_le :
  ∀ x, (x ≠ 0)%R →
    (bpow (ln_beta x-1) ≤ Rabs x)%R.

Theorem ln_beta_le_Zpower :
  ∀ m e,
  m ≠ Z0 →
  (Zabs m < Zpower r e)%Z→
  (ln_beta (Z2R m) ≤ e)%Z.

Theorem ln_beta_gt_Zpower :
  ∀ m e,
  m ≠ Z0 →
  (Zpower r e ≤ Zabs m)%Z →
  (e < ln_beta (Z2R m))%Z.

Lemma ln_beta_mult :
  ∀ x y,
  (x ≠ 0)%R → (y ≠ 0)%R →
  (ln_beta x + ln_beta y - 1 ≤ ln_beta (x × y) ≤ ln_beta x + ln_beta y)%Z.

Lemma ln_beta_plus :
  ∀ x y,
  (0 < y)%R → (y ≤ x)%R →
  (ln_beta x ≤ ln_beta (x + y) ≤ ln_beta x + 1)%Z.

Lemma ln_beta_minus :
  ∀ x y,
  (0 < y)%R → (y < x)%R →
  (ln_beta (x - y) ≤ ln_beta x)%Z.

Lemma ln_beta_minus_lb :
  ∀ x y,
  (0 < x)%R → (0 < y)%R →
  (ln_beta y ≤ ln_beta x - 2)%Z →
  (ln_beta x - 1 ≤ ln_beta (x - y))%Z.

Lemma ln_beta_div :
  ∀ x y : R,
  (0 < x)%R → (0 < y)%R →
  (ln_beta x - ln_beta y ≤ ln_beta (x / y) ≤ ln_beta x - ln_beta y + 1)%Z.

Lemma ln_beta_sqrt :
  ∀ x,
  (0 < x)%R →
  (2 × ln_beta (sqrt x) - 1 ≤ ln_beta x ≤ 2 × ln_beta (sqrt x))%Z.

End pow.

Section Bool.

Theorem eqb_sym :
  ∀ x y, Bool.eqb x y = Bool.eqb y x.

Theorem eqb_false :
  ∀ x y, x = negb y → Bool.eqb x y = false.

Theorem eqb_true :
  ∀ x y, x = y → Bool.eqb x y = true.

End Bool.

Section cond_Ropp.

Definition cond_Ropp (b : bool) m := if b then Ropp m else m.

Theorem Z2R_cond_Zopp :
  ∀ b m,
  Z2R (cond_Zopp b m) = cond_Ropp b (Z2R m).

Theorem abs_cond_Ropp :
  ∀ b m,
  Rabs (cond_Ropp b m) = Rabs m.

Theorem cond_Ropp_Rlt_bool :
  ∀ m,
  cond_Ropp (Rlt_bool m 0) m = Rabs m.

Theorem cond_Ropp_involutive :
  ∀ b x,
  cond_Ropp b (cond_Ropp b x) = x.

Theorem cond_Ropp_even_function :
  ∀ {A : Type} (f : R → A),
  (∀ x, f (Ropp x) = f x) →
  ∀ b x, f (cond_Ropp b x) = f x.

Theorem cond_Ropp_odd_function :
  ∀ (f : R → R),
  (∀ x, f (Ropp x) = Ropp (f x)) →
  ∀ b x, f (cond_Ropp b x) = cond_Ropp b (f x).

Theorem cond_Ropp_inj :
  ∀ b x y,
  cond_Ropp b x = cond_Ropp b y → x = y.

Theorem cond_Ropp_mult_l :
  ∀ b x y,
  cond_Ropp b (x × y) = (cond_Ropp b x × y)%R.

Theorem cond_Ropp_mult_r :
  ∀ b x y,
  cond_Ropp b (x × y) = (x × cond_Ropp b y)%R.

Theorem cond_Ropp_plus :
  ∀ b x y,
  cond_Ropp b (x + y) = (cond_Ropp b x + cond_Ropp b y)%R.

End cond_Ropp.

Theorem LPO_min :
  ∀ P : nat → Prop, (∀ n, P n ∨ ¬ P n) →
  {n : nat | P n ∧ ∀ i, (i < n)%nat → ¬ P i} + {∀ n, ¬ P n}.

Theorem LPO :
  ∀ P : nat → Prop, (∀ n, P n ∨ ¬ P n) →
  {n : nat | P n} + {∀ n, ¬ P n}.

Lemma LPO_Z : ∀ P : Z → Prop, (∀ n, P n ∨ ¬P n) →
  {n : Z| P n} + {∀ n, ¬ P n}.

Ltac bpow_simplify :=
  
  repeat
    match goal with
      | |- context [(bpow _ _ × bpow _ _)] ⇒
        rewrite <- bpow_plus
      | |- context [(?X1 × bpow _ _ × bpow _ _)] ⇒
        rewrite (Rmult_assoc X1); rewrite <- bpow_plus
      | |- context [(?X1 × (?X2 × bpow _ _) × bpow _ _)] ⇒
        rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
        rewrite <- bpow_plus
    end;
  
  repeat
    match goal with
      | |- context [(bpow _ ?X)] ⇒
        progress ring_simplify X
    end;
  
  change (bpow _ 0) with 1;
  repeat
    match goal with
      | |- context [(_ × 1)] ⇒
        rewrite Rmult_1_r
    end.