From Stdlib Require Import Utf8 Arith.

Require Import Core.
Require Import RealLike.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context {rl : real_like_prop T}.

Context {Hop : rngl_has_opp T = true}.
Context {Hor : rngl_is_ordered T = true}.

Theorem rngl_dist_mul_distr_r :
  rngl_has_inv_or_pdiv T = true →
  ∀ a b c,
  (0 ≤ c)%L → (rngl_dist a b × c = rngl_dist (a × c) (b × c))%L.

Definition is_limit_when_tending_to_neighbourhood_le (is_left : bool) {A B}
  (lt : A → A → Prop) (da : A → A → T) (db : B → B → T)
  (f : A → B) (x₀ : A) (L : B) :=
  (∀ ε : T, 0 < ε →
   ∃ η : T, (0 < η)%L ∧ ∀ x : A,
   (if is_left then lt x x₀ else lt x₀ x)
   → da x x₀ < η
   → db (f x) L ≤ ε)%L.

Theorem is_limit_lt_is_limit_le_iff :
  rngl_has_inv T = true →
  ∀ is_left {A B} lt da db (f : A → B) x₀ L,
  is_limit_when_tending_to_neighbourhood is_left lt da db f x₀ L
  ↔ is_limit_when_tending_to_neighbourhood_le is_left lt da db f x₀ L.
Theorem left_or_right_derivable_continuous_when_derivative_eq_0 :
  rngl_has_inv T = true →
  ∀ is_left A lt,
  (∀ x, ¬ (lt x x))
  → ∀ {da} (dist : is_dist da) (f : A → T) x,
  left_or_right_derivative_at is_left lt da rngl_dist f x 0%L
  → left_or_right_continuous_at is_left lt da rngl_dist f x.
Theorem left_or_right_derivable_continuous :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ is_left A lt, (∀ x, ¬ (lt x x)) →
  ∀ {da} (dist : is_dist da) (f : A → T) x a,
  left_or_right_derivative_at is_left lt da rngl_dist f x a
  → left_or_right_continuous_at is_left lt da rngl_dist f x.
Theorem dist_comm : ∀ A (d : distance A) x y, d_dist x y = d_dist y x.


Theorem left_or_right_derivative_mul_at :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ is_left A lt, (∀ x, ¬ (lt x x)) →
  ∀ {da} (dist : is_dist da) (f g : A → T) u v x₀,
  left_or_right_derivative_at is_left lt da rngl_dist f x₀ u
  → left_or_right_derivative_at is_left lt da rngl_dist g x₀ v
  → left_or_right_derivative_at is_left lt da rngl_dist
       (λ x : A, (f x × g x)%L) x₀ (f x₀ × v + u × g x₀)%L.
Theorem left_or_right_continuous_lower_bounded :
  rngl_has_inv T = true →
  ∀ is_left {A} (da : A → A → T) le f x₀,
  left_or_right_continuous_at is_left le da rngl_dist f x₀
  → f x₀ ≠ 0%L
  → ∃ δ,
    (0 < δ)%L ∧ ∀ x,
    (if is_left then le x x₀ else le x₀ x)
    → (da x x₀ < δ)%L
    → (rngl_abs (f x₀) / 2 < rngl_abs (f x))%L.

Theorem left_or_right_continuous_upper_bounded :
  rngl_characteristic T ≠ 1 →
  ∀ is_left {A} (da : A → A → T) le f x₀ u,

  is_limit_when_tending_to_neighbourhood is_left le da rngl_dist f x₀ u
  → ∃ δ M,
    (0 < δ)%L ∧ (0 < M)%L ∧ ∀ x,
    (if is_left then le x x₀ else le x₀ x)
    → (da x x₀ < δ)%L
    → (rngl_abs (f x) < M)%L.

Theorem left_or_right_continuous_mul_at :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ is_left A le da (f g : A → T) x₀ u v,
  is_limit_when_tending_to_neighbourhood is_left le da rngl_dist f x₀ u
  → is_limit_when_tending_to_neighbourhood is_left le da rngl_dist g x₀ v
  → is_limit_when_tending_to_neighbourhood is_left le da rngl_dist
       (λ x : A, (f x × g x)%L) x₀ (u × v)%L.

Theorem left_or_right_continuous_inv :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ is_left A le (da : A → A → T) f x₀,
  f x₀ ≠ 0%L
  → left_or_right_continuous_at is_left le da rngl_dist f x₀
  → left_or_right_continuous_at is_left le da rngl_dist
      (λ x, (f x)⁻¹) x₀.
Theorem rngl_abs_inv :
  rngl_has_inv T = true →
  ∀ a, a ≠ 0%L → (rngl_abs a⁻¹ = (rngl_abs a)⁻¹)%L.

Theorem left_or_right_derivative_inv :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ {A} lt is_left (da : A → A → T) f f' x₀,
  f x₀ ≠ 0%L
  → left_or_right_continuous_at is_left lt da rngl_dist f x₀
  → left_or_right_derivative_at is_left lt da rngl_dist f x₀ (f' x₀)
  → left_or_right_derivative_at is_left lt da rngl_dist (λ x : A, (f x)⁻¹)
      x₀ (- f' x₀ / (f x₀)²)%L.


Theorem derivative_mul_at :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ A lt, (∀ x, ¬ (lt x x)) →
  ∀ {da} (dist : is_dist da) (f g : A → T) f' g' x₀,
  is_derivative_at lt da rngl_dist f f' x₀
  → is_derivative_at lt da rngl_dist g g' x₀
  → is_derivative_at lt da rngl_dist (λ x : A, (f x × g x)%L)
       (λ x, f x × g' x + f' x × g x)%L x₀.
Theorem derivative_mul :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ A lt, (∀ x, ¬ (lt x x)) →
  ∀ {da} (dist : is_dist da) (f g : A → T) f' g',
  is_derivative lt da rngl_dist f f'
  → is_derivative lt da rngl_dist g g'
  → is_derivative lt da rngl_dist (λ x : A, (f x × g x)%L)
       (λ x, f x × g' x + f' x × g x)%L.

Theorem derivative_inv_at :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ A lt, (∀ x, ¬ (lt x x)) →
  ∀ da (f : A → T) f' x₀,
  f x₀ ≠ 0%L
  → is_derivative_at lt da rngl_dist f f' x₀
  → is_derivative_at lt da rngl_dist (λ x : A, (f x)⁻¹)
       (λ x, (- f' x / rngl_squ (f x))%L) x₀.
End a.