Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.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 VariablesR Rlt f.Sectionsemiring_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
forallz : R, OrderEmbedding (funy : 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
forallz : R, OrderEmbedding (funy : 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 (funy : 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 (funy : 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 (funy : 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 (funy : R => y + z)
exact 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 (funy : R => y + z)
exact 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
forallz : 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
forallz : 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
applysymmetry;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
forallz : 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
forallz : 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
(funr : 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
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 = plus x z))%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 = plus x z))%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 = plus x z))%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 = plus x z))%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 = plus x z))%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
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
forallz : R,
PropHolds (0 ≤ z) ->
OrderPreserving (funy : 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
forallz : R,
PropHolds (0 ≤ z) ->
OrderPreserving (funy : 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 (funy : R => y * z)
exact 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
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₂
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
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.Endsemiring_order.(* Due to bug #2528 *)#[export]
Hint Extern7 (PropHolds (0 ≤ _ + _)) =>
eapply @nonneg_plus_compat : typeclass_instances.Sectionstrict_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
forallz : R,
StrictOrderEmbedding (funy : 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
forallz : R,
StrictOrderEmbedding (funy : 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 (funy : 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 (funy : 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 (funy : 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 (funy : R => y + z)
exact 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 (funy : R => y + z)
exact 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
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₂
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
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 = plus x z))%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 = plus x z))%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 = plus x z))%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 = plus x z))%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 = plus x z))%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
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
forallz : R,
PropHolds (0 < z) ->
StrictlyOrderPreserving (funy : 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
forallz : R,
PropHolds (0 < z) ->
StrictlyOrderPreserving (funy : 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 (funy : R => y * z)
exact 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
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
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₂
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
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.Endstrict_semiring_order.(* Due to bug #2528 *)#[export]
Hint Extern7 (PropHolds (0 < _ + _)) =>
eapply @pos_plus_compat : typeclass_instances.Sectionpseudo_semiring_order.Context `{PseudoSemiRingOrder R} `{!IsSemiCRing R}.(* Add Ring Rp : (stdlib_semiring_theory R). *)Local Existing Instancepseudo_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
forallxy : 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
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
forallz : 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: forallz : 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
forallz : 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)
exact 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: forallz : 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
forallz : 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
forallz : 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
((plus z x < plus z y) + (plus z y < plus z x))%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
forallz : 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
forallz : 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
exact (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)
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)
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
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
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
forallz : R,
PropHolds (0 < z) ->
StrictlyOrderReflecting (funy : 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
forallz : R,
PropHolds (0 < z) ->
StrictlyOrderReflecting (funy : 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 (funy : R => y * z)
exact 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
forallz : 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
forallz : 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
((mult z x < mult z y) + (mult z y < mult z x))%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
((mult z x < mult z y) + (mult z y < mult z x))%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
((mult z x < mult z y) + (mult z y < mult z x))%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
((mult z x < mult z y) + (mult z y < mult z x))%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
((mult z x < mult z y) + (mult z y < mult z x))%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
((mult z x < mult z y) + (mult z y < mult z x))%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
((mult z x < mult z y) + (mult z y < mult z x))%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
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
((mult z x < mult z y) + (mult z y < mult z x))%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
((mult z x < mult z y) + (mult z y < mult z x))%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
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
forallz : 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
forallz : 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
exact (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
forallz : 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
forallz : 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
exact _.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
forallz : 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
forallz : 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
exact _.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 (1 ≶ 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 H5: PropHolds (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
PropHolds (0 < 2)
exact _.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 (1 ≶ 0)
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 (1 ≶ 0)
PropHolds (0 < 3)
exact _.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 (1 ≶ 0)
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 (1 ≶ 0)
PropHolds (0 < 4)
exact _.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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 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
forallxy : 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
forallz : 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
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
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)
exact 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
forallz : R,
PropHolds (0 < z) ->
OrderReflecting (funy : 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
forallz : R,
PropHolds (0 < z) ->
OrderReflecting (funy : 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 (funy : R => y * z)
exact 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₂
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 (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
PropHolds (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
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
0 ≤ 1 * 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 (0 ≤ 2)
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 (0 ≤ 2)
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 (0 ≤ 3)
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 (0 ≤ 3)
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 (0 ≤ 4)
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 (0 ≤ 4)
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
1 ≤ 2
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
1 ≤ 2
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
1 ≤ 3
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
1 ≤ 3
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
1 ≤ 4
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
1 ≤ 4
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
2 ≤ 3
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
2 ≤ 3
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
2 ≤ 4
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
2 ≤ 4
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
3 ≤ 4
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
3 ≤ 4
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
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
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 ≤ 1
exact 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
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
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 ≤ 1
exact 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
forallabcd : 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
forallabcd : 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 (1 ≶ 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 (1 ≶ 0)
~ (1 ≤ 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 (1 ≶ 0)
~ (1 ≤ 0)
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 (1 ≶ 0)
~ (2 ≤ 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 (1 ≶ 0)
~ (2 ≤ 0)
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 (1 ≶ 0)
foralln : 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 (1 ≶ 0)
foralln : 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 (1 ≶ 0)
0 ≤ 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 (1 ≶ 0) n: nat IHn: 0
≤ (fix F (m : nat) : R :=
match m with
| 0%nat => 0
| m'.+1%nat => 1 + F m'
end) n
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 (1 ≶ 0)
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 (1 ≶ 0) n: nat IHn: 0
≤ (fix F (m : nat) : R :=
match m with
| 0%nat => 0
| m'.+1%nat => 1 + F m'
end) n
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 (1 ≶ 0) 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 ≤ 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 (1 ≶ 0) 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 (1 ≶ 0) 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 ≤ 1)
exact _.
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 (1 ≶ 0) 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)
exact 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 (1 ≶ 0)
foralln : 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 (1 ≶ 0)
foralln : 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 (1 ≶ 0) 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 (1 ≶ 0) 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 (1 ≶ 0) 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 (1 ≶ 0) 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 (1 ≶ 0) 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 (1 ≶ 0) 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 (1 ≶ 0)
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 (1 ≶ 0)
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 (1 ≶ 0)
foralln : nat,
Core.lt 0 n ->
(forallm : nat, n <> Core.nat_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 (1 ≶ 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 (1 ≶ 0)
0 ≶ 0 -> forallm : nat, 0%nat <> Core.nat_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 (1 ≶ 0) n: nat
(forallm : nat, n.+1%nat <> Core.nat_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 (1 ≶ 0) n: nat
1 +
(fix F (m : nat) : R :=
match m with
| 0%nat => 0
| m'.+1%nat => 1 + F m'
end) n ≶ 0 ->
forallm : nat, n.+1%nat <> Core.nat_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 (1 ≶ 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 (1 ≶ 0) E': forallm : nat, 0%nat <> Core.nat_mul 0 m
0 ≶ 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 (1 ≶ 0) E': forallm : nat, 0%nat <> Core.nat_mul 0 m
0%nat = Core.nat_mul 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 (1 ≶ 0)
0 ≶ 0 -> forallm : nat, 0%nat <> Core.nat_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 (1 ≶ 0) n: nat
(forallm : nat, n.+1%nat <> Core.nat_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 (1 ≶ 0) n: nat
1 +
(fix F (m : nat) : R :=
match m with
| 0%nat => 0
| m'.+1%nat => 1 + F m'
end) n ≶ 0 ->
forallm : nat, n.+1%nat <> Core.nat_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 (1 ≶ 0) 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 (1 ≶ 0) 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 (1 ≶ 0) 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 (1 ≶ 0) n, m: nat E: Unit = Empty
Unit
trivial.Qed.Endfull_pseudo_semiring_order.(* Due to bug #2528 *)#[export]
Hint Extern7 (PropHolds (0 ≤ 1)) => eapply @le_0_1 : typeclass_instances.#[export]
Hint Extern7 (PropHolds (0 ≤ 2)) => eapply @le_0_2 : typeclass_instances.#[export]
Hint Extern7 (PropHolds (0 ≤ 3)) => eapply @le_0_3 : typeclass_instances.#[export]
Hint Extern7 (PropHolds (0 ≤ 4)) => eapply @le_0_4 : typeclass_instances.Sectiondec_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 : forallxy, x < y <-> x ≤ y /\ x <> y).Instancedec_srorder_fullpseudo
: FullPseudoOrder _ _ := dec_full_pseudo_order lt_correct.Local Existing Instancepseudo_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: forallxy : 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: forallxy : 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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y)
forallxy : 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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y)
forallz : 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: forallxy : 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: forallxy : R,
x < y <-> (x ≤ y) * (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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y)
forallxy : 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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y) x, y: R E: ~ (y < x)
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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y)
forallz : 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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y) z, x, y: R E: ((x ≤ y) * (x <> y))%type
((plus z x ≤ plus z y) * (plus z x <> plus z y))%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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y) z, x, y: R E2a: x ≤ y E2b: x <> y
((plus z x ≤ plus z y) * (plus z x <> plus z y))%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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : R,
x < y <-> (x ≤ y) * (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: forallxy : R,
x < y <-> (x ≤ y) * (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: forallxy : 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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y) x, y: R E1: ((0 ≤ x) * (0 <> x))%type E2: ((0 ≤ y) * (0 <> y))%type
((0 ≤ mult x y) * (0 <> mult x y))%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: forallxy : R,
x < y <-> (x ≤ y) * (x <> y) x, y: R E1a: 0 ≤ x E1b: 0 <> x E2a: 0 ≤ y E2b: 0 <> y
((0 ≤ mult x y) * (0 <> mult x y))%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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : 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: forallxy : R,
x < y <-> (x ≤ 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
(forallxy : R2, x ≤ y <-> f x ≤ f y) ->
(forallxy : 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
(forallxy : R2, x ≤ y <-> f x ≤ f y) ->
(forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y
(forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le
(forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : R2, x ≤ y -> {z : R2 & y = x + z}
forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : R2, x ≤ y -> {z : R2 & y = x + z}
forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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: forallxy : R2, x ≤ y <-> f x ≤ f y X: PartialOrder R2le X0: forallxy : 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)
(forallx : 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)
(forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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
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)
(forallx : 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)
(forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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: forallx : 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.Endanother_semiring_strict.(* Due to bug #2528 *)#[export]
Hint Extern15 (PropHolds (_ ≤ _ _)) =>
eapply @preserves_nonneg : typeclass_instances.#[export]
Hint Extern15 (PropHolds (_ < _ _)) =>
eapply @preserves_pos : typeclass_instances.(* Oddly enough, the above hints do not work for goals of the following shape? *)#[export]
Hint Extern15 (PropHolds (_ ≤ '_)) =>
eapply @preserves_nonneg : typeclass_instances.#[export]
Hint Extern15 (PropHolds (_ < '_)) =>
eapply @preserves_pos : typeclass_instances.