Require Import RingLike.Core.

Require Import Stdlib.Arith.Arith.
Require Import Utf8 Structures Order Add.

Section a.

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

Tactic Notation "pauto" := progress auto.
Hint Resolve rngl_le_refl : core.

Theorem rngl_add_le_mono_l :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (b ≤ c ↔ a + b ≤ a + c)%L.

Theorem rngl_add_lt_mono_l :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (b < c ↔ a + b < a + c)%L.
Theorem rngl_add_le_mono :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a ≤ b → c ≤ d → a + c ≤ b + d)%L.

Theorem rngl_add_le_mono_r :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a ≤ b ↔ a + c ≤ b + c)%L.
Theorem rngl_add_lt_mono_r :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a < b ↔ a + c < b + c)%L.

Theorem rngl_le_0_sub :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 ≤ b - a ↔ a ≤ b)%L.
Theorem rngl_lt_0_sub :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < b - a ↔ a < b)%L.
Theorem rngl_le_sub_0 :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a - b ≤ 0 ↔ a ≤ b)%L.
Theorem rngl_lt_sub_0 :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a - b < 0 ↔ a < b)%L.
Theorem rngl_opp_le_compat :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ b ↔ - b ≤ - a)%L.
Theorem rngl_opp_lt_compat :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a < b ↔ - b < - a)%L.
Theorem rngl_opp_nonneg_nonpos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 ≤ - a)%L ↔ (a ≤ 0)%L.
Theorem rngl_opp_pos_neg :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 < - a)%L ↔ (a < 0)%L.
Theorem rngl_opp_nonpos_nonneg :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (- a ≤ 0)%L ↔ (0 ≤ a)%L.
Theorem rngl_opp_neg_pos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (- a < 0 ↔ 0 < a)%L.
Theorem rngl_sub_le_mono_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (a ≤ b)%L ↔ (c - b ≤ c - a)%L.
Theorem rngl_sub_lt_mono_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (a < b)%L ↔ (c - b < c - a)%L.
Theorem rngl_sub_le_mono_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a ≤ b ↔ a - c ≤ b - c)%L.
Theorem rngl_sub_lt_mono_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (a < b)%L ↔ (a - c < b - c)%L.
Theorem rngl_le_add_le_sub_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a + b ≤ c ↔ b ≤ c - a)%L.
Theorem rngl_lt_add_lt_sub_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a + b < c ↔ b < c - a)%L.
Theorem rngl_le_add_le_sub_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a + b ≤ c ↔ a ≤ c - b)%L.

Theorem rngl_lt_add_lt_sub_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a + b < c ↔ a < c - b)%L.

Theorem rngl_le_sub_le_add_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a - b ≤ c ↔ a ≤ b + c)%L.
Theorem rngl_lt_sub_lt_add_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a - b < c ↔ a < b + c)%L.
Theorem rngl_le_sub_le_add_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a - b ≤ c ↔ a ≤ c + b)%L.

Theorem rngl_lt_sub_lt_add_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a - b < c ↔ a < c + b)%L.

Theorem rngl_add_le_lt_mono :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a ≤ b)%L → (c < d)%L → (a + c < b + d)%L.

Theorem rngl_add_lt_le_mono :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a < b)%L → (c ≤ d)%L → (a + c < b + d)%L.

Theorem rngl_le_add_l :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → b ≤ a + b)%L.

Theorem rngl_lt_add_l :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < a)%L → (b < a + b)%L.

Theorem rngl_le_add_r :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ b → a ≤ a + b)%L.

Theorem rngl_lt_add_r :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < b → a < a + b)%L.

Theorem rngl_sub_le_compat :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a ≤ b → c ≤ d → a - d ≤ b - c)%L.

Theorem rngl_sub_lt_compat :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a < b → c < d → a - d < b - c)%L.

Theorem rngl_le_sub_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ b ↔ a - b ≤ a)%L.
Theorem rngl_lt_sub_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < b ↔ a - b < a)%L.
Theorem rngl_le_opp_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (- a ≤ b ↔ 0 ≤ a + b)%L.

Theorem rngl_lt_opp_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (- a < b ↔ 0 < a + b)%L.

