Require Import
  HoTT.Types.Sigma.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import
  HoTT.Classes.theory.naturals.
Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.theory.rings
  HoTT.Classes.orders.rings
  HoTT.Classes.implementations.peano_naturals.
Require Export
  HoTT.Classes.orders.nat_int.

Generalizable Variables N R Rle Rlt f.

Section naturals_order.
Context `{Funext} `{Univalence}.
Context `{Naturals N} `{!TrivialApart N}.

Instance nat_nonneg x : PropHolds (0 ≤ x).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
PropHolds (0 ≤ x)
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
PropHolds (0 ≤ x) apply (to_semiring_nonneg (f:=id)). Qed.

Lemma nat_le_plus {x y: N}: x ≤ y <-> exists z, y = x + z.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
x ≤ y <-> {z : N & y = x + z}
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
x ≤ y <-> {z : N & y = x + z}
split; intros E.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: x ≤ y
{z : N & y = x + z}
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: {z : N & y = x + z}
x ≤ y
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: x ≤ y
{z : N & y = x + z} destruct (decompose_le E) as [z [Ez1 Ez2]].
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: x ≤ y
z: N
Ez1: 0 ≤ z
Ez2: y = x + z
{z : N & y = x + z} exists z.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: x ≤ y
z: N
Ez1: 0 ≤ z
Ez2: y = x + z
y = x + z trivial.
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: {z : N & y = x + z}
x ≤ y destruct E as [z Ez].
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y, z: N
Ez: y = x + z
x ≤ y
  apply compose_le with z; [solve_propholds | trivial].
Qed.

Lemma nat_not_neg x : ~(x < 0).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
~ (x < 0)
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
~ (x < 0) apply le_not_lt_flip, nat_nonneg. Qed.

Lemma nat_0_or_pos x : x = 0 |_| 0 < x.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
((x = 0) + (0 < x))%type
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
((x = 0) + (0 < x))%type
destruct (trichotomy (<) 0 x) as [?|[?|?]]; auto.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
p: 0 = x
((x = 0) + (0 < x))%type
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
l: x < 0
((x = 0) + (0 < x))%type
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
p: 0 = x
((x = 0) + (0 < x))%type left;symmetry;trivial.
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
l: x < 0
((x = 0) + (0 < x))%type destruct (nat_not_neg x).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
l: x < 0
x < 0 trivial.
Qed.

Lemma nat_0_or_ge_1 x : x = 0 |_| 1 ≤ x.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
((x = 0) + (1 ≤ x))%type
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
((x = 0) + (1 ≤ x))%type
destruct (nat_0_or_pos x);auto.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
l: 0 < x
((x = 0) + (1 ≤ x))%type
right;apply pos_ge_1.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
l: 0 < x
0 < x trivial.
Qed.

Lemma nat_ne_0_pos x : x <> 0 <-> 0 < x.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
x <> 0 <-> 0 < x
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
x <> 0 <-> 0 < x
split.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
x <> 0 -> 0 < x
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
0 < x -> x <> 0
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
x <> 0 -> 0 < x destruct (nat_0_or_pos x); auto.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
p: x = 0
x <> 0 -> 0 < x
  intros E;destruct E;trivial.
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
0 < x -> x <> 0 intros E1 E2.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
E1: 0 < x
E2: x = 0
Empty rewrite E2 in E1.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
E1: 0 < 0
E2: x = 0
Empty destruct (irreflexivity (<) 0).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
E1: 0 < 0
E2: x = 0
0 < 0 trivial.
Qed.

Lemma nat_ne_0_ge_1 x : x <> 0 <-> 1 ≤ x.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
x <> 0 <-> 1 ≤ x
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
x <> 0 <-> 1 ≤ x
etransitivity.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
x <> 0 <-> ?Goal
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
?Goal <-> 1 ≤ x
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
x <> 0 <-> ?Goal apply nat_ne_0_pos.
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x: N
0 < x <-> 1 ≤ x apply pos_ge_1.
Qed.

#[export] Instance orderreflecting_left_mult : forall (z : N), PropHolds (z <> 0) -> OrderReflecting (z *.).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
forall z : N,
PropHolds (z <> 0) -> OrderReflecting (mult z)
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
forall z : N,
PropHolds (z <> 0) -> OrderReflecting (mult z)
intros z ?.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
z: N
X: PropHolds (z <> 0)
OrderReflecting (mult z) red.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
z: N
X: PropHolds (z <> 0)
forall x y : N, z * x ≤ z * y -> x ≤ y apply (order_reflecting_pos (.*.) z).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
z: N
X: PropHolds (z <> 0)
0 < z
apply nat_ne_0_pos.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
z: N
X: PropHolds (z <> 0)
z <> 0 trivial.
Qed.

#[export] Instance slow_nat_le_dec: forall x y: N, Decidable (x ≤ y) | 10.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
forall x y : N, Decidable (x ≤ y)
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
forall x y : N, Decidable (x ≤ y)
intros x y.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
Decidable (x ≤ y)
destruct (nat_le_dec (naturals_to_semiring _ nat x) (naturals_to_semiring _ nat y))
as [E | E].
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: naturals_to_semiring N nat x
≤ naturals_to_semiring N nat y
Decidable (x ≤ y)
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: ~
(naturals_to_semiring N nat x
 ≤ naturals_to_semiring N nat y)
Decidable (x ≤ y)
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: naturals_to_semiring N nat x
≤ naturals_to_semiring N nat y
Decidable (x ≤ y) left.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: naturals_to_semiring N nat x
≤ naturals_to_semiring N nat y
x ≤ y
  apply (order_reflecting (naturals_to_semiring N nat)).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: naturals_to_semiring N nat x
≤ naturals_to_semiring N nat y
naturals_to_semiring N nat x
≤ naturals_to_semiring N nat y exact E.
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: ~
(naturals_to_semiring N nat x
 ≤ naturals_to_semiring N nat y)
Decidable (x ≤ y) right.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: ~
(naturals_to_semiring N nat x
 ≤ naturals_to_semiring N nat y)
~ (x ≤ y) intros E'.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: ~
(naturals_to_semiring N nat x
 ≤ naturals_to_semiring N nat y)
E': x ≤ y
Empty apply E.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: ~
(naturals_to_semiring N nat x
 ≤ naturals_to_semiring N nat y)
E': x ≤ y
naturals_to_semiring N nat x
≤ naturals_to_semiring N nat y
  apply order_preserving;trivial.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
x, y: N
E: ~
(naturals_to_semiring N nat x
 ≤ naturals_to_semiring N nat y)
E': x ≤ y
OrderPreserving (naturals_to_semiring N nat) exact _.
Qed.

Section another_ring.
  Context `{IsCRing R} `{Apart R} `{!FullPseudoSemiRingOrder (A:=R) Rle Rlt}
    `{!IsSemiRingPreserving (f : N -> R)}.

  Lemma negate_to_ring_nonpos n : -f n ≤ 0.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
H3: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Rle
  Rlt
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
n: N
- f n ≤ 0
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
H3: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Rle
  Rlt
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
n: N
- f n ≤ 0 apply flip_nonneg_negate.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
H3: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Rle
  Rlt
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
n: N
0 ≤ f n apply to_semiring_nonneg. Qed.

  Lemma between_to_ring n : -f n ≤ f n.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
H3: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Rle
  Rlt
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
n: N
- f n ≤ f n
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
H3: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Rle
  Rlt
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
n: N
- f n ≤ f n apply between_nonneg.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
TrivialApart0: TrivialApart N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
H3: Apart R
Rle: Le R
Rlt: Lt R
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Rle
  Rlt
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
n: N
0 ≤ f n apply to_semiring_nonneg. Qed.
End another_ring.
End naturals_order.

#[export]
Hint Extern 20 (PropHolds (_ ≤ _)) => eapply @nat_nonneg : typeclass_instances.