orders.rings

Require Import
  Relation_Definitions Ring
  abstract_algebra interfaces.orders theory.rings.
Require Export
  orders.semirings.

Section from_ring_order.
  Context `{Ring R} `{!PartialOrder Rle}
    (plus_spec : z, OrderPreserving (z +))
    (mult_spec : x y, PropHolds (0 x) PropHolds (0 y) PropHolds (0 x * y)).

  Lemma from_ring_order: SemiRingOrder (≤).
End from_ring_order.

Section from_strict_ring_order.
  Context `{Ring R} `{!StrictSetoidOrder Rle}
    (plus_spec : z, StrictlyOrderPreserving (z +))
    (mult_spec : x y, PropHolds (0 < x) PropHolds (0 < y) PropHolds (0 < x * y)).

  Lemma from_strict_ring_order: StrictSemiRingOrder (<).
End from_strict_ring_order.

Section from_pseudo_ring_order.
  Context `{Ring R} `{Apart R} `{!PseudoOrder Rlt}
    (plus_spec : z, StrictlyOrderPreserving (z +))
    (mult_ext : StrongSetoid_BinaryMorphism (.*.))
    (mult_spec : x y, PropHolds (0 < x) PropHolds (0 < y) PropHolds (0 < x * y)).

  Lemma from_pseudo_ring_order: PseudoSemiRingOrder (<).
End from_pseudo_ring_order.

Section from_full_pseudo_ring_order.
  Context `{Ring R} `{Apart R} `{!FullPseudoOrder Rle Rlt}
    (plus_spec : z, StrictlyOrderPreserving (z +))
    (mult_ext : StrongSetoid_BinaryMorphism (.*.))
    (mult_spec : x y, PropHolds (0 < x) PropHolds (0 < y) PropHolds (0 < x * y)).

  Lemma from_full_pseudo_ring_order: FullPseudoSemiRingOrder (≤) (<).
End from_full_pseudo_ring_order.

Section ring_order.
  Context `{Ring R} `{!SemiRingOrder Rle}.
  Add Ring R : (stdlib_ring_theory R).

  Lemma flip_le_opp x y : -y -x x y.

  Lemma flip_nonneg_opp x : 0 x -x 0.

  Lemma flip_nonpos_opp x : x 0 0 -x.

  Lemma flip_le_minus_r (x y z : R) : z y - x z + x y.

  Lemma flip_le_minus_l (x y z : R) : y - x z y z + x.

  Lemma flip_nonneg_minus (x y : R) : 0 y - x x y.

  Lemma flip_nonpos_minus (x y : R) : y - x 0 y x.

  Lemma nonneg_minus_compat (x y z : R) : 0 z x y x - z y.

  Lemma nonneg_minus_compat_back (x y z : R) : 0 z x y - z x y.

  Lemma between_nonneg (x : R) : 0 x -x x.
End ring_order.

Section strict_ring_order.
  Context `{Ring R} `{!StrictSemiRingOrder Rlt}.
  Add Ring Rs : (stdlib_ring_theory R).

  Lemma flip_lt_opp x y : -y < -x x < y.

  Lemma flip_pos_opp x : 0 < x -x < 0.

  Lemma flip_neg_opp x : x < 0 0 < -x.

  Lemma flip_lt_minus_r (x y z : R) : z < y - x z + x < y.

  Lemma flip_lt_minus_l (x y z : R) : y - x < z y < z + x.

  Lemma flip_pos_minus (x y : R) : 0 < y - x x < y.

  Lemma flip_neg_minus (x y : R) : y - x < 0 y < x.

  Lemma pos_minus_compat (x y z : R) : 0 < z x < y x - z < y.

  Lemma between_pos (x : R) : 0 < x -x < x.
End strict_ring_order.

Section another_ring_order.
  Context `{Ring R1} `{!SemiRingOrder R1le} `{Ring R2} `{R2le : Le R2}.

  Lemma projected_ring_order (f : R2 R1) `{!SemiRing_Morphism f} `{!Injective f} `{!OrderEmbedding f} :
    SemiRingOrder R2le.

  Context `{!SemiRingOrder R2le} {f : R1 R2} `{!SemiRing_Morphism f}.

  Lemma preserving_back_preserves_nonneg : ( x, 0 f x 0 x) OrderPreservingBack f.

  Lemma preserves_ge_opp1 `{!OrderPreserving f} x : -1 x -1 f x.

  Lemma preserves_le_opp1 `{!OrderPreserving f} x : x -1 f x -1.
End another_ring_order.

Section another_strict_ring_order.
  Context `{Ring R1} `{!StrictSemiRingOrder R1lt} `{Ring R2} `{R2lt : Lt R2}.

  Lemma projected_strict_ring_order (f : R2 R1) `{!SemiRing_Morphism f} `{!StrictOrderEmbedding f} :
    StrictSemiRingOrder R2lt.
End another_strict_ring_order.

Section another_pseudo_ring_order.
  Context `{Ring R1} `{Apart R1} `{!PseudoSemiRingOrder R1lt}
    `{Ring R2} `{Apart R2} `{R2lt : Lt R2}.

  Lemma projected_pseudo_ring_order (f : R2 R1) `{!SemiRing_Morphism f} `{!StrongInjective f}
    `{!StrictOrderEmbedding f} : PseudoSemiRingOrder R2lt.
End another_pseudo_ring_order.

Section another_full_pseudo_ring_order.
  Context `{Ring R1} `{Apart R1} `{!FullPseudoSemiRingOrder R1le R1lt}
    `{Ring R2} `{Apart R2} `{R2le : Le R2} `{R2lt : Lt R2}.

  Lemma projected_full_pseudo_ring_order (f : R2 R1) `{!SemiRing_Morphism f} `{!StrongInjective f}
    `{!StrictOrderEmbedding f} `{!OrderEmbedding f} : FullPseudoSemiRingOrder R2le R2lt.
End another_full_pseudo_ring_order.