Theorem rngl_le_opp_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ - b ↔ a + b ≤ 0)%L.

Theorem rngl_lt_opp_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a < - b ↔ a + b < 0)%L.

Theorem rngl_le_0_add :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → 0 ≤ b → 0 ≤ a + b)%L.

Theorem rngl_lt_0_add :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < a)%L → (0 ≤ b)%L → (0 < a + b)%L.

Theorem rngl_add_lt_compat :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a < b → c < d → a + c < b + d)%L.

Theorem rngl_leb_sub_0 :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, ((a - b ≤? 0) = (a ≤? b))%L.

Theorem rngl_eq_add_0 :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → 0 ≤ b → a + b = 0 → a = 0 ∧ b = 0)%L.
Theorem rngl_mul_nat_inj_le :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 < a)%L → ∀ i j, i ≤ j ↔ (rngl_mul_nat a i ≤ rngl_mul_nat a j)%L.
Theorem rngl_mul_nat_inj_lt :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 < a)%L → ∀ i j, i < j ↔ (rngl_mul_nat a i < rngl_mul_nat a j)%L.
Theorem rngl_add_nonneg_pos :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a)%L → (0 < b)%L → (0 < a + b)%L.

Theorem rngl_add_nonpos_nonpos :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ 0 → b ≤ 0 → a + b ≤ 0)%L.

Theorem rngl_add_neg_nonpos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a < 0 → b ≤ 0 → a + b < 0)%L.

Theorem rngl_add_nonpos_neg :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ 0 → b < 0 → a + b < 0)%L.

Theorem rngl_abs_nonneg :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a, (0 ≤ rngl_abs a)%L.
Theorem rngl_abs_opp :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a, rngl_abs (- a)%L = rngl_abs a.
Theorem rngl_le_abs_diag :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (a ≤ rngl_abs a)%L.

Theorem rngl_abs_nonneg_eq :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 ≤ a)%L → rngl_abs a = a.

Theorem rngl_abs_nonpos_eq :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a : T, (a ≤ 0)%L → rngl_abs a = (- a)%L.

Theorem rngl_abs_le :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ x y, (- x ≤ y ≤ x ↔ rngl_abs y ≤ x)%L.
Theorem rngl_le_abs :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ x y, (x ≤ y ∨ x ≤ -y)%L ↔ (x ≤ rngl_abs y)%L.

Theorem rngl_abs_lt :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ x y, (- x < y < x ↔ rngl_abs y < x)%L.
Theorem rngl_abs_sub_comm :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, rngl_abs (a - b)%L = rngl_abs (b - a)%L.

Theorem rngl_abs_pos :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ x, (x ≠ 0 → 0 < rngl_abs x)%L.

Theorem rngl_abs_triangle :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (rngl_abs (a + b) ≤ rngl_abs a + rngl_abs b)%L.

Theorem rngl_leb_opp_l :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (-a ≤? b)%L = (-b ≤? a)%L.
Theorem rngl_leb_opp_r :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (a ≤? -b)%L = (b ≤? -a)%L.
Theorem rngl_leb_0_opp :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a, (0 ≤? - a)%L = (a ≤? 0)%L.

Theorem rngl_ltb_opp_l :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (-a <? b)%L = (-b <? a)%L.
Theorem rngl_ltb_opp_r :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (a <? -b)%L = (b <? -a)%L.
Theorem rngl_archimedean_ub :
  rngl_is_archimedean T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b : T, (0 < a < b)%L →
  ∃ₜ n : nat, (rngl_mul_nat a n ≤ b < rngl_mul_nat a (n + 1))%L.

Theorem rngl_archimedean :
  rngl_is_archimedean T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < a)%L → ∃ₜ n, (b < rngl_mul_nat a n)%L.

End a.

Arguments rngl_abs_nonneg_eq {T ro rp} Hop Hor a%_L.
Arguments rngl_add_le_mono_l {T ro rp} Hos Hor (a b c)%_L.
Arguments rngl_add_lt_mono_l {T ro rp} Hos Hor (a b c)%_L.
Arguments rngl_le_add_r {T ro rp} Hos Hor (a b)%_L.