Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export HoTT.Classes.orders.orders HoTT.Classes.orders.maps. Generalizable Variables R Rlt f. Section semiring_order. Context `{SemiRingOrder R} `{!IsSemiCRing R}. (* Add Ring R : (stdlib_semiring_theory R). *)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, OrderEmbedding (fun y : R => y + z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, OrderEmbedding (fun y : R => y + z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R

OrderEmbedding (fun y : R => y + z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R

OrderPreserving (fun y : R => y + z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R
OrderReflecting (fun y : R => y + z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R

OrderPreserving (fun y : R => y + z)
apply order_preserving_flip.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R

OrderReflecting (fun y : R => y + z)
apply order_reflecting_flip. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, LeftCancellation plus z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, LeftCancellation plus z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E: z + x = z + y

x = y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E: z + x = z + y

z + y = z + x
apply symmetry;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, RightCancellation plus z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, RightCancellation plus z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R

RightCancellation plus z
apply (right_cancel_from_left (+)). Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R

0 ≤ z <-> x ≤ x + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R

0 ≤ z <-> x ≤ x + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R

(fun r : R => 0 ≤ z <-> r ≤ x + z) x
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R

0 ≤ z <-> x + 0 ≤ x + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R
X: 0 ≤ z

x + 0 ≤ x + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R
X: x + 0 ≤ x + z
0 ≤ z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R
X: 0 ≤ z

x + 0 ≤ x + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R
X: 0 ≤ z

0 ≤ z
trivial.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R
X: x + 0 ≤ x + z

0 ≤ z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R
X: x + 0 ≤ x + z

x + 0 ≤ x + z
trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R

0 ≤ z <-> x ≤ z + x
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R

0 ≤ z <-> x ≤ z + x
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, z: R

0 ≤ z <-> x ≤ x + z
apply nonneg_plus_le_compat_r. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R

x₁ ≤ y₁ -> x₂ ≤ y₂ -> x₁ + x₂ ≤ y₁ + y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R

x₁ ≤ y₁ -> x₂ ≤ y₂ -> x₁ + x₂ ≤ y₁ + y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

x₁ + x₂ ≤ y₁ + y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

x₁ + x₂ ≤ y₁ + x₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂
y₁ + x₂ ≤ y₁ + y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

x₁ + x₂ ≤ y₁ + x₂
apply (order_preserving (+ x₂));trivial.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

y₁ + x₂ ≤ y₁ + y₂
apply (order_preserving (y₁ +));trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x ≤ y -> x ≤ y + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x ≤ y -> x ≤ y + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 ≤ z
X0: x ≤ y

x ≤ y + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 ≤ z
X0: x ≤ y

x + 0 ≤ y + z
apply plus_le_compat;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x ≤ y -> x ≤ z + y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x ≤ y -> x ≤ z + y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x ≤ y -> x ≤ y + z
apply plus_le_compat_r. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

x ≤ 0 -> y ≤ 0 -> x + y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

x ≤ 0 -> y ≤ 0 -> x + y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x ≤ 0
X0: y ≤ 0

x + y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x ≤ 0
X0: y ≤ 0

x + y ≤ 0 + 0
apply plus_le_compat;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) -> PropHolds (0 ≤ x + y)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) -> PropHolds (0 ≤ x + y)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: PropHolds (0 ≤ x)
X0: PropHolds (0 ≤ y)

PropHolds (0 ≤ x + y)
apply plus_le_compat_l;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

x ≤ y -> {z : R & ((0 ≤ z) * (y = (x + z)%mc))%type}
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

x ≤ y -> {z : R & ((0 ≤ z) * (y = (x + z)%mc))%type}
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
E: x ≤ y

{z : R & ((0 ≤ z) * (y = (x + z)%mc))%type}
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
E: x ≤ y
z: R
Ez: y = x + z

{z : R & ((0 ≤ z) * (y = (x + z)%mc))%type}
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
E: x ≤ y
z: R
Ez: y = x + z

((0 ≤ z) * (y = (x + z)%mc))%type
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
E: x ≤ y
z: R
Ez: y = x + z

0 ≤ z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
E: x ≤ y
z: R
Ez: y = x + z

x + 0 ≤ x + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
E: x ≤ y
z: R
Ez: y = x + z

x ≤ y
trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> y = x + z -> x ≤ y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> y = x + z -> x ≤ y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
E1: 0 ≤ z
E2: y = x + z

x ≤ y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
E1: 0 ≤ z
E2: y = x + z

x ≤ x + z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
E1: 0 ≤ z
E2: y = x + z

0 ≤ z
trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 ≤ z) -> OrderPreserving (mult z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 ≤ z) -> OrderPreserving (mult z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R
E: PropHolds (0 ≤ z)

OrderPreserving (mult z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R
E: PropHolds (0 ≤ z)

OrderPreserving (mult z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R
E: PropHolds (0 ≤ z)
x, y: R
F: x ≤ y

z * x ≤ z * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R
E: PropHolds (0 ≤ z)
x, y: R
F: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: y = x + a

z * x ≤ z * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R
E: PropHolds (0 ≤ z)
x, y: R
F: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: y = x + a

z * x ≤ z * x + z * a
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R
E: PropHolds (0 ≤ z)
x, y: R
F: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: y = x + a

0 ≤ z * a
apply nonneg_mult_compat;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 ≤ z) -> OrderPreserving (fun y : R => y * z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 ≤ z) -> OrderPreserving (fun y : R => y * z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
z: R
X: PropHolds (0 ≤ z)

OrderPreserving (fun y : R => y * z)
apply order_preserving_flip. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R

0 ≤ x₁ -> 0 ≤ x₂ -> x₁ ≤ y₁ -> x₂ ≤ y₂ -> x₁ * x₂ ≤ y₁ * y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R

0 ≤ x₁ -> 0 ≤ x₂ -> x₁ ≤ y₁ -> x₂ ≤ y₂ -> x₁ * x₂ ≤ y₁ * y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
Ex₁: 0 ≤ x₁
Ey₁: 0 ≤ x₂
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

x₁ * x₂ ≤ y₁ * y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
Ex₁: 0 ≤ x₁
Ey₁: 0 ≤ x₂
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

x₁ * x₂ ≤ y₁ * x₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
Ex₁: 0 ≤ x₁
Ey₁: 0 ≤ x₂
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂
y₁ * x₂ ≤ y₁ * y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
Ex₁: 0 ≤ x₁
Ey₁: 0 ≤ x₂
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

x₁ * x₂ ≤ y₁ * x₂
apply (order_preserving_flip_nonneg (.*.) x₂);trivial.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
Ex₁: 0 ≤ x₁
Ey₁: 0 ≤ x₂
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

y₁ * x₂ ≤ y₁ * y₂
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
Ex₁: 0 ≤ x₁
Ey₁: 0 ≤ x₂
E1: x₁ ≤ y₁
E2: x₂ ≤ y₂

0 ≤ y₁
transitivity x₁;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

1 ≤ z -> 0 ≤ y -> x ≤ y -> x ≤ y * z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

1 ≤ z -> 0 ≤ y -> x ≤ y -> x ≤ y * z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 1 ≤ z
X0: 0 ≤ y
X1: x ≤ y

x ≤ y * z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 1 ≤ z
X0: 0 ≤ y
X1: x ≤ y

y ≤ y * z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 1 ≤ z
X0: 0 ≤ y
X1: x ≤ y

y * 1 ≤ y * z
apply (order_preserving_nonneg (.*.) y);trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

1 ≤ z -> 0 ≤ y -> x ≤ y -> x ≤ z * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

1 ≤ z -> 0 ≤ y -> x ≤ y -> x ≤ z * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

1 ≤ z -> 0 ≤ y -> x ≤ y -> x ≤ y * z
apply ge_1_mult_le_compat_r. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

z ≤ 0 -> x ≤ y -> z * y ≤ z * x
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

z ≤ 0 -> x ≤ y -> z * y ≤ z * x
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y

z * y ≤ z * x
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * y ≤ z * x
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * (x + b) ≤ z * x
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

0 ≤ a * b
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b
z * x = z * (x + b) + a * b
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

0 ≤ a * b
apply nonneg_mult_compat;trivial.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * x = z * (x + b) + a * b
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * x = z * x + (z + a) * b
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b
z * x + (z + a) * b = z * (x + b) + a * b
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * x = z * x + (z + a) * b
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * x = z * x + 0 * b
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * x = z * x
reflexivity.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * x + (z + a) * b = z * (x + b) + a * b
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R
Ez: z ≤ 0
Exy: x ≤ y
a: R
Ea1: 0 ≤ a
Ea2: 0 = z + a
b: R
Eb1: 0 ≤ b
Eb2: y = x + b

z * x + (z * b + a * b) = z * x + z * b + a * b
apply associativity. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

z ≤ 0 -> x ≤ y -> y * z ≤ x * z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

z ≤ 0 -> x ≤ y -> y * z ≤ x * z
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y, z: R

z ≤ 0 -> x ≤ y -> z * y ≤ z * x
apply flip_nonpos_mult_l. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

x ≤ 0 -> y ≤ 0 -> 0 ≤ x * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

x ≤ 0 -> y ≤ 0 -> 0 ≤ x * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x ≤ 0
X0: y ≤ 0

0 ≤ x * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x ≤ 0
X0: y ≤ 0

x * 0 ≤ x * y
apply flip_nonpos_mult_l;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

x ≤ 0 -> 0 ≤ y -> x * y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

x ≤ 0 -> 0 ≤ y -> x * y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x ≤ 0
X0: 0 ≤ y

x * y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x ≤ 0
X0: 0 ≤ y

x * y ≤ x * 0
apply flip_nonpos_mult_l;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

0 ≤ x -> y ≤ 0 -> x * y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R

0 ≤ x -> y ≤ 0 -> x * y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x
X0: y ≤ 0

x * y ≤ 0
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x
X0: y ≤ 0

y * x ≤ 0
apply nonpos_nonneg_mult;trivial. Qed. End semiring_order. (* Due to bug #2528 *) #[export] Hint Extern 7 (PropHolds (0 ≤ _ + _)) => eapply @nonneg_plus_compat : typeclass_instances. Section strict_semiring_order. Context `{IsSemiCRing R} `{!StrictSemiRingOrder Rlt}. (* Add Ring Rs : (stdlib_semiring_theory R). *)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt

forall z : R, StrictOrderEmbedding (fun y : R => y + z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt

forall z : R, StrictOrderEmbedding (fun y : R => y + z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R

StrictOrderEmbedding (fun y : R => y + z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R

StrictlyOrderPreserving (fun y : R => y + z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R
StrictlyOrderReflecting (fun y : R => y + z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R

StrictlyOrderPreserving (fun y : R => y + z)
apply strictly_order_preserving_flip.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R

StrictlyOrderReflecting (fun y : R => y + z)
apply strictly_order_reflecting_flip. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R

0 < z <-> x < x + z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R

0 < z <-> x < x + z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R

0 < z <-> x + 0 < x + z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
X: 0 < z

x + 0 < x + z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
X: x + 0 < x + z
0 < z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
X: 0 < z

x + 0 < x + z
apply (strictly_order_preserving _);trivial.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R
X: x + 0 < x + z

0 < z
apply (strictly_order_reflecting (x+));trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R

0 < z -> x < z + x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R

0 < z -> x < z + x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, z: R

0 < z -> x < x + z
apply pos_plus_lt_compat_r. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R

x₁ < y₁ -> x₂ < y₂ -> x₁ + x₂ < y₁ + y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R

x₁ < y₁ -> x₂ < y₂ -> x₁ + x₂ < y₁ + y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ < y₂

x₁ + x₂ < y₁ + y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ < y₂

x₁ + x₂ < y₁ + x₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ < y₂
y₁ + x₂ < y₁ + y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ < y₂

x₁ + x₂ < y₁ + x₂
apply (strictly_order_preserving (+ x₂));trivial.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ < y₂

y₁ + x₂ < y₁ + y₂
apply (strictly_order_preserving (y₁ +));trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

0 < z -> x < y -> x < y + z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

0 < z -> x < y -> x < y + z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
X: 0 < z
X0: x < y

x < y + z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
X: 0 < z
X0: x < y

x + 0 < y + z
apply plus_lt_compat;trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
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
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
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
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

0 < z -> x < y -> x < y + z
apply plus_lt_compat_r. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

x < 0 -> y < 0 -> x + y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

x < 0 -> y < 0 -> x + y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: x < 0
X0: y < 0

x + y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: x < 0
X0: y < 0

x + y < 0 + 0
apply plus_lt_compat;trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x + y)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x + y)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: PropHolds (0 < x)
X0: PropHolds (0 < y)

PropHolds (0 < x + y)
apply plus_lt_compat_l;trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

0 < z -> y = x + z -> x < y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

0 < z -> y = x + z -> x < y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E1: 0 < z
E2: y = x + z

x < y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
E1: 0 < z
E2: y = x + z

x < x + z
apply pos_plus_lt_compat_r;trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

x < y -> {z : R & ((0 < z) * (y = (x + z)%mc))%type}
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

x < y -> {z : R & ((0 < z) * (y = (x + z)%mc))%type}
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
E: x < y

{z : R & ((0 < z) * (y = (x + z)%mc))%type}
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
E: x < y
z: R
Ez: y = x + z

{z : R & ((0 < z) * (y = (x + z)%mc))%type}
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
E: x < y
z: R
Ez: y = x + z

((0 < z) * (y = (x + z)%mc))%type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
E: x < y
z: R
Ez: y = x + z

0 < z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
E: x < y
z: R
Ez: y = x + z

x + 0 < x + z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
E: x < y
z: R
Ez: y = x + z

x < y
trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt

forall z : R, PropHolds (0 < z) -> StrictlyOrderPreserving (mult z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt

forall z : R, PropHolds (0 < z) -> StrictlyOrderPreserving (mult z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R
E: PropHolds (0 < z)
x, y: R
F: x < y

z * x < z * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R
E: PropHolds (0 < z)
x, y: R
F: x < y
a: R
Ea1: 0 < a
Ea2: y = x + a

z * x < z * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R
E: PropHolds (0 < z)
x, y: R
F: x < y
a: R
Ea1: 0 < a
Ea2: y = x + a

z * x < z * x + z * a
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R
E: PropHolds (0 < z)
x, y: R
F: x < y
a: R
Ea1: 0 < a
Ea2: y = x + a

0 < z * a
apply pos_mult_compat;trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt

forall z : R, PropHolds (0 < z) -> StrictlyOrderPreserving (fun y : R => y * z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt

forall z : R, PropHolds (0 < z) -> StrictlyOrderPreserving (fun y : R => y * z)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
z: R
X: PropHolds (0 < z)

StrictlyOrderPreserving (fun y : R => y * z)
apply strictly_order_preserving_flip. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R

0 < x₁ -> 0 < x₂ -> x₁ < y₁ -> x₂ < y₂ -> x₁ * x₂ < y₁ * y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R

0 < x₁ -> 0 < x₂ -> x₁ < y₁ -> x₂ < y₂ -> x₁ * x₂ < y₁ * y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
Ex₁: 0 < x₁
Ey₁: 0 < x₂
E1: x₁ < y₁
E2: x₂ < y₂

x₁ * x₂ < y₁ * y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
Ex₁: 0 < x₁
Ey₁: 0 < x₂
E1: x₁ < y₁
E2: x₂ < y₂

x₁ * x₂ < y₁ * x₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
Ex₁: 0 < x₁
Ey₁: 0 < x₂
E1: x₁ < y₁
E2: x₂ < y₂
y₁ * x₂ < y₁ * y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
Ex₁: 0 < x₁
Ey₁: 0 < x₂
E1: x₁ < y₁
E2: x₂ < y₂

x₁ * x₂ < y₁ * x₂
apply (strictly_order_preserving_flip_pos (.*.) x₂);trivial.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
Ex₁: 0 < x₁
Ey₁: 0 < x₂
E1: x₁ < y₁
E2: x₂ < y₂

y₁ * x₂ < y₁ * y₂
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x₁, y₁, x₂, y₂: R
Ex₁: 0 < x₁
Ey₁: 0 < x₂
E1: x₁ < y₁
E2: x₂ < y₂

0 < y₁
transitivity x₁;trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

1 < z -> 0 < y -> x < y -> x < y * z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

1 < z -> 0 < y -> x < y -> x < y * z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
X: 1 < z
X0: 0 < y
X1: x < y

x < y * z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
X: 1 < z
X0: 0 < y
X1: x < y

y < y * z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
X: 1 < z
X0: 0 < y
X1: x < y

y * 1 < y * z
apply (strictly_order_preserving_pos (.*.) y);trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

1 < z -> 0 < y -> x < y -> x < z * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

1 < z -> 0 < y -> x < y -> x < z * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

1 < z -> 0 < y -> x < y -> x < y * z
apply gt_1_mult_lt_compat_r. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

z < 0 -> x < y -> z * y < z * x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

z < 0 -> x < y -> z * y < z * x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y

z * y < z * x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

z * y < z * x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

z * (x + b) < z * x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

0 < a * b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b
z * x = z * (x + b) + a * b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

0 < a * b
apply pos_mult_compat;trivial.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

z * x = z * (x + b) + a * b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

z * x = z * x + (z + a) * b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b
z * x + (z + a) * b = z * (x + b) + a * b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

z * x = z * x + (z + a) * b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

z * x = z * x + 0 * b
rewrite mult_0_l,plus_0_r;reflexivity.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

z * x + (z + a) * b = z * (x + b) + a * b
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R
Ez: z < 0
Exy: x < y
a: R
Ea1: 0 < a
Ea2: 0 = z + a
b: R
Eb1: 0 < b
Eb2: y = x + b

z * x + (z * b + a * b) = z * x + z * b + a * b
apply associativity. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

z < 0 -> x < y -> y * z < x * z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

z < 0 -> x < y -> y * z < x * z
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y, z: R

z < 0 -> x < y -> z * y < z * x
apply flip_neg_mult_l. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

x < 0 -> y < 0 -> 0 < x * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

x < 0 -> y < 0 -> 0 < x * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: x < 0
X0: y < 0

0 < x * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: x < 0
X0: y < 0

x * 0 < x * y
apply flip_neg_mult_l;trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

0 < x -> 0 < y -> 0 < x * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

0 < x -> 0 < y -> 0 < x * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
xpos: 0 < x
ypos: 0 < y

0 < x * y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
xpos: 0 < x
ypos: 0 < y

x * 0 < x * y
apply (pos_mult_lt_l); assumption. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

x < 0 -> 0 < y -> x * y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

x < 0 -> 0 < y -> x * y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: x < 0
X0: 0 < y

x * y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: x < 0
X0: 0 < y

x * y < x * 0
apply flip_neg_mult_l;trivial. Qed.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

0 < x -> y < 0 -> x * y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R

0 < x -> y < 0 -> x * y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: 0 < x
X0: y < 0

x * y < 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
Rlt: Lt R
StrictSemiRingOrder0: StrictSemiRingOrder Rlt
x, y: R
X: 0 < x
X0: y < 0

y * x < 0
apply neg_pos_mult;trivial. Qed. End strict_semiring_order. (* Due to bug #2528 *) #[export] Hint Extern 7 (PropHolds (0 < _ + _)) => eapply @pos_plus_compat : typeclass_instances. Section pseudo_semiring_order. Context `{PseudoSemiRingOrder R} `{!IsSemiCRing R}. (* Add Ring Rp : (stdlib_semiring_theory R). *) Local Existing Instance pseudo_order_apart.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

StrictSemiRingOrder (Alt : Lt R)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

StrictSemiRingOrder (Alt : Lt R)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall x y : R, x < y -> {z : R & y = x + z}
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
forall x y : R, PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x * y)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall x y : R, x < y -> {z : R & y = x + z}
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x < y

{z : R & y = x + z}
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x < y

x < y
trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall x y : R, PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x * y)
apply pseudo_srorder_pos_mult_compat. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

StrongBinaryExtensionality plus
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

StrongBinaryExtensionality plus
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, StrongExtensionality (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
X: forall z : R, StrongExtensionality (plus z)
StrongBinaryExtensionality plus
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, StrongExtensionality (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R

StrongExtensionality (plus z)
apply pseudo_order_embedding_ext.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
X: forall z : R, StrongExtensionality (plus z)

StrongBinaryExtensionality plus
apply apartness.strong_binary_setoid_morphism_commutative. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, StrongLeftCancellation plus z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, StrongLeftCancellation plus z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E: x ≶ y

z + x ≶ z + y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E: ((x < y) + (y < x))%type

(((z + x)%mc < (z + y)%mc) + ((z + y)%mc < (z + x)%mc))%type
destruct E; [left | right]; apply (strictly_order_preserving (z +));trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, StrongRightCancellation plus z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, StrongRightCancellation plus z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R

StrongRightCancellation plus z
apply (strong_right_cancel_from_left (+)). Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

x * y < 0 -> ((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

x * y < 0 -> ((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0

((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0

0 ≶ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 ≶ x
0 ≶ y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 ≶ x
Ey: 0 ≶ y
((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0

0 ≶ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0

0 * y ≶ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0

0 ≶ x * y
apply pseudo_order_lt_apart_flip;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 ≶ x

0 ≶ y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 ≶ x

x * 0 ≶ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 ≶ x

0 ≶ x * y
apply pseudo_order_lt_apart_flip;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 ≶ x
Ey: 0 ≶ y

((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: ((0 < x) + (x < 0))%type
Ey: ((0 < y) + (y < 0))%type

((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 < x
Ey: 0 < y

((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: x < 0
Ey: y < 0
((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 < x
Ey: 0 < y

((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 < x
Ey: 0 < y

0 < 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: 0 < x
Ey: 0 < y

0 < x * y
apply pos_mult_compat;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: x < 0
Ey: y < 0

((x < 0 < y) + (0 < x) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: x < 0
Ey: y < 0

0 < 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: x * y < 0
Ex: x < 0
Ey: y < 0

0 < x * y
apply neg_mult;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 < x * y -> ((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 < x * y -> ((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y

((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y

0 ≶ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
0 ≶ y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: 0 ≶ x
Ey: 0 ≶ y
((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y

0 ≶ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y

0 * y ≶ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y

0 ≶ x * y
apply pseudo_order_lt_apart;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y

0 ≶ y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y

x * 0 ≶ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y

0 ≶ x * y
apply pseudo_order_lt_apart;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: 0 ≶ x
Ey: 0 ≶ y

((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: ((0 < x) + (x < 0))%type
Ey: ((0 < y) + (y < 0))%type

((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: 0 < x
Ey: y < 0

((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: x < 0
Ey: 0 < y
((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: 0 < x
Ey: y < 0

((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: 0 < x
Ey: y < 0

0 < 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: 0 < x
Ey: y < 0

x * y < 0
apply pos_neg_mult;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: x < 0
Ey: 0 < y

((0 < x) * (0 < y) + (x < 0) * (y < 0))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: x < 0
Ey: 0 < y

0 < 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
Ex: x < 0
Ey: 0 < y

x * y < 0
apply neg_pos_mult;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 < z) -> StrictlyOrderReflecting (mult z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 < z) -> StrictlyOrderReflecting (mult z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (0 < z)
x, y: R
E1: z * x < z * y

x < y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (0 < z)
x, y: R
E1: z * x < z * y

~ (y < x)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (0 < z)
x, y: R
E1: z * x < z * y
y ≶ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (0 < z)
x, y: R
E1: z * x < z * y

~ (y < x)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (0 < z)
x, y: R
E1: z * x < z * y
E2: y < x

Empty
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (0 < z)
x, y: R
E1: z * x < z * y
E2: y < x

z * y < z * x
apply (strictly_order_preserving (z *.));trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (0 < z)
x, y: R
E1: z * x < z * y

y ≶ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (0 < z)
x, y: R
E1: z * x < z * y

z * y ≶ z * x
apply pseudo_order_lt_apart_flip;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 < z) -> StrictlyOrderReflecting (fun y : R => y * z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 < z) -> StrictlyOrderReflecting (fun y : R => y * z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
X: PropHolds (0 < z)

StrictlyOrderReflecting (fun y : R => y * z)
apply strictly_order_reflecting_flip. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (z ≶ 0) -> StrongLeftCancellation mult z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (z ≶ 0) -> StrongLeftCancellation mult z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: PropHolds (z ≶ 0)
x, y: R
E: x ≶ y

z * x ≶ z * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: z ≶ 0
x, y: R
E: x ≶ y

z * x ≶ z * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: ((z < 0) + (0 < z))%type
x, y: R
E: ((x < y) + (y < x))%type

(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: z < 0
x, y: R
E: x < y

(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: 0 < z
x, y: R
E: x < y
(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: z < 0
x, y: R
E: y < x
(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: 0 < z
x, y: R
E: y < x
(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: z < 0
x, y: R
E: x < y

(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: z < 0
x, y: R
E: x < y

z * y < z * x
apply flip_neg_mult_l;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: 0 < z
x, y: R
E: x < y

(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: 0 < z
x, y: R
E: x < y

z * x < z * y
apply (strictly_order_preserving_pos (.*.) z);trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: z < 0
x, y: R
E: y < x

(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: z < 0
x, y: R
E: y < x

z * x < z * y
apply flip_neg_mult_l;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: 0 < z
x, y: R
E: y < x

(((z * x)%mc < (z * y)%mc) + ((z * y)%mc < (z * x)%mc))%type
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
Ez: 0 < z
x, y: R
E: y < x

z * y < z * x
apply (strictly_order_preserving_pos (.*.) z);trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (z ≶ 0) -> StrongRightCancellation mult z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (z ≶ 0) -> StrongRightCancellation mult z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
X: PropHolds (z ≶ 0)

StrongRightCancellation mult z
apply (strong_right_cancel_from_left (.*.)). Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (z ≶ 0) -> LeftCancellation mult z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (z ≶ 0) -> LeftCancellation mult z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
X: PropHolds (z ≶ 0)

LeftCancellation mult z
apply _. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (z ≶ 0) -> RightCancellation mult z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (z ≶ 0) -> RightCancellation mult z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
z: R
X: PropHolds (z ≶ 0)

RightCancellation mult z
apply _. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R

x ≶ 0 -> 0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R

x ≶ 0 -> 0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x ≶ 0

0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: ((x < 0) + (0 < x))%type

0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0

0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: 0 < x
0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0

0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

0 < z * z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z
x * x = 0 + z * z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

0 < z * z
apply pos_mult_compat;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

x * x = 0 + z * z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

x * x = z * z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

x * z + x * x = x * z + z * z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

x * (z + x) = (x + z) * z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

x * 0 = 0 * z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x < 0
z: R
Ez1: 0 < z
Ez2: 0 = x + z

0 = 0
reflexivity.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: 0 < x

0 < x * x
apply pos_mult_compat;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 < x * y -> 0 < y -> 0 < x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 < x * y -> 0 < y -> 0 < x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
X0: 0 < y

0 < x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
X0: 0 < y

0 * y < x * y
rewrite rings.mult_0_l;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 < x * y -> 0 < x -> 0 < y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 < x * y -> 0 < x -> 0 < y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
X0: 0 < x

0 < y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
X0: 0 < x

0 < y * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
X0: 0 < x
0 < x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
X0: 0 < x

0 < y * x
rewrite (commutativity (f:=mult));trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 < x * y
X0: 0 < x

0 < x
trivial. Qed. Context `{PropHolds (10)}.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (0 < 1)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (0 < 1)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

0 < 1
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

0 < 1 * 1
apply square_pos;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (0 < 2)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (0 < 2)
apply _. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (0 < 3)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (0 < 3)
apply _. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (0 < 4)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (0 < 4)
apply _. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

1 < 2
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

1 < 2
apply pos_plus_lt_compat_r, lt_0_1. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

1 < 3
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

1 < 3
apply pos_plus_lt_compat_r, lt_0_2. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

1 < 4
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

1 < 4
apply pos_plus_lt_compat_r, lt_0_3. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

2 < 3
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

2 < 3
apply (strictly_order_preserving (1+)), lt_1_2. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

2 < 4
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

2 < 4
apply (strictly_order_preserving (1+)), lt_1_3. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

3 < 4
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

3 < 4
apply (strictly_order_preserving (1+)), lt_2_3. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (20)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

PropHolds (20)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

20
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Alt: Lt R
H4: PseudoSemiRingOrder Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

02
apply pseudo_order_lt_apart, lt_0_2. Qed. End pseudo_semiring_order. #[export] Hint Extern 7 (PropHolds (0 < 1)) => eapply @lt_0_1 : typeclass_instances. #[export] Hint Extern 7 (PropHolds (0 < 2)) => eapply @lt_0_2 : typeclass_instances. #[export] Hint Extern 7 (PropHolds (0 < 3)) => eapply @lt_0_3 : typeclass_instances. #[export] Hint Extern 7 (PropHolds (0 < 4)) => eapply @lt_0_4 : typeclass_instances. #[export] Hint Extern 7 (PropHolds (20)) => eapply @apart_0_2 : typeclass_instances. Section full_pseudo_semiring_order. Context `{FullPseudoSemiRingOrder R} `{!IsSemiCRing R}. (* Add Ring Rf : (stdlib_semiring_theory R). *)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

FullPseudoOrder (Ale : Le R) (Alt : Lt R)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

FullPseudoOrder (Ale : Le R) (Alt : Lt R)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

is_mere_relation R Ale
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
PseudoOrder Alt
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
forall x y : R, x ≤ y <-> ~ (y < x)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

is_mere_relation R Ale
apply _.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PseudoOrder Alt
apply _.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall x y : R, x ≤ y <-> ~ (y < x)
apply full_pseudo_srorder_le_iff_not_lt_flip. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

SemiRingOrder (Ale : Le R)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

SemiRingOrder (Ale : Le R)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall x y : R, x ≤ y -> {z : R & y = x + z}
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
forall z : R, OrderEmbedding (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
forall x y : R, PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall x y : R, x ≤ y -> {z : R & y = x + z}
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
E: x ≤ y

{z : R & y = x + z}
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
E: ~ (y < x)

{z : R & y = x + z}
apply pseudo_srorder_partial_minus;trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, OrderEmbedding (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z: R

OrderEmbedding (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z: R

OrderPreserving (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z: R
OrderReflecting (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z: R

OrderPreserving (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: x ≤ y

z + x ≤ z + y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: ~ (y < x)

~ (z + y < z + x)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: ~ (y < x)
E2: z + y < z + x

Empty
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: ~ (y < x)
E2: z + y < z + x

y < x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: ~ (y < x)
E2: z + y < z + x

z + y < z + x
trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z: R

OrderReflecting (plus z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: z + x ≤ z + y

x ≤ y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: ~ (z + y < z + x)

~ (y < x)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: ~ (z + y < z + x)
E2: y < x

Empty
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z, x, y: R
E1: ~ (z + y < z + x)
E2: y < x

z + y < z + x
apply (strictly_order_preserving _);trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall x y : R, PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
Ex: PropHolds (0 ≤ x)
Ey: PropHolds (0 ≤ y)

PropHolds (0 ≤ x * y)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
Ex: ~ (x < 0)
Ey: ~ (y < 0)

~ (x * y < 0)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
Ex: ~ (x < 0)
Ey: ~ (y < 0)
E: x * y < 0

Empty
destruct (neg_mult_decompose x y E) as [[? ?]|[? ?]];auto. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 < z) -> OrderReflecting (mult z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 < z) -> OrderReflecting (mult z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z: R
E: PropHolds (0 < z)

OrderReflecting (mult z)
apply full_pseudo_order_reflecting. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 < z) -> OrderReflecting (fun y : R => y * z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall z : R, PropHolds (0 < z) -> OrderReflecting (fun y : R => y * z)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
z: R
X: PropHolds (0 < z)

OrderReflecting (fun y : R => y * z)
apply order_reflecting_flip. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R

x₁ < y₁ -> x₂ ≤ y₂ -> x₁ + x₂ < y₁ + y₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R

x₁ < y₁ -> x₂ ≤ y₂ -> x₁ + x₂ < y₁ + y₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ ≤ y₂

x₁ + x₂ < y₁ + y₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ ≤ y₂

x₁ + x₂ < y₁ + x₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ ≤ y₂
y₁ + x₂ ≤ y₁ + y₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ ≤ y₂

x₁ + x₂ < y₁ + x₂
apply (strictly_order_preserving (+ x₂));trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ < y₁
E2: x₂ ≤ y₂

y₁ + x₂ ≤ y₁ + y₂
apply (order_preserving (y₁ +));trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R

x₁ ≤ y₁ -> x₂ < y₂ -> x₁ + x₂ < y₁ + y₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R

x₁ ≤ y₁ -> x₂ < y₂ -> x₁ + x₂ < y₁ + y₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ < y₂

x₁ + x₂ < y₁ + y₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ < y₂

x₁ + x₂ ≤ y₁ + x₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ < y₂
y₁ + x₂ < y₁ + y₂
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ < y₂

x₁ + x₂ ≤ y₁ + x₂
apply (order_preserving (+ x₂));trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x₁, y₁, x₂, y₂: R
E1: x₁ ≤ y₁
E2: x₂ < y₂

y₁ + x₂ < y₁ + y₂
apply (strictly_order_preserving (y₁ +));trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x < y -> x < y + z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x < y -> x < y + z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 ≤ z
X0: x < y

x < y + z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 ≤ z
X0: x < y

x + 0 < y + z
apply plus_lt_le_compat;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x < y -> x < z + y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 ≤ z -> x < y -> x < z + y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 ≤ z
X0: x < y

x < z + y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 ≤ z
X0: x < y

x < y + z
apply nonneg_plus_lt_compat_r;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 < z -> x ≤ y -> x < y + z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 < z -> x ≤ y -> x < y + z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 < z
X0: x ≤ y

x < y + z
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 < z
X0: x ≤ y

x + 0 < y + z
apply plus_le_lt_compat;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 < z -> x ≤ y -> x < z + y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R

0 < z -> x ≤ y -> x < z + y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 < z
X0: x ≤ y

x < z + y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y, z: R
X: 0 < z
X0: x ≤ y

x < y + z
apply pos_plus_le_lt_compat_r;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R

0 ≤ x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R

0 ≤ x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R

~ (x * x < 0)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x * x < 0

Empty
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x * x < 0

x * x < 0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x * x < 0

0 < x * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x * x < 0

x ≶ 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x * x < 0
X: IsApart R

x ≶ 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x * x < 0
X: IsApart R

x * x ≶ x * 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x * x < 0
X: IsApart R

x * x ≶ 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x: R
E: x * x < 0
X: IsApart R

x * x < 0
trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 ≤ x * y -> 0 < y -> 0 ≤ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 ≤ x * y -> 0 < y -> 0 ≤ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < y

0 ≤ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < y

0 * y ≤ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < y

0 ≤ x * y
trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 ≤ x * y -> 0 < x -> 0 ≤ y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

0 ≤ x * y -> 0 < x -> 0 ≤ y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < x

0 ≤ y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < x

0 ≤ y * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < x
0 < x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < x

0 ≤ y * x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < x

0 ≤ x * y
trivial.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 0 ≤ x * y
X0: 0 < x

0 < x
trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PropHolds (01)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PropHolds (01)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

01
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

01 * 1
apply square_nonneg. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PropHolds (02)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PropHolds (02)
solve_propholds. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PropHolds (03)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PropHolds (03)
solve_propholds. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PropHolds (04)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

PropHolds (04)
solve_propholds. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

12
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

12
apply nonneg_plus_le_compat_r, le_0_1. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

13
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

13
apply nonneg_plus_le_compat_r, le_0_2. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

14
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

14
apply nonneg_plus_le_compat_r, le_0_3. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

23
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

23
apply (order_preserving (1+)), le_1_2. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

24
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

24
apply (order_preserving (1+)), le_1_3. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

34
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

34
apply (order_preserving (1+)), le_2_3. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

1 ≤ x -> 1 ≤ y -> 1 ≤ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

1 ≤ x -> 1 ≤ y -> 1 ≤ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 ≤ x
X0: 1 ≤ y

1 ≤ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 ≤ x
X0: 1 ≤ y

0 ≤ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 ≤ x
X0: 1 ≤ y

01
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 ≤ x
X0: 1 ≤ y
1 ≤ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 ≤ x
X0: 1 ≤ y

01
apply le_0_1.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 ≤ x
X0: 1 ≤ y

1 ≤ x
trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

1 < x -> 1 ≤ y -> 1 < x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

1 < x -> 1 ≤ y -> 1 < x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 < x
X0: 1 ≤ y

1 < x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 < x
X0: 1 ≤ y

x ≤ x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 < x
X0: 1 ≤ y

0 ≤ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 < x
X0: 1 ≤ y

01
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 < x
X0: 1 ≤ y
1 ≤ x
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 < x
X0: 1 ≤ y

01
apply le_0_1.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 < x
X0: 1 ≤ y

1 ≤ x
apply lt_le;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

1 ≤ x -> 1 < y -> 1 < x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R

1 ≤ x -> 1 < y -> 1 < x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 ≤ x
X0: 1 < y

1 < x * y
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
x, y: R
X: 1 ≤ x
X0: 1 < y

1 < y * x
apply gt_1_ge_1_mult_compat;trivial. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall a b c d : R, 0 ≤ a ≤ b -> 0 < b -> 0 ≤ c < d -> a * c < b * d
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R

forall a b c d : R, 0 ≤ a ≤ b -> 0 < b -> 0 ≤ c < d -> a * c < b * d
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
a, b, c, d: R
E1: 0 ≤ a
E2: a ≤ b
E3: 0 < b
E4: 0 ≤ c
E5: c < d

a * c < b * d
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
a, b, c, d: R
E1: 0 ≤ a
E2: a ≤ b
E3: 0 < b
E4: 0 ≤ c
E5: c < d

a * c ≤ b * c
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
a, b, c, d: R
E1: 0 ≤ a
E2: a ≤ b
E3: 0 < b
E4: 0 ≤ c
E5: c < d
b * c < b * d
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
a, b, c, d: R
E1: 0 ≤ a
E2: a ≤ b
E3: 0 < b
E4: 0 ≤ c
E5: c < d

a * c ≤ b * c
apply mult_le_compat;auto.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
a, b, c, d: R
E1: 0 ≤ a
E2: a ≤ b
E3: 0 < b
E4: 0 ≤ c
E5: c < d

b * c < b * d
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
a, b, c, d: R
E1: 0 ≤ a
E2: a ≤ b
E3: 0 < b
E4: 0 ≤ c
E5: c < d

c < d
trivial. Qed. Context `{PropHolds (10)}.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

~ (10)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

~ (10)
apply lt_not_le_flip, lt_0_1. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

~ (20)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

~ (20)
apply lt_not_le_flip, lt_0_2. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

forall n : nat, 0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

forall n : nat, 0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

00
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
IHn: 0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
01 + (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

00
reflexivity.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
IHn: 0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n

01 + (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
IHn: 0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n

PropHolds (01)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
IHn: 0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
PropHolds (0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n)
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
IHn: 0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n

PropHolds (01)
apply _.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
IHn: 0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n

PropHolds (0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n)
apply IHn. Qed.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

forall n : nat, 0 < (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) (n.+1)%nat
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

forall n : nat, 0 < (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) (n.+1)%nat
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat

0 < (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) (n.+1)%nat
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat

0 < 1 + (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat

0 < 1
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat

0 < 1
solve_propholds.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat

0 ≤ (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n
apply repeat_nat_nonneg. Qed. Local Existing Instance pseudo_order_apart.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

FieldCharacteristic R 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

FieldCharacteristic R 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

forall n : nat, Core.lt 0 n -> (forall m : nat, n <> Core.mul 0 m) <-> (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n ≶ 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

(forall m : nat, 0%nat <> Core.mul 0 m) -> 00
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
00 -> forall m : nat, 0%nat <> Core.mul 0 m
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
(forall m : nat, (n.+1)%nat <> Core.mul 0 m) -> 1 + (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n ≶ 0
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat
1 + (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n ≶ 0 -> forall m : nat, (n.+1)%nat <> Core.mul 0 m
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

(forall m : nat, 0%nat <> Core.mul 0 m) -> 00
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
E': forall m : nat, 0%nat <> Core.mul 0 m

00
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
E': forall m : nat, 0%nat <> Core.mul 0 m

0%nat = Core.mul 0 0
reflexivity.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)

00 -> forall m : nat, 0%nat <> Core.mul 0 m
intros E';apply (irreflexivity _) in E';destruct E'.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat

(forall m : nat, (n.+1)%nat <> Core.mul 0 m) -> 1 + (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n ≶ 0
intros _;apply apart_iff_total_lt;right;apply repeat_nat_pos.
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n: nat

1 + (fix F (m : nat) : R := match m with | 0%nat => 0 | (m'.+1)%nat => 1 + F m' end) n ≶ 0 -> forall m : nat, (n.+1)%nat <> Core.mul 0 m
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n, m: nat

(n.+1)%nat <> 0%nat
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n, m: nat
E: (n.+1)%nat = 0%nat

Empty
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n, m: nat
E: Unit = Empty

Empty
R: Type
H: Apart R
H0: Plus R
H1: Mult R
H2: Zero R
H3: One R
Ale: Le R
Alt: Lt R
H4: FullPseudoSemiRingOrder Ale Alt
IsSemiCRing0: IsSemiCRing R
H5: PropHolds (10)
n, m: nat
E: Unit = Empty

Unit
trivial. Qed. End full_pseudo_semiring_order. (* Due to bug #2528 *) #[export] Hint Extern 7 (PropHolds (01)) => eapply @le_0_1 : typeclass_instances. #[export] Hint Extern 7 (PropHolds (02)) => eapply @le_0_2 : typeclass_instances. #[export] Hint Extern 7 (PropHolds (03)) => eapply @le_0_3 : typeclass_instances. #[export] Hint Extern 7 (PropHolds (04)) => eapply @le_0_4 : typeclass_instances. Section dec_semiring_order. (* Maybe these assumptions can be weakened? *) Context `{SemiRingOrder R} `{Apart R} `{!TrivialApart R} `{!NoZeroDivisors R} `{!TotalRelation (≤)} `{DecidablePaths R}. Context `{Rlt : Lt R} `{is_mere_relation R lt} (lt_correct : forall x y, x < y <-> x ≤ y /\ x <> y). Instance dec_srorder_fullpseudo : FullPseudoOrder _ _ := dec_full_pseudo_order lt_correct. Local Existing Instance pseudo_order_apart.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

PseudoSemiRingOrder lt
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

PseudoSemiRingOrder lt
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

forall x y : R, ~ (y < x) -> {z : R & y = x + z}
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
forall z : R, StrictOrderEmbedding (plus z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
StrongBinaryExtensionality mult
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
forall x y : R, PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x * y)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

forall x y : R, ~ (y < x) -> {z : R & y = x + z}
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E: ~ (y < x)

{z : R & y = x + z}
apply srorder_partial_minus, not_lt_le_flip;trivial.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

forall z : R, StrictOrderEmbedding (plus z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z: R

StrictOrderEmbedding (plus z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z: R

StrictlyOrderPreserving (plus z)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E: x < y

z + x < z + y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E: ((x ≤ y) * (x <> y))%type

(((z + x)%mc ≤ (z + y)%mc) * ((z + x)%mc <> (z + y)%mc))%type
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E2a: x ≤ y
E2b: x <> y

(((z + x)%mc ≤ (z + y)%mc) * ((z + x)%mc <> (z + y)%mc))%type
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E2a: x ≤ y
E2b: x <> y

z + x ≤ z + y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E2a: x ≤ y
E2b: x <> y
z + x <> z + y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E2a: x ≤ y
E2b: x <> y

z + x ≤ z + y
apply (order_preserving (z+));trivial.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E2a: x ≤ y
E2b: x <> y

z + x <> z + y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E2a: x ≤ y
E2b: x <> y
E3: z + x = z + y

Empty
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
z, x, y: R
E2a: x ≤ y
E2b: x <> y
E3: z + x = z + y

x = y
apply (left_cancellation (+) z);trivial.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

StrongBinaryExtensionality mult
apply (apartness.dec_strong_binary_morphism (.*.)).
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

forall x y : R, PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x * y)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E1: PropHolds (0 < x)
E2: PropHolds (0 < y)

PropHolds (0 < x * y)
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E1: ((0 ≤ x) * (0 <> x))%type
E2: ((0 ≤ y) * (0 <> y))%type

((0 ≤ (x * y)%mc) * (0 <> (x * y)%mc))%type
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E1a: 0 ≤ x
E1b: 0 <> x
E2a: 0 ≤ y
E2b: 0 <> y

((0 ≤ (x * y)%mc) * (0 <> (x * y)%mc))%type
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E1a: 0 ≤ x
E1b: 0 <> x
E2a: 0 ≤ y
E2b: 0 <> y

0 ≤ x * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E1a: 0 ≤ x
E1b: 0 <> x
E2a: 0 ≤ y
E2b: 0 <> y
0 <> x * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E1a: 0 ≤ x
E1b: 0 <> x
E2a: 0 ≤ y
E2b: 0 <> y

0 ≤ x * y
apply nonneg_mult_compat;trivial.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E1a: 0 ≤ x
E1b: 0 <> x
E2a: 0 ≤ y
E2b: 0 <> y

0 <> x * y
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)
x, y: R
E1a: 0 ≤ x
E1b: 0 <> x
E2a: 0 ≤ y
E2b: 0 <> y

x * y <> 0
apply mult_ne_0; apply symmetric_neq;trivial. Qed.
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

FullPseudoSemiRingOrder le lt
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

FullPseudoSemiRingOrder le lt
R: Type
H: Plus R
H0: Mult R
H1: Zero R
H2: One R
Ale: Le R
H3: SemiRingOrder Ale
H4: Apart R
TrivialApart0: TrivialApart R
NoZeroDivisors0: NoZeroDivisors R
TotalRelation0: TotalRelation le
H5: DecidablePaths R
Rlt: Lt R
is_mere_relation0: is_mere_relation R lt
lt_correct: forall x y : R, x < y <-> (x ≤ y) * (x <> y)

forall x y : R, x ≤ y <-> ~ (y < x)
apply le_iff_not_lt_flip. Qed. End dec_semiring_order. Section another_semiring. Context `{SemiRingOrder R1}.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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) -> (forall x y : R2, x ≤ y -> {z : R2 & y = x + z}) -> SemiRingOrder R2le
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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) -> (forall x y : R2, x ≤ y -> {z : R2 & y = x + z}) -> SemiRingOrder R2le
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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}) -> SemiRingOrder R2le
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le

(forall x y : R2, x ≤ y -> {z : R2 & y = x + z}) -> SemiRingOrder R2le
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}

forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z: R2
OrderPreserving (plus z)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z: R2
OrderReflecting (plus z)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
forall x y : R2, PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}

forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
assumption.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z: R2

OrderPreserving (plus z)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: x ≤ y

z + x ≤ z + y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: x ≤ y

f (z + x) ≤ f (z + y)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: x ≤ y

f z + f x ≤ f z + f y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: x ≤ y

x ≤ y
trivial.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z: R2

OrderReflecting (plus z)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: z + x ≤ z + y

x ≤ y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: z + x ≤ z + y

f x ≤ f y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: z + x ≤ z + y

f z + f x ≤ f z + f y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: z + x ≤ z + y

f (z + x) ≤ f (z + y)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
z, x, y: R2
X1: z + x ≤ z + y

z + x ≤ z + y
trivial.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}

forall x y : R2, PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
x, y: R2
X1: PropHolds (0 ≤ x)
X2: PropHolds (0 ≤ y)

PropHolds (0 ≤ x * y)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
x, y: R2
X1: PropHolds (0 ≤ x)
X2: PropHolds (0 ≤ y)

f 0 ≤ f (x * y)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
R2: Type
Aplus: Plus R2
Amult: Mult R2
Azero: Zero R2
Aone: One R2
H4: IsSemiCRing 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: PartialOrder R2le
X0: forall x y : R2, x ≤ y -> {z : R2 & y = x + z}
x, y: R2
X1: PropHolds (0 ≤ x)
X2: PropHolds (0 ≤ y)

0 ≤ f x * f y
apply nonneg_mult_compat; rewrite <-(preserves_0 (f:=f)); apply P;trivial. Qed. Context `{!IsSemiCRing R1} `{SemiRingOrder R2} `{!IsSemiCRing R2} `{!IsSemiRingPreserving (f : R1 -> R2)}. (* If a morphism agrees on the positive cone then it is order preserving *)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)

(forall x : R1, 0 ≤ x -> 0 ≤ f x) -> OrderPreserving f
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)

(forall x : R1, 0 ≤ x -> 0 ≤ f x) -> OrderPreserving f
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x

OrderPreserving f
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x

OrderPreserving f
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x
x, y: R1
F: x ≤ y

f x ≤ f y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x
x, y: R1
F: x ≤ y
z: R1
Ez1: 0 ≤ z
Ez2: y = x + z

f x ≤ f y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x
x, y: R1
F: x ≤ y
z: R1
Ez1: 0 ≤ z
Ez2: y = x + z

0 ≤ f z
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x
x, y: R1
F: x ≤ y
z: R1
Ez1: 0 ≤ z
Ez2: y = x + z
f y = f x + f z
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x
x, y: R1
F: x ≤ y
z: R1
Ez1: 0 ≤ z
Ez2: y = x + z

0 ≤ f z
apply E;trivial.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x
x, y: R1
F: x ≤ y
z: R1
Ez1: 0 ≤ z
Ez2: y = x + z

f y = f x + f z
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 ≤ x -> 0 ≤ f x
x, y: R1
F: x ≤ y
z: R1
Ez1: 0 ≤ z
Ez2: y = x + z

f x + f z = f x + f z
trivial. Qed.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1

PropHolds (0 ≤ x) -> PropHolds (0 ≤ f x)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1

PropHolds (0 ≤ x) -> PropHolds (0 ≤ f x)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1
X: PropHolds (0 ≤ x)

PropHolds (0 ≤ f x)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1
X: PropHolds (0 ≤ x)

PropHolds (f 0 ≤ f x)
apply (order_preserving f);trivial. Qed.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1

x ≤ 0 -> f x ≤ 0
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1

x ≤ 0 -> f x ≤ 0
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1
X: x ≤ 0

f x ≤ 0
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1
X: x ≤ 0

f x ≤ f 0
apply (order_preserving f);trivial. Qed.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1

1 ≤ x -> 1 ≤ f x
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1

1 ≤ x -> 1 ≤ f x
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1
X: 1 ≤ x

1 ≤ f x
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1
X: 1 ≤ x

f 1 ≤ f x
apply (order_preserving f);trivial. Qed.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1

x ≤ 1 -> f x ≤ 1
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1

x ≤ 1 -> f x ≤ 1
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1
X: x ≤ 1

f x ≤ 1
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Ale: Le R1
H3: SemiRingOrder Ale
IsSemiCRing0: IsSemiCRing R1
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Ale0: Le R2
H8: SemiRingOrder Ale0
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
OrderPreserving0: OrderPreserving f
x: R1
X: x ≤ 1

f x ≤ f 1
apply (order_preserving f);trivial. Qed. End another_semiring. Section another_semiring_strict. Context `{StrictSemiRingOrder R1} `{StrictSemiRingOrder R2} `{!IsSemiCRing R1} `{!IsSemiCRing R2} `{!IsSemiRingPreserving (f : R1 -> R2)}.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)

(forall x : R1, 0 < x -> 0 < f x) -> StrictlyOrderPreserving f
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)

(forall x : R1, 0 < x -> 0 < f x) -> StrictlyOrderPreserving f
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x

StrictlyOrderPreserving f
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x

StrictlyOrderPreserving f
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x
x, y: R1
F: x < y

f x < f y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x
x, y: R1
F: x < y
z: R1
Ez1: 0 < z
Ez2: y = x + z

f x < f y
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x
x, y: R1
F: x < y
z: R1
Ez1: 0 < z
Ez2: y = x + z

0 < f z
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x
x, y: R1
F: x < y
z: R1
Ez1: 0 < z
Ez2: y = x + z
f y = f x + f z
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x
x, y: R1
F: x < y
z: R1
Ez1: 0 < z
Ez2: y = x + z

0 < f z
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x
x, y: R1
F: x < y
z: R1
Ez1: 0 < z
Ez2: y = x + z

0 < z
trivial.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x
x, y: R1
F: x < y
z: R1
Ez1: 0 < z
Ez2: y = x + z

f y = f x + f z
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
E: forall x : R1, 0 < x -> 0 < f x
x, y: R1
F: x < y
z: R1
Ez1: 0 < z
Ez2: y = x + z

f x + f z = f x + f z
trivial. Qed.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1

PropHolds (0 < x) -> PropHolds (0 < f x)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1

PropHolds (0 < x) -> PropHolds (0 < f x)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1
X: PropHolds (0 < x)

PropHolds (0 < f x)
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1
X: PropHolds (0 < x)

PropHolds (f 0 < f x)
apply (strictly_order_preserving f);trivial. Qed.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1

x < 0 -> f x < 0
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1

x < 0 -> f x < 0
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1
X: x < 0

f x < 0
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1
X: x < 0

f x < f 0
apply (strictly_order_preserving f);trivial. Qed.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1

1 < x -> 1 < f x
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1

1 < x -> 1 < f x
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1
X: 1 < x

1 < f x
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1
X: 1 < x

f 1 < f x
apply (strictly_order_preserving f);trivial. Qed.
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1

x < 1 -> f x < 1
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1

x < 1 -> f x < 1
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1
X: x < 1

f x < 1
R1: Type
H: Plus R1
H0: Mult R1
H1: Zero R1
H2: One R1
Alt: Lt R1
H3: StrictSemiRingOrder Alt
R2: Type
H4: Plus R2
H5: Mult R2
H6: Zero R2
H7: One R2
Alt0: Lt R2
H8: StrictSemiRingOrder Alt0
IsSemiCRing0: IsSemiCRing R1
IsSemiCRing1: IsSemiCRing R2
f: R1 -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R1 -> R2)
StrictlyOrderPreserving0: StrictlyOrderPreserving f
x: R1
X: x < 1

f x < f 1
apply (strictly_order_preserving f);trivial. Qed. End another_semiring_strict. (* Due to bug #2528 *) #[export] Hint Extern 15 (PropHolds (_ ≤ _ _)) => eapply @preserves_nonneg : typeclass_instances. #[export] Hint Extern 15 (PropHolds (_ < _ _)) => eapply @preserves_pos : typeclass_instances. (* Oddly enough, the above hints do not work for goals of the following shape? *) #[export] Hint Extern 15 (PropHolds (_ ≤ '_)) => eapply @preserves_nonneg : typeclass_instances. #[export] Hint Extern 15 (PropHolds (_ < '_)) => eapply @preserves_pos : typeclass_instances.