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.