Require Import RingLike.Core.

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

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_ord_mul_le_compat_nonneg_mul_le_compat_nonpos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  (∀ a b c d, (c ≤ a ≤ 0)%L → (d ≤ b ≤ 0)%L → (a × b ≤ c × d)%L).

Theorem rngl_mul_le_compat_nonneg :
  rngl_is_ordered T = true →
  ∀ a b c d, (0 ≤ a ≤ c)%L → (0 ≤ b ≤ d)%L → (a × b ≤ c × d)%L.

Theorem rngl_mul_le_compat_nonpos :
  rngl_is_ordered T = true →
  ∀ a b c d, (c ≤ a ≤ 0)%L → (d ≤ b ≤ 0)%L → (a × b ≤ c × d)%L.

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

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

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

Theorem rngl_mul_nonneg_nonpos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → b ≤ 0 → a × b ≤ 0)%L.

Theorem rngl_mul_nonpos_nonneg :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ 0 → 0 ≤ b → a × b ≤ 0)%L.

Theorem rngl_0_le_1 :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  (0 ≤ 1)%L.

Theorem rngl_0_lt_1 :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  (0 < 1)%L.

Theorem rngl_0_leb_1 :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  (0 ≤? 1)%L = true.

Theorem rngl_1_le_2 :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  (1 ≤ 2)%L.

Theorem rngl_0_le_2 :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  (0 ≤ 2)%L.

Theorem rngl_0_lt_2 :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  (0 < 2)%L.

Theorem rngl_2_neq_0 :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  (2 ≠ 0)%L.

Theorem rngl_0_lt_3 :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
 (0 < 3)%L.

Theorem rngl_3_neq_0 :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  (3 ≠ 0)%L.

Theorem rngl_opp_1_le_0 :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  (-1 ≤ 0)%L.

Theorem rngl_opp_1_lt_0 :
  rngl_has_opp T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  (-1 < 0)%L.

Theorem rngl_opp_1_lt_1 :
  rngl_has_opp T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  (-1 < 1)%L.

Theorem rngl_opp_1_le_1 :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  (-1 ≤ 1)%L.

Theorem rngl_mul_diag_nonneg :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  ∀ a, (0 ≤ a × a)%L.
Theorem rngl_squ_nonneg :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  ∀ a, (0 ≤ a²)%L.

Theorem rngl_squ_abs :
  rngl_has_opp T = true →
  ∀ a, rngl_squ (rngl_abs a) = rngl_squ a.

Theorem rngl_of_nat_nonneg :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  ∀ n, (0 ≤ rngl_of_nat n)%L.


Theorem rngl_of_nat_inj_le :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  ∀ i j, i ≤ j ↔ (rngl_of_nat i ≤ rngl_of_nat j)%L.

Theorem rngl_of_nat_inj_lt :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  ∀ i j, i < j ↔ (rngl_of_nat i < rngl_of_nat j)%L.

Theorem rngl_abs_1 :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  (rngl_abs 1 = 1)%L.

Theorem rngl_abs_2 :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  (rngl_abs 2 = 2)%L.

Theorem rngl_add_squ_nonneg :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (0 ≤ a² + b²)%L.

Theorem rngl_mul_le_mono_nonneg_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 ≤ a)%L → (b ≤ c)%L → (a × b ≤ a × c)%L.

Theorem rngl_mul_le_mono_nonneg_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 ≤ c → a ≤ b → a × c ≤ b × c)%L.

Theorem rngl_mul_le_mono_nonpos_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a ≤ 0)%L → (b ≤ c)%L → (a × c ≤ a × b)%L.

Theorem rngl_mul_le_mono_nonpos_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (c ≤ 0 → a ≤ b → b × c ≤ a × c)%L.

Theorem rngl_lt_mul_0_if :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (a × b < 0)%L → (a < 0 < b)%L ∨ (0 < a)%L ∧ (b < 0)%L.

Theorem rngl_pow_ge_1 :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  ∀ a n, (1 ≤ a → 1 ≤ a ^ n)%L.
Theorem rngl_pow_le_mono_l :
  rngl_has_opp_or_psub T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b n, (0 ≤ a)%L → (a ≤ b)%L → (a ^ n ≤ b ^ n)%L.

Theorem rngl_pow_le_mono_r :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a m n, (1 ≤ a)%L → m ≤ n → (a ^ m ≤ a ^ n)%L.

Theorem rngl_abs_le_squ_le :
  rngl_has_opp T = true →
  rngl_is_totally_ordered T = true →
  ∀ a b, (rngl_abs a ≤ rngl_abs b → a² ≤ b²)%L.
Theorem int_part :
  rngl_has_opp T = true →
  rngl_characteristic T ≠ 1 →
  rngl_is_totally_ordered T = true →
  rngl_is_archimedean T = true →
  ∀ a, ∃ₜ n, (rngl_of_nat n ≤ rngl_abs a < rngl_of_nat (n + 1))%L.

End a.

Arguments rngl_mul_le_mono_nonneg_r {T ro rp} Hop Hor (a b c)%_L.