rings.v

Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.theory.groups
  HoTT.Classes.theory.rings.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export
  HoTT.Classes.orders.semirings.

Generalizable Variables R Rle Rlt R1le R1lt.

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

  Lemma from_ring_order: SemiRingOrder (≤).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
SemiRingOrder le
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
SemiRingOrder le
  repeat (split; try exact _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
forall x y : R, x ≤ y -> {z : R & y = x + z}
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
z: R
OrderReflecting (plus z)
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
forall x y : R, x ≤ y -> {z : R & y = x + z} intros x y E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
x, y: R
E: x ≤ y
{z : R & y = x + z} exists (- x + y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
x, y: R
E: x ≤ y
y = x + (- x + y)
    rewrite simple_associativity, plus_negate_r, plus_0_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
x, y: R
E: x ≤ y
y = y
    reflexivity.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
z: R
OrderReflecting (plus z) intros x y E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
z, x, y: R
E: z + x ≤ z + y
x ≤ y
    rewrite <-(plus_0_l x), <-(plus_0_l y), <-!(plus_negate_l z),
      <-!simple_associativity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
z, x, y: R
E: z + x ≤ z + y
- z + (z + x) ≤ - z + (z + y)
    apply (order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
PartialOrder0: PartialOrder Rle
plus_spec: forall z : R, OrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 ≤ x) ->
PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
z, x, y: R
E: z + x ≤ z + y
z + x ≤ z + y trivial.
  Qed.
End from_ring_order.

Section from_strict_ring_order.
  Context `{IsCRing R} `{!StrictOrder Rlt}
    (plus_spec : forall z, StrictlyOrderPreserving (z +))
    (mult_spec : forall x y, PropHolds (0 < x) -> PropHolds (0 < y) ->
      PropHolds (0 < x * y)).

  Lemma from_strict_ring_order: StrictSemiRingOrder (<).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
StrictSemiRingOrder lt
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
StrictSemiRingOrder lt
  repeat (split; try exact _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
forall x y : R, x < y -> {z : R & y = x + z}
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z: R
StrictlyOrderReflecting (plus z)
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
forall x y : R, x < y -> {z : R & y = x + z} intros x y E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
x, y: R
E: x < y
{z : R & y = x + z} exists (- x + y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
x, y: R
E: x < y
y = x + (- x + y)
    rewrite simple_associativity, plus_negate_r, plus_0_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
x, y: R
E: x < y
y = y
    reflexivity.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z: R
StrictlyOrderReflecting (plus z) intros x y E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z, x, y: R
E: z + x < z + y
x < y
    rewrite <-(plus_0_l x), <-(plus_0_l y), <-!(plus_negate_l z),
      <-!simple_associativity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z, x, y: R
E: z + x < z + y
- z + (z + x) < - z + (z + y)
    apply (strictly_order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictOrder0: StrictOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z, x, y: R
E: z + x < z + y
z + x < z + y trivial.
  Qed.
End from_strict_ring_order.

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

  Lemma from_pseudo_ring_order: PseudoSemiRingOrder (<).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
PseudoSemiRingOrder lt
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
PseudoSemiRingOrder lt
  repeat (split; try exact _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
forall x y : R, ~ (y < x) -> {z : R & y = x + z}
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z: R
StrictlyOrderReflecting (plus z)
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
forall x y : R, ~ (y < x) -> {z : R & y = x + z} intros x y E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
x, y: R
E: ~ (y < x)
{z : R & y = x + z} exists (- x + y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
x, y: R
E: ~ (y < x)
y = x + (- x + y)
    rewrite simple_associativity, plus_negate_r, plus_0_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
x, y: R
E: ~ (y < x)
y = y
    reflexivity.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z: R
StrictlyOrderReflecting (plus z) intros x y E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z, x, y: R
E: z + x < z + y
x < y
    rewrite <-(plus_0_l x), <-(plus_0_l y), <-!(plus_negate_l z),
      <-!simple_associativity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z, x, y: R
E: z + x < z + y
- z + (z + x) < - z + (z + y)
    apply (strictly_order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rlt: Lt R
PseudoOrder0: PseudoOrder Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
z, x, y: R
E: z + x < z + y
z + x < z + y
    trivial.
  Qed.
End from_pseudo_ring_order.

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

  Lemma from_full_pseudo_ring_order: FullPseudoSemiRingOrder (≤) (<).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoOrder0: FullPseudoOrder Rle Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
FullPseudoSemiRingOrder le lt
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoOrder0: FullPseudoOrder Rle Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
FullPseudoSemiRingOrder le lt
  split.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoOrder0: FullPseudoOrder Rle Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
is_mere_relation R le
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoOrder0: FullPseudoOrder Rle Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
PseudoSemiRingOrder lt
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoOrder0: FullPseudoOrder Rle Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
forall x y : R, x ≤ y <-> ~ (y < x)
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoOrder0: FullPseudoOrder Rle Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
is_mere_relation R le exact _.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoOrder0: FullPseudoOrder Rle Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
PseudoSemiRingOrder lt apply from_pseudo_ring_order;trivial.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
H0: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoOrder0: FullPseudoOrder Rle Rlt
plus_spec: forall z : R,
StrictlyOrderPreserving (plus z)
mult_ext: StrongBinaryExtensionality mult
mult_spec: forall x y : R,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
forall x y : R, x ≤ y <-> ~ (y < x) exact le_iff_not_lt_flip;trivial.
  Qed.
End from_full_pseudo_ring_order.

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

  Lemma flip_le_negate x y : -y ≤ -x <-> x ≤ y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
- y ≤ - x <-> x ≤ y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
- y ≤ - x <-> x ≤ y
  assert (forall a b, a ≤ b -> -b ≤ -a).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
forall a b : R, a ≤ b -> - b ≤ - a
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
X: forall a b : R, a ≤ b -> - b ≤ - a
- y ≤ - x <-> x ≤ y
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
forall a b : R, a ≤ b -> - b ≤ - a intros a b E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- b ≤ - a
    transitivity (-a + -b + a);[apply eq_le|
    transitivity (-a + -b + b);[|apply eq_le]].R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- b = - a - b + a
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- a - b + a ≤ - a - b + b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- a - b + b = - a
    +R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- b = - a - b + a rewrite plus_comm, plus_assoc, plus_negate_r, plus_0_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- b = - b
      reflexivity.
    +R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- a - b + a ≤ - a - b + b apply (order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
a ≤ b trivial.
    +R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- a - b + b = - a rewrite <-plus_assoc, plus_negate_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, a, b: R
E: a ≤ b
- a + 0 = - a apply plus_0_r.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
X: forall a b : R, a ≤ b -> - b ≤ - a
- y ≤ - x <-> x ≤ y split; intros; auto.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
X: forall a b : R, a ≤ b -> - b ≤ - a
X0: - y ≤ - x
x ≤ y
    rewrite <-(negate_involutive x), <-(negate_involutive y); auto.
  Qed.

  Lemma flip_nonneg_negate x : 0 ≤ x <-> -x ≤ 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
0 ≤ x <-> - x ≤ 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
0 ≤ x <-> - x ≤ 0
  split; intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: 0 ≤ x
- x ≤ 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: - x ≤ 0
0 ≤ x
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: 0 ≤ x
- x ≤ 0 rewrite <-negate_0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: 0 ≤ x
- x ≤ - 0 apply flip_le_negate.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: 0 ≤ x
- - 0 ≤ - - x
    rewrite !involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: 0 ≤ x
0 ≤ x trivial.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: - x ≤ 0
0 ≤ x apply flip_le_negate.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: - x ≤ 0
- x ≤ - 0 rewrite negate_0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
E: - x ≤ 0
- x ≤ 0 trivial.
  Qed.

  Lemma flip_nonpos_negate x : x ≤ 0 <-> 0 ≤ -x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
x ≤ 0 <-> 0 ≤ - x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
x ≤ 0 <-> 0 ≤ - x
  pattern x at 1;apply (transport _ (negate_involutive x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
- - x ≤ 0 <-> 0 ≤ - x
  split; intros; apply flip_nonneg_negate;trivial.
  Qed.

  Lemma flip_le_minus_r (x y z : R) : z ≤ y - x <-> z + x ≤ y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
z ≤ y - x <-> z + x ≤ y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
z ≤ y - x <-> z + x ≤ y
  split; intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z ≤ y - x
z + x ≤ y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z + x ≤ y
z ≤ y - x
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z ≤ y - x
z + x ≤ y rewrite plus_comm.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z ≤ y - x
x + z ≤ y
    rewrite (plus_conjugate_alt y x).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z ≤ y - x
x + z ≤ x + (y - x)
    apply (order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z ≤ y - x
z ≤ y - x trivial.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z + x ≤ y
z ≤ y - x rewrite plus_comm.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z + x ≤ y
z ≤ - x + y
    rewrite (plus_conjugate_alt z (- x)), involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z + x ≤ y
- x + (z + x) ≤ - x + y
    apply (order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E: z + x ≤ y
z + x ≤ y trivial.
  Qed.

  Lemma flip_le_minus_l (x y z : R) : y - x ≤ z <-> y ≤ z + x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
y - x ≤ z <-> y ≤ z + x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
y - x ≤ z <-> y ≤ z + x
  pattern x at 2;apply (transport _ (negate_involutive x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
y - x ≤ z <-> y ≤ z - - x
  split; apply flip_le_minus_r.
  Qed.

  Lemma flip_nonneg_minus (x y : R) : 0 ≤ y - x <-> x ≤ y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
0 ≤ y - x <-> x ≤ y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
0 ≤ y - x <-> x ≤ y
  pattern x at 2;apply (transport _ (plus_0_l x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
0 ≤ y - x <-> 0 + x ≤ y
  apply flip_le_minus_r.
  Qed.

  Lemma flip_nonpos_minus (x y : R) : y - x ≤ 0 <-> y ≤ x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
y - x ≤ 0 <-> y ≤ x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
y - x ≤ 0 <-> y ≤ x
  pattern x at 2;apply (transport _ (plus_0_l x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y: R
y - x ≤ 0 <-> y ≤ 0 + x
  apply flip_le_minus_l.
  Qed.

  Lemma nonneg_minus_compat (x y z : R) : 0 ≤ z -> x ≤ y -> x - z ≤ y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
0 ≤ z -> x ≤ y -> x - z ≤ y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
0 ≤ z -> x ≤ y -> x - z ≤ y
  intros E1 E2.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y
x - z ≤ y
  rewrite plus_comm, (plus_conjugate_alt y (- z)), involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y
- z + x ≤ - z + (y + z)
  apply (order_preserving (-(z) +)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y
x ≤ y + z
  transitivity y; trivial.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y
y ≤ y + z
  pattern y at 1;apply (transport _ (plus_0_r y)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y
y + 0 ≤ y + z
  apply (order_preserving (y +)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y
0 ≤ z trivial.
  Qed.

  Lemma nonneg_minus_compat_back (x y z : R) : 0 ≤ z -> x ≤ y - z -> x ≤ y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
0 ≤ z -> x ≤ y - z -> x ≤ y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
0 ≤ z -> x ≤ y - z -> x ≤ y
  intros E1 E2.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y - z
x ≤ y
  transitivity (y - z); trivial.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y - z
y - z ≤ y
  apply nonneg_minus_compat;trivial.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x, y, z: R
E1: 0 ≤ z
E2: x ≤ y - z
y ≤ y apply reflexivity.
  Qed.

  Lemma between_nonneg (x : R) : 0 ≤ x -> -x ≤ x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
0 ≤ x -> - x ≤ x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
0 ≤ x -> - x ≤ x
  intros.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
X: 0 ≤ x
- x ≤ x
  transitivity 0; trivial.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
X: 0 ≤ x
- x ≤ 0
  apply flip_nonneg_negate.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rle: Le R
SemiRingOrder0: SemiRingOrder Rle
x: R
X: 0 ≤ x
0 ≤ x trivial.
  Qed.
End ring_order.

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

  Lemma flip_lt_negate x y : -y < -x <-> x < y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
- y < - x <-> x < y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
- y < - x <-> x < y
  assert (forall a b, a < b -> -b < -a).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
forall a b : R, a < b -> - b < - a
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: forall a b : R, a < b -> - b < - a
- y < - x <-> x < y
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
forall a b : R, a < b -> - b < - a intros a b E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, a, b: R
E: a < b
- b < - a
    rewrite (plus_conjugate (-b) (-a)), involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, a, b: R
E: a < b
- a - b + a < - a
    apply lt_eq_trans with (-a + -b + b).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, a, b: R
E: a < b
- a - b + a < - a - b + b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, a, b: R
E: a < b
- a - b + b = - a
    +R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, a, b: R
E: a < b
- a - b + a < - a - b + b apply (strictly_order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, a, b: R
E: a < b
a < b trivial.
    +R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, a, b: R
E: a < b
- a - b + b = - a rewrite <-plus_assoc,plus_negate_l, plus_0_r.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, a, b: R
E: a < b
- a = - a reflexivity.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: forall a b : R, a < b -> - b < - a
- y < - x <-> x < y split; intros; auto.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: forall a b : R, a < b -> - b < - a
X0: - y < - x
x < y
    rewrite <-(negate_involutive x), <-(negate_involutive y); auto.
  Qed.

  Lemma flip_lt_negate_r x y : y < - x -> x < - y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
y < - x -> x < - y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
y < - x -> x < - y
    pattern y at 1.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
(fun r : R => r < - x -> x < - y) y rewrite <- (@involutive _ (-) _ y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
- - y < - x -> x < - y
    apply flip_lt_negate.
  Qed.
  Lemma flip_lt_negate_l x y : - x < y -> - y < x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
- x < y -> - y < x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
- x < y -> - y < x
    pattern y at 1.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
(fun r : R => - x < r -> - y < x) y rewrite <- (@involutive _ (-) _ y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
- x < - - y -> - y < x
    apply flip_lt_negate.
  Qed.
  Lemma flip_pos_negate x : 0 < x <-> -x < 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
0 < x <-> - x < 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
0 < x <-> - x < 0
  split; intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: 0 < x
- x < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: - x < 0
0 < x
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: 0 < x
- x < 0 rewrite <- negate_0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: 0 < x
- x < - 0 apply flip_lt_negate.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: 0 < x
- - 0 < - - x rewrite !involutive;trivial.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: - x < 0
0 < x apply flip_lt_negate.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: - x < 0
- x < - 0 rewrite negate_0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: - x < 0
- x < 0 trivial.
  Qed.

  Lemma flip_neg_negate x : x < 0 <-> 0 < -x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
x < 0 <-> 0 < - x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
x < 0 <-> 0 < - x
  pattern x at 1;apply (transport _ (negate_involutive x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
- - x < 0 <-> 0 < - x
  split; intros; apply flip_pos_negate;trivial.
  Qed.

  Lemma flip_lt_minus_r (x y z : R) : z < y - x <-> z + x < y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
z < y - x <-> z + x < y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
z < y - x <-> z + x < y
  split; intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E: z < y - x
z + x < y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E: z + x < y
z < y - x
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E: z < y - x
z + x < y rewrite plus_comm, (plus_conjugate_alt y x).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E: z < y - x
x + z < x + (y - x)
    apply (strictly_order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E: z < y - x
z < y - x trivial.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E: z + x < y
z < y - x rewrite plus_comm, (plus_conjugate_alt z (-x)), involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E: z + x < y
- x + (z + x) < - x + y
    apply (strictly_order_preserving _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E: z + x < y
z + x < y trivial.
  Qed.

  Lemma flip_lt_minus_l (x y z : R) : y - x < z <-> y < z + x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
y - x < z <-> y < z + x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
y - x < z <-> y < z + x
  pattern x at 2;apply (transport _ (negate_involutive x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
y - x < z <-> y < z - - x
  split; apply flip_lt_minus_r.
  Qed.

  Lemma flip_pos_minus (x y : R) : 0 < y - x <-> x < y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
0 < y - x <-> x < y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
0 < y - x <-> x < y
  pattern x at 2;apply (transport _ (plus_0_l x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
0 < y - x <-> 0 + x < y
  apply flip_lt_minus_r.
  Qed.

  Lemma flip_neg_minus (x y : R) : y - x < 0 <-> y < x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
y - x < 0 <-> y < x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
y - x < 0 <-> y < x
  pattern x at 2;apply (transport _ (plus_0_l x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
y - x < 0 <-> y < 0 + x
  apply flip_lt_minus_l.
  Qed.

  Lemma pos_minus_compat (x y z : R) : 0 < z -> x < y -> x - z < y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
0 < z -> x < y -> x - z < y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
0 < z -> x < y -> x - z < y
  intros E1 E2.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E1: 0 < z
E2: x < y
x - z < y
  rewrite plus_comm, (plus_conjugate_alt y (-z)), involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E1: 0 < z
E2: x < y
- z + x < - z + (y + z)
  apply (strictly_order_preserving (-(z) +)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E1: 0 < z
E2: x < y
x < y + z
  transitivity y; trivial.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E1: 0 < z
E2: x < y
y < y + z
  pattern y at 1;apply (transport _ (plus_0_r y)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E1: 0 < z
E2: x < y
y + 0 < y + z
  apply (strictly_order_preserving (y +)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E1: 0 < z
E2: x < y
0 < z
  trivial.
  Qed.

  Lemma pos_minus_lt_compat_r x z : 0 < z <-> x - z < x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
0 < z <-> x - z < x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
0 < z <-> x - z < x
    pattern x at 2;apply (transport _ (plus_0_r x)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
0 < z <-> x - z < x + 0
    split; intros.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
X: 0 < z
x - z < x + 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
X: x - z < x + 0
0 < z
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
X: 0 < z
x - z < x + 0 apply (strictly_order_preserving _), flip_pos_negate; assumption.
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
X: x - z < x + 0
0 < z apply flip_pos_negate, (strictly_order_reflecting (x+)); assumption.
  Qed.

  Lemma pos_minus_lt_compat_l x z : 0 < z <-> - z + x < x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
0 < z <-> - z + x < x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
0 < z <-> - z + x < x
    split; intros ltz.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
ltz: 0 < z
- z + x < x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
ltz: - z + x < x
0 < z
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
ltz: 0 < z
- z + x < x rewrite (commutativity (-z) x); apply pos_minus_lt_compat_r; assumption.
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
ltz: - z + x < x
0 < z rewrite (commutativity (-z) x) in ltz.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
ltz: x - z < x
0 < z
      apply (snd (pos_minus_lt_compat_r x z)); assumption.
  Qed.

  Lemma between_pos (x : R) : 0 < x -> -x < x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
0 < x -> - x < x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
0 < x -> - x < x
  intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: 0 < x
- x < x
  transitivity 0; trivial.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: 0 < x
- x < 0
  apply flip_pos_negate.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x: R
E: 0 < x
0 < x trivial.
  Qed.

End strict_ring_order.

Section strict_ring_apart.
  Context `{FullPseudoSemiRingOrder R}.

  Definition positive_apart_zero (z : R) (Pz : 0 < z) : z ≶ 0
    := pseudo_order_lt_apart_flip 0 z Pz.
  Definition negative_apart_zero (z : R) (Nz : z < 0) : z ≶ 0
    := pseudo_order_lt_apart z 0 Nz.

End strict_ring_apart.

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

  Lemma projected_ring_order (f : R2 -> R1) `{!IsSemiRingPreserving f} `{!IsInjective f}
    : (forall x y, x ≤ y <-> f x ≤ f y) -> SemiRingOrder R2le.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective0: IsInjective f
(forall x y : R2, x ≤ y <-> f x ≤ f y) ->
SemiRingOrder R2le
  Proof.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective0: IsInjective f
(forall x y : R2, x ≤ y <-> f x ≤ f y) ->
SemiRingOrder R2le
  intros P.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective0: IsInjective f
P: forall x y : R2, x ≤ y <-> f x ≤ f y
SemiRingOrder R2le apply (projected_srorder f P).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective0: IsInjective f
P: forall x y : R2, x ≤ y <-> f x ≤ f y
forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
  intros x y E.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective0: IsInjective f
P: forall x y : R2, x ≤ y <-> f x ≤ f y
x, y: R2
E: x ≤ y
{z : R2 & y = x + z} exists (-x + y).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective0: IsInjective f
P: forall x y : R2, x ≤ y <-> f x ≤ f y
x, y: R2
E: x ≤ y
y = x + (- x + y)
  rewrite plus_assoc, plus_negate_r, plus_0_l.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective0: IsInjective f
P: forall x y : R2, x ≤ y <-> f x ≤ f y
x, y: R2
E: x ≤ y
y = y reflexivity.
  Qed.

  Context `{!SemiRingOrder R2le} {f : R1 -> R2} `{!IsSemiRingPreserving f}.

  Lemma reflecting_preserves_nonneg : (forall x, 0 ≤ f x -> 0 ≤ x) -> OrderReflecting f.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
(forall x : R1, 0 ≤ f x -> 0 ≤ x) -> OrderReflecting f
  Proof.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
(forall x : R1, 0 ≤ f x -> 0 ≤ x) -> OrderReflecting f
  intros E.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
E: forall x : R1, 0 ≤ f x -> 0 ≤ x
OrderReflecting f repeat (split; try exact _).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
E: forall x : R1, 0 ≤ f x -> 0 ≤ x
OrderReflecting f intros x y F.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
E: forall x : R1, 0 ≤ f x -> 0 ≤ x
x, y: R1
F: f x ≤ f y
x ≤ y
  apply flip_nonneg_minus, E.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
E: forall x : R1, 0 ≤ f x -> 0 ≤ x
x, y: R1
F: f x ≤ f y
0 ≤ f (y - x)
  rewrite preserves_plus, preserves_negate.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
E: forall x : R1, 0 ≤ f x -> 0 ≤ x
x, y: R1
F: f x ≤ f y
0 ≤ f y - f x
  apply (flip_nonneg_minus (f x)), F.
  Qed.

  Lemma preserves_ge_negate1 `{!OrderPreserving f} x : - 1 ≤ x -> - 1 ≤ f x.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
-1 ≤ x -> -1 ≤ f x
  Proof.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
-1 ≤ x -> -1 ≤ f x
  intros.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
X: -1 ≤ x
-1 ≤ f x rewrite <-(preserves_1 (f:=f)), <-preserves_negate.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
X: -1 ≤ x
f (-1) ≤ f x
  apply (order_preserving f).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
X: -1 ≤ x
-1 ≤ x trivial.
  Qed.

  Lemma preserves_le_negate1 `{!OrderPreserving f} x : x ≤ - 1 -> f x ≤ - 1.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
x ≤ -1 -> f x ≤ -1
  Proof.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
x ≤ -1 -> f x ≤ -1
  intros.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
X: x ≤ -1
f x ≤ -1 rewrite <-(preserves_1 (f:=f)), <-preserves_negate.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
X: x ≤ -1
f x ≤ f (-1)
  apply (order_preserving f).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1le: Le R1
SemiRingOrder0: SemiRingOrder R1le
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2le: Le R2
is_mere_relation0: is_mere_relation R2 R2le
SemiRingOrder1: SemiRingOrder R2le
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
OrderPreserving0: OrderPreserving f
x: R1
X: x ≤ -1
x ≤ -1 trivial.
  Qed.
End another_ring_order.

Section another_strict_ring_order.
  Context `{IsCRing R1} `{!StrictSemiRingOrder R1lt} `{IsCRing R2} `{R2lt : Lt R2}
    `{is_mere_relation R2 lt}.

  Lemma projected_strict_ring_order (f : R2 -> R1) `{!IsSemiRingPreserving f} :
    (forall x y, x < y <-> f x < f y) -> StrictSemiRingOrder R2lt.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
(forall x y : R2, x < y <-> f x < f y) ->
StrictSemiRingOrder R2lt
  Proof.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
(forall x y : R2, x < y <-> f x < f y) ->
StrictSemiRingOrder R2lt
  intros P.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
StrictSemiRingOrder R2lt pose proof (projected_strict_order f P).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
StrictSemiRingOrder R2lt
  apply from_strict_ring_order.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
forall z : R2, StrictlyOrderPreserving (plus z)
R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
forall x y : R2,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
  -R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
forall z : R2, StrictlyOrderPreserving (plus z) intros z x y E.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
z, x, y: R2
E: x < y
z + x < z + y
    apply P.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
z, x, y: R2
E: x < y
f (z + x) < f (z + y) rewrite 2!(preserves_plus (f:=f)).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
z, x, y: R2
E: x < y
f z + f x < f z + f y
    apply (strictly_order_preserving _), P.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
z, x, y: R2
E: x < y
x < y trivial.
  -R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
forall x y : R2,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y) intros x y E1 E2.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
x, y: R2
E1: PropHolds (0 < x)
E2: PropHolds (0 < y)
PropHolds (0 < x * y)
    apply P.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
x, y: R2
E1: PropHolds (0 < x)
E2: PropHolds (0 < y)
f 0 < f (x * y) rewrite preserves_mult, preserves_0.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
R1lt: Lt R1
StrictSemiRingOrder0: StrictSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H0: IsCRing R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
P: forall x y : R2, x < y <-> f x < f y
X: StrictOrder R2lt
x, y: R2
E1: PropHolds (0 < x)
E2: PropHolds (0 < y)
0 < f x * f y
    apply pos_mult_compat; rewrite <-(preserves_0 (f:=f)); apply P; trivial.
  Qed.
End another_strict_ring_order.

Section another_pseudo_ring_order.
  Context `{IsCRing R1} `{Apart R1} `{!PseudoSemiRingOrder R1lt}
    `{IsCRing R2} `{IsApart R2} `{R2lt : Lt R2}
    `{is_mere_relation R2 lt}.

  Lemma projected_pseudo_ring_order (f : R2 -> R1) `{!IsSemiRingPreserving f}
    `{!IsStrongInjective f}
    : (forall x y, x < y <-> f x < f y) -> PseudoSemiRingOrder R2lt.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
(forall x y : R2, x < y <-> f x < f y) ->
PseudoSemiRingOrder R2lt
  Proof.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
(forall x y : R2, x < y <-> f x < f y) ->
PseudoSemiRingOrder R2lt
  intros P.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
PseudoSemiRingOrder R2lt
  pose proof (projected_pseudo_order f P).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
PseudoSemiRingOrder R2lt
  pose proof (projected_strict_ring_order f P).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
PseudoSemiRingOrder R2lt
  apply from_pseudo_ring_order; try exact _.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
StrongBinaryExtensionality mult
  pose proof (@pseudo_order_apart R1 H0 R1lt pseudo_srorder_strict : IsApart R1).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
X1: IsApart R1
StrongBinaryExtensionality mult
  pose proof (pseudo_order_apart : IsApart R2).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
X1: IsApart R1
X2: IsApart R2
StrongBinaryExtensionality mult
  pose proof (strong_injective_mor f).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
X1: IsApart R1
X2: IsApart R2
X3: StrongExtensionality f
StrongBinaryExtensionality mult
  repeat (split; try exact _).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
X1: IsApart R1
X2: IsApart R2
X3: StrongExtensionality f
StrongBinaryExtensionality mult
  intros x₁ y₁ x₂ y₂ E.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
X1: IsApart R1
X2: IsApart R2
X3: StrongExtensionality f
x₁, y₁, x₂, y₂: R2
E: x₁ * y₁ ≶ x₂ * y₂
hor (x₁ ≶ x₂) (y₁ ≶ y₂)
  apply (strong_injective f) in E.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
X1: IsApart R1
X2: IsApart R2
X3: StrongExtensionality f
x₁, y₁, x₂, y₂: R2
E: f (x₁ * y₁) ≶ f (x₂ * y₂)
hor (x₁ ≶ x₂) (y₁ ≶ y₂) rewrite 2!(preserves_mult (f:=f)) in E.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1lt: Lt R1
PseudoSemiRingOrder0: PseudoSemiRingOrder R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P: forall x y : R2, x < y <-> f x < f y
X: PseudoOrder R2lt
X0: StrictSemiRingOrder R2lt
X1: IsApart R1
X2: IsApart R2
X3: StrongExtensionality f
x₁, y₁, x₂, y₂: R2
E: f x₁ * f y₁ ≶ f x₂ * f y₂
hor (x₁ ≶ x₂) (y₁ ≶ y₂)
  apply (merely_destruct (strong_binary_extensionality (.*.) _ _ _ _ E));
  intros [?|?];apply tr; [left | right];
  apply (strong_extensionality f); trivial.
  Qed.
End another_pseudo_ring_order.

Section another_full_pseudo_ring_order.
  Context `{IsCRing R1} `{Apart R1} `{!FullPseudoSemiRingOrder R1le R1lt}
    `{IsCRing R2} `{IsApart R2} `{R2le : Le R2} `{R2lt : Lt R2}
    `{is_mere_relation R2 le} `{is_mere_relation R2 lt}.

  Lemma projected_full_pseudo_ring_order (f : R2 -> R1) `{!IsSemiRingPreserving f}
    `{!IsStrongInjective f}
    : (forall x y, x ≤ y <-> f x ≤ f y) -> (forall x y, x < y <-> f x < f y) ->
    FullPseudoSemiRingOrder R2le R2lt.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1le: Le R1
R1lt: Lt R1
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  R1le R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2le: Le R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 le
is_mere_relation1: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
(forall x y : R2, x ≤ y <-> f x ≤ f y) ->
(forall x y : R2, x < y <-> f x < f y) ->
FullPseudoSemiRingOrder R2le R2lt
  Proof.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1le: Le R1
R1lt: Lt R1
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  R1le R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2le: Le R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 le
is_mere_relation1: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
(forall x y : R2, x ≤ y <-> f x ≤ f y) ->
(forall x y : R2, x < y <-> f x < f y) ->
FullPseudoSemiRingOrder R2le R2lt
  intros P1 P2.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1le: Le R1
R1lt: Lt R1
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  R1le R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2le: Le R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 le
is_mere_relation1: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P1: forall x y : R2, x ≤ y <-> f x ≤ f y
P2: forall x y : R2, x < y <-> f x < f y
FullPseudoSemiRingOrder R2le R2lt pose proof (projected_full_pseudo_order f P1 P2).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1le: Le R1
R1lt: Lt R1
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  R1le R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2le: Le R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 le
is_mere_relation1: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P1: forall x y : R2, x ≤ y <-> f x ≤ f y
P2: forall x y : R2, x < y <-> f x < f y
X: FullPseudoOrder R2le R2lt
FullPseudoSemiRingOrder R2le R2lt
  pose proof (projected_pseudo_ring_order f P2).R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1le: Le R1
R1lt: Lt R1
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  R1le R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2le: Le R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 le
is_mere_relation1: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P1: forall x y : R2, x ≤ y <-> f x ≤ f y
P2: forall x y : R2, x < y <-> f x < f y
X: FullPseudoOrder R2le R2lt
X0: PseudoSemiRingOrder R2lt
FullPseudoSemiRingOrder R2le R2lt
  split; try exact _.R1: Type
Aplus: Plus R1
Amult: Mult R1
Azero: Zero R1
Aone: One R1
Anegate: Negate R1
H: IsCRing R1
H0: Apart R1
R1le: Le R1
R1lt: Lt R1
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  R1le R1lt
R2: Type
Aplus0: Plus R2
Amult0: Mult R2
Azero0: Zero R2
Aone0: One R2
Anegate0: Negate R2
H1: IsCRing R2
Aap: Apart R2
H2: IsApart R2
R2le: Le R2
R2lt: Lt R2
is_mere_relation0: is_mere_relation R2 le
is_mere_relation1: is_mere_relation R2 lt
f: R2 -> R1
IsSemiRingPreserving0: IsSemiRingPreserving f
IsStrongInjective0: IsStrongInjective f
P1: forall x y : R2, x ≤ y <-> f x ≤ f y
P2: forall x y : R2, x < y <-> f x < f y
X: FullPseudoOrder R2le R2lt
X0: PseudoSemiRingOrder R2lt
forall x y : R2, x ≤ y <-> ~ (y < x) exact le_iff_not_lt_flip.
  Qed.
End another_full_pseudo_ring_order.