rngl_is_ordered T = true

    Require Import RingLike.Core.

From Stdlib Require Import Utf8 Arith.
Require Import Structures.

Section a.

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

Definition rngl_eqb_dec a b := sumbool_of_bool (a =? b)%L.
Definition rngl_leb_dec a b := sumbool_of_bool (a ≤? b)%L.
Definition rngl_ltb_dec a b := sumbool_of_bool (a <? b)%L.

Theorem rngl_leb_neg_ltb :
  rngl_is_ordered T = true →
  ∀ a b, (a ≤? b = negb (b <? a))%L.

Theorem rngl_ltb_neg_leb :
  rngl_is_ordered T = true →
  ∀ a b, (a <? b = negb (b ≤? a))%L.

Theorem rngl_leb_le :
  ∀ a b, (a ≤? b)%L = true ↔ (a ≤ b)%L.

Theorem rngl_ltb_lt :
  ∀ a b, (a <? b)%L = true ↔ (a < b)%L.
Theorem rngl_leb_nle :
  ∀ a b, (a ≤? b)%L = false ↔ ¬ (a ≤ b)%L.
Theorem rngl_ltb_nlt :
  ∀ a b, (a <? b)%L = false ↔ ¬ (a < b)%L.
Theorem rngl_le_refl :
  rngl_is_ordered T = true →
  ∀ a, (a ≤ a)%L.

Theorem rngl_leb_refl :
  rngl_is_ordered T = true →
  ∀ a, (a ≤? a)%L = true.

Theorem rngl_le_antisymm :
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ b → b ≤ a → a = b)%L.

Theorem rngl_le_neq :
  rngl_is_ordered T = true → ∀ a b, (a < b ↔ a ≤ b ∧ a ≠ b)%L.
Theorem rngl_lt_le_incl :
  rngl_is_ordered T = true →
  ∀ a b, (a < b → a ≤ b)%L.

Theorem rngl_lt_asymm :
  rngl_is_ordered T = true →
  ∀ a b, (a < b → ¬ b < a)%L.

Theorem rngl_nle_gt :
  ∀ a b, (b < a → ¬ (a ≤ b))%L.


Theorem rngl_le_trans :
  rngl_is_ordered T = true →
   ∀ a b c : T, (a ≤ b)%L → (b ≤ c)%L → (a ≤ c)%L.

Theorem rngl_lt_trans :
  rngl_is_ordered T = true →
   ∀ a b c : T, (a < b)%L → (b < c)%L → (a < c)%L.
Theorem rngl_lt_le_trans :
  rngl_is_ordered T = true →
   ∀ a b c : T, (a < b)%L → (b ≤ c)%L → (a < c)%L.
Theorem rngl_le_lt_trans :
  rngl_is_ordered T = true →
   ∀ a b c : T, (a ≤ b)%L → (b < c)%L → (a < c)%L.
Theorem rngl_le_iff_leb_eq :
  ∀ a b c d,
  (a ≤ b ↔ c ≤ d)%L
  → ((a ≤? b) = (c ≤? d))%L.
Theorem rngl_lt_eq_cases :
  rngl_is_ordered T = true → ∀ a b : T, (a ≤ b)%L ↔ (a < b)%L ∨ a = b.
Theorem rngl_lt_irrefl :
  rngl_is_ordered T = true → ∀ a : T, ¬ (a < a)%L.

Theorem rngl_not_le :
  rngl_is_ordered T = true →
  ∀ a b, (¬ a ≤ b → a ≠ b ∧ b ≤ a)%L.

Theorem rngl_nle_gt_iff :
  rngl_is_ordered T = true →
  ∀ a b, (¬ (a ≤ b) ↔ b < a)%L.
Theorem rngl_nlt_ge :
  ∀ a b, (b ≤ a → ¬ (a < b))%L.

Theorem rngl_nlt_ge_iff :
  rngl_is_ordered T = true →
  ∀ a b, (¬ (a < b) ↔ b ≤ a)%L.
Theorem rngl_leb_gt :
  ∀ a b, (b < a → ¬ (a ≤ b))%L.

Theorem rngl_leb_gt_iff :
  rngl_is_ordered T = true →
  ∀ a b, ((a ≤? b) = false ↔ b < a)%L.
Theorem rngl_ltb_ge :
  ∀ a b, (b ≤ a → (a <? b) = false)%L.

Theorem rngl_ltb_ge_iff :
  rngl_is_ordered T = true →
  ∀ a b, ((a <? b) = false ↔ b ≤ a)%L.
Theorem rngl_eq_le_incl :
  rngl_is_ordered T = true →
  ∀ a b, a = b → (a ≤ b)%L.


Theorem rngl_min_id :
  rngl_is_ordered T = true →
  ∀ a, rngl_min a a = a.

Theorem rngl_max_id :
  rngl_is_ordered T = true →
  ∀ a, rngl_max a a = a.

Theorem rngl_min_comm :
  rngl_is_ordered T = true →
  ∀ a b, rngl_min a b = rngl_min b a.
Theorem rngl_max_comm :
  rngl_is_ordered T = true →
  ∀ a b, rngl_max a b = rngl_max b a.

Theorem rngl_min_assoc :
  rngl_is_ordered T = true →
  ∀ a b c,
  rngl_min a (rngl_min b c) = rngl_min (rngl_min a b) c.

Theorem rngl_max_assoc :
  rngl_is_ordered T = true →
  ∀ a b c,
  rngl_max a (rngl_max b c) = rngl_max (rngl_max a b) c.

Theorem rngl_min_l_iff :
  rngl_is_ordered T = true →
  ∀ a b, rngl_min a b = a ↔ (a ≤ b)%L.
Theorem rngl_min_r_iff :
  rngl_is_ordered T = true →
  ∀ a b, rngl_min a b = b ↔ (b ≤ a)%L.

Theorem rngl_max_l_iff :
  rngl_is_ordered T = true →
  ∀ a b, rngl_max a b = a ↔ (b ≤ a)%L.
Theorem rngl_max_r_iff :
  rngl_is_ordered T = true →
  ∀ a b, rngl_max a b = b ↔ (a ≤ b)%L.

Theorem rngl_min_glb_lt_iff :
  rngl_is_ordered T = true →
  ∀ a b c, (c < rngl_min a b ↔ c < a ∧ c < b)%L.

Theorem rngl_min_le_iff :
  rngl_is_ordered T = true →
  ∀ a b c, (rngl_min a b ≤ c ↔ a ≤ c ∨ b ≤ c)%L.

Theorem rngl_min_lt_iff :
  rngl_is_ordered T = true →
  ∀ a b c, (rngl_min a b < c ↔ a < c ∨ b < c)%L.

Theorem rngl_max_lt_iff :
  rngl_is_ordered T = true →
  ∀ a b c, (a < rngl_max b c ↔ a < b ∨ a < c)%L.
Theorem rngl_le_min_l :
  rngl_is_ordered T = true →
  ∀ a b, (rngl_min a b ≤ a)%L.

Theorem rngl_le_min_r :
  rngl_is_ordered T = true →
  ∀ a b, (rngl_min a b ≤ b)%L.

Theorem rngl_min_le_compat_l :
  rngl_is_ordered T = true →
  ∀ a b c, (b ≤ c → rngl_min a b ≤ rngl_min a c)%L.
Theorem rngl_le_max_l :
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ rngl_max a b)%L.

Theorem rngl_le_max_r :
  rngl_is_ordered T = true →
  ∀ a b, (b ≤ rngl_max a b)%L.

Theorem rngl_min_glb :
  ∀ a b c, (a ≤ b → a ≤ c → a ≤ rngl_min b c)%L.

Theorem rngl_min_glb_lt :
  ∀ a b c, (a < b → a < c → a < rngl_min b c)%L.

Theorem rngl_max_lub :
  ∀ a b c, (a ≤ c → b ≤ c → rngl_max a b ≤ c)%L.

Theorem rngl_max_lub_lt :
  ∀ a b c, (a < c → b < c → rngl_max a b < c)%L.


Definition rngl_compare a b :=
  if (a =? b)%L then Eq
  else if (a ≤? b)%L then Lt else Gt.

Theorem rngl_compare_eq_iff :
  rngl_has_eq_dec_or_order T = true →
  ∀ a b, rngl_compare a b = Eq ↔ a = b.
Theorem rngl_compare_lt_iff :
  rngl_is_ordered T = true →
  ∀ a b, rngl_compare a b = Lt ↔ (a < b)%L.
Theorem rngl_compare_gt_iff :
  rngl_is_ordered T = true →
  ∀ a b, rngl_compare a b = Gt ↔ (b < a)%L.
Theorem rngl_compare_le_iff :
  rngl_is_ordered T = true →
  ∀ a b, rngl_compare a b ≠ Gt ↔ (a ≤ b)%L.
Theorem rngl_compare_refl :
  rngl_has_eq_dec_or_order T = true →
  ∀ a, rngl_compare a a = Eq.

End a.

Notation "x ?= y" := (rngl_compare x y) : ring_like_scope.

Arguments rngl_eqb_dec {T ro} (a b)%_L.
Arguments rngl_le_trans {T ro rp} Hor (a b c)%_L.
Arguments rngl_le_lt_trans {T ro rp} Hor (a b c)%_L.
Arguments rngl_leb_dec {T ro} (a b)%_L.
Arguments rngl_lt_le_trans {T ro rp} Hor (a b c)%_L.
Arguments rngl_lt_trans {T ro rp} Hor (a b c)%_L.
Arguments rngl_ltb_dec {T ro} (a b)%_L.
Arguments rngl_min {T ro} (a b)%_L.
Arguments rngl_max {T ro} (a b)%_L.