Require ImportRequire Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.theory.naturals
  HoTT.Classes.theory.rings.
Require Export
  HoTT.Classes.orders.semirings.

Generalizable Variables N R f.

Section Univ.
Context `{Funext} `{Univalence}.

(**
We axiomatize the order on the naturals and the integers as a non trivial
pseudo semiring order that satisfies the biinduction principle. We prove
some results that hold for the order on the naturals and the integers.
In particular, we show that given another non trivial pseudo semiring order
(that not necessarily has to satisfy the biinduction principle, for example
the rationals or the reals), any morphism to it is an order embedding.
*)
Lemma to_semiring_nonneg `{FullPseudoSemiRingOrder N}
  `{!NaturalsToSemiRing N} `{!Naturals N} `{FullPseudoSemiRingOrder R}
  `{!IsSemiCRing R}
  `{!IsSemiRingPreserving (f : N -> R)} n : 0 ≤ f n.
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
n: N
0 ≤ f n
Proof.
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
n: N
0 ≤ f n
revert n.
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
forall n : N, 0 ≤ f n apply naturals.induction.
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
0 ≤ f 0
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
forall n : N, 0 ≤ f n -> 0 ≤ f (1 + n)
-
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
0 ≤ f 0 rewrite (preserves_0 (f:=f)).
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
0 ≤ 0
  reflexivity.
-
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
forall n : N, 0 ≤ f n -> 0 ≤ f (1 + n) intros n E.
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
n: N
E: 0 ≤ f n
0 ≤ f (1 + n)
  rewrite (preserves_plus (f:=f)), (preserves_1 (f:=f)).
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
n: N
E: 0 ≤ f n
0 ≤ 1 + f n
  apply nonneg_plus_compat.
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
n: N
E: 0 ≤ f n
PropHolds (0 ≤ 1)
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
n: N
E: 0 ≤ f n
PropHolds (0 ≤ f n)
  +
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
n: N
E: 0 ≤ f n
PropHolds (0 ≤ 1) solve_propholds.
  +
H: Funext
H0: Univalence
N: Type
H1: Apart N
H2: Plus N
H3: Mult N
H4: Zero N
H5: One N
Ale: Le N
Alt: Lt N
H6: FullPseudoSemiRingOrder Ale Alt
NaturalsToSemiRing0: NaturalsToSemiRing N
Naturals0: Naturals N
R: Type
H7: Apart R
H8: Plus R
H9: Mult R
H10: Zero R
H11: One R
Ale0: Le R
Alt0: Lt R
H12: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving (f : N -> R)
n: N
E: 0 ≤ f n
PropHolds (0 ≤ f n) trivial.
Qed.

Section nat_int_order.
Context `{Naturals N} `{Apart N} `{Le N} `{Lt N} `{!FullPseudoSemiRingOrder le lt}
  `{FullPseudoSemiRingOrder R} `{!IsSemiCRing R}
  `{!Biinduction R} `{PropHolds (1 ≶ 0)}.

(* Add Ring R : (stdlib_semiring_theory R). *)

Lemma nat_int_to_semiring : forall x : R, exists z,
  x = naturals_to_semiring N R z |_| x + naturals_to_semiring N R z = 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
forall x : R,
{z : N &
((x = naturals_to_semiring N R z) + (plus x (naturals_to_semiring N R z) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
forall x : R,
{z : N &
((x = naturals_to_semiring N R z) + (plus x (naturals_to_semiring N R z) = 0))%type}
apply biinduction.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
{z : N &
((0 = naturals_to_semiring N R z) + (plus 0 (naturals_to_semiring N R z) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
forall n : R,
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%type} <->
{z : N &
((plus 1 n = naturals_to_semiring N R z) +
 (plus (plus 1 n) (naturals_to_semiring N R z) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
{z : N &
((0 = naturals_to_semiring N R z) + (plus 0 (naturals_to_semiring N R z) = 0))%type} exists 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
(0 = naturals_to_semiring N R 0) + (0 + naturals_to_semiring N R 0 = 0)
  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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
0 = naturals_to_semiring N R 0 symmetry.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
naturals_to_semiring N R 0 = 0 exact preserves_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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
forall n : R,
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%type} <->
{z : N &
((plus 1 n = naturals_to_semiring N R z) +
 (plus (plus 1 n) (naturals_to_semiring N R z) = 0))%type} intros.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%type} <->
{z : N &
((plus 1 n = naturals_to_semiring N R z) +
 (plus (plus 1 n) (naturals_to_semiring N R z) = 0))%type} 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
E: {z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%type}
{z : N &
((plus 1 n = naturals_to_semiring N R z) +
 (plus (plus 1 n) (naturals_to_semiring N R z) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
E: {z : N &
((plus 1 n = naturals_to_semiring N R z) +
 (plus (plus 1 n) (naturals_to_semiring N R z) = 0))%type}
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
E: {z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%type}
{z : N &
((plus 1 n = naturals_to_semiring N R z) +
 (plus (plus 1 n) (naturals_to_semiring N R z) = 0))%type} destruct E as [z [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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = naturals_to_semiring N R z
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n + naturals_to_semiring N R z = 0
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = naturals_to_semiring N R z
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%type} exists (1+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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = naturals_to_semiring N R z
(1 + n = naturals_to_semiring N R (1 + z)) +
(1 + n + naturals_to_semiring N R (1 + z) = 0)
      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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = naturals_to_semiring N R z
1 + n = naturals_to_semiring N R (1 + z) rewrite 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = naturals_to_semiring N R z
1 + naturals_to_semiring N R z = naturals_to_semiring N R (1 + z)
      rewrite (preserves_plus (f:=naturals_to_semiring N R)),
      (preserves_1 (f:=naturals_to_semiring N R)).
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = naturals_to_semiring N R z
1 + naturals_to_semiring N R z = 1 + naturals_to_semiring N R z reflexivity.
    *
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n + naturals_to_semiring N R z = 0
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%type} destruct (naturals.case z) as [Ez|[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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n + naturals_to_semiring N R z = 0
Ez: z = 0
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n + naturals_to_semiring N R z = 0
z': N
Ez: z = 1 + z'
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n + naturals_to_semiring N R z = 0
Ez: z = 0
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%type} rewrite Ez in *.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n + naturals_to_semiring N R 0 = 0
Ez: z = 0
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%type}
         rewrite (preserves_0 (A:=N)),plus_0_r in 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = 0
Ez: z = 0
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%type}
         rewrite 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = 0
Ez: z = 0
{z0 : N &
((plus 1 0 = naturals_to_semiring N R z0) +
 (plus (plus 1 0) (naturals_to_semiring N R z0) = 0))%type} exists 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = 0
Ez: z = 0
(1 + 0 = naturals_to_semiring N R 1) +
(1 + 0 + naturals_to_semiring N R 1 = 0) 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = 0
Ez: z = 0
1 + 0 = naturals_to_semiring N R 1
         rewrite (preserves_1 (A:=N)),plus_0_r.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n = 0
Ez: z = 0
1 = 1 reflexivity.
      **
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: n + naturals_to_semiring N R z = 0
z': N
Ez: z = 1 + z'
{z0 : N &
((plus 1 n = naturals_to_semiring N R z0) +
 (plus (plus 1 n) (naturals_to_semiring N R z0) = 0))%type} rewrite Ez in *;clear 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
E: n + naturals_to_semiring N R (1 + z') = 0
{z : N &
((plus 1 n = naturals_to_semiring N R z) +
 (plus (plus 1 n) (naturals_to_semiring N R z) = 0))%type}
         exists z';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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
E: n + naturals_to_semiring N R (1 + z') = 0
1 + n + naturals_to_semiring N R z' = 0
         path_via (n + naturals_to_semiring N R (1 + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
E: n + naturals_to_semiring N R (1 + z') = 0
1 + n + naturals_to_semiring N R z' = n + naturals_to_semiring N R (1 + z')
         clear 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
1 + n + naturals_to_semiring N R z' = n + naturals_to_semiring N R (1 + z') rewrite (preserves_plus (A:=N)),(preserves_1 (A:=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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
1 + n + naturals_to_semiring N R z' = n + (1 + naturals_to_semiring N R z')
         rewrite plus_assoc,(plus_comm n);reflexivity.
  +
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
E: {z : N &
((plus 1 n = naturals_to_semiring N R z) +
 (plus (plus 1 n) (naturals_to_semiring N R z) = 0))%type}
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%type} destruct E as [z [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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: 1 + n = naturals_to_semiring N R z
{z0 : N &
((n = naturals_to_semiring N R z0) +
 (plus n (naturals_to_semiring N R z0) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: 1 + n + naturals_to_semiring N R z = 0
{z0 : N &
((n = naturals_to_semiring N R z0) +
 (plus n (naturals_to_semiring N R z0) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: 1 + n = naturals_to_semiring N R z
{z0 : N &
((n = naturals_to_semiring N R z0) +
 (plus n (naturals_to_semiring N R z0) = 0))%type} destruct (naturals.case z) as [Ez|[z' Ez]];rewrite Ez in *;clear 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
E: 1 + n = naturals_to_semiring N R 0
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
E: 1 + n = naturals_to_semiring N R (1 + z')
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
E: 1 + n = naturals_to_semiring N R 0
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%type} exists 1;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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
E: 1 + n = naturals_to_semiring N R 0
n + naturals_to_semiring N R 1 = 0
         rewrite (preserves_1 (A:=N)),plus_comm,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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
E: 1 + n = naturals_to_semiring N R 0
naturals_to_semiring N R 0 = 0
         exact preserves_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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
E: 1 + n = naturals_to_semiring N R (1 + z')
{z : N &
((n = naturals_to_semiring N R z) + (plus n (naturals_to_semiring N R z) = 0))%type} exists z';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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
E: 1 + n = naturals_to_semiring N R (1 + z')
n = naturals_to_semiring N R z'
         rewrite (preserves_plus (A:=N)),(preserves_1 (A:=N)) in 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
E: 1 + n = 1 + naturals_to_semiring N R z'
n = naturals_to_semiring N R z'
         apply (left_cancellation plus 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z': N
E: 1 + n = 1 + naturals_to_semiring N R z'
1 + n = 1 + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: 1 + n + naturals_to_semiring N R z = 0
{z0 : N &
((n = naturals_to_semiring N R z0) +
 (plus n (naturals_to_semiring N R z0) = 0))%type} exists (1+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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: 1 + n + naturals_to_semiring N R z = 0
(n = naturals_to_semiring N R (1 + z)) +
(n + naturals_to_semiring N R (1 + z) = 0)
      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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: 1 + n + naturals_to_semiring N R z = 0
n + naturals_to_semiring N R (1 + z) = 0 rewrite (preserves_plus (A:=N)), (preserves_1 (A:=N)),<-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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
n: R
z: N
E: 1 + n + naturals_to_semiring N R z = 0
n + (1 + naturals_to_semiring N R z) = 1 + n + naturals_to_semiring N R z
      rewrite plus_assoc,(plus_comm n);reflexivity.
Qed.

Lemma nat_int_nonneg_decompose x : 0 ≤ x -> exists z, x = naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
0 ≤ x -> {z : N & x = naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
0 ≤ x -> {z : N & x = naturals_to_semiring N R z}
destruct (nat_int_to_semiring x) 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez1: x = naturals_to_semiring N R z
0 ≤ x -> {z0 : N & x = naturals_to_semiring N R z0}
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez2: x + naturals_to_semiring N R z = 0
0 ≤ x -> {z0 : N & x = naturals_to_semiring N R z0}
-
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez1: x = naturals_to_semiring N R z
0 ≤ x -> {z0 : N & x = naturals_to_semiring N R z0} 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez1: x = naturals_to_semiring N R z
X: 0 ≤ x
x = naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez2: x + naturals_to_semiring N R z = 0
0 ≤ x -> {z0 : N & x = naturals_to_semiring N R z0} 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez2: x + naturals_to_semiring N R z = 0
E: 0 ≤ x
{z0 : N & x = naturals_to_semiring N R z0} exists 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez2: x + naturals_to_semiring N R z = 0
E: 0 ≤ x
x = naturals_to_semiring N R 0 rewrite (preserves_0 (A:=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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez2: x + naturals_to_semiring N R z = 0
E: 0 ≤ x
x = 0
  apply (antisymmetry (≤)); 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez2: x + naturals_to_semiring N R z = 0
E: 0 ≤ x
x ≤ 0
  rewrite <-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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez2: x + naturals_to_semiring N R z = 0
E: 0 ≤ x
x ≤ x + naturals_to_semiring N R z apply nonneg_plus_le_compat_r.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
z: N
Ez2: x + naturals_to_semiring N R z = 0
E: 0 ≤ x
0 ≤ naturals_to_semiring N R z
  apply to_semiring_nonneg.
Qed.

Lemma nat_int_le_plus x y : x ≤ y <-> exists z, y = x + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y <-> {z : N & y = x + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y <-> {z : N & y = x + naturals_to_semiring N R z}
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y -> {z : N & y = x + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
{z : N & y = x + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y -> {z : N & y = x + naturals_to_semiring N R z} 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
{z : N & y = x + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
z: R
Ez1: 0 ≤ z
Ez2: y = x + z
{z0 : N & y = x + naturals_to_semiring N R z0}
  destruct (nat_int_nonneg_decompose _ Ez1) as [u Eu].
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
z: R
Ez1: 0 ≤ z
Ez2: y = x + z
u: N
Eu: z = naturals_to_semiring N R u
{z0 : N & y = x + naturals_to_semiring N R z0}
  exists u.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
z: R
Ez1: 0 ≤ z
Ez2: y = x + z
u: N
Eu: z = naturals_to_semiring N R u
y = x + naturals_to_semiring N R u rewrite <-Eu.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
z: R
Ez1: 0 ≤ z
Ez2: y = x + z
u: N
Eu: z = naturals_to_semiring N R u
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
{z : N & y = x + naturals_to_semiring N R z} -> x ≤ y intros [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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
z: N
Ez: y = x + naturals_to_semiring N R z
x ≤ y rewrite 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
z: N
Ez: y = x + naturals_to_semiring N R z
x ≤ x + naturals_to_semiring N R z
  apply nonneg_plus_le_compat_r, to_semiring_nonneg.
Qed.

Lemma nat_int_lt_plus x y : x < y <-> exists z, y = x + 1 + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> {z : N & y = x + 1 + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> {z : N & y = x + 1 + naturals_to_semiring N R z}
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y -> {z : N & y = x + 1 + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
{z : N & y = x + 1 + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y -> {z : N & y = x + 1 + naturals_to_semiring N R z} 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
{z : N & y = x + 1 + naturals_to_semiring N R z}
  destruct ((fst (nat_int_le_plus x y) (lt_le _ _ E))) as [z0 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
z0: N
Ez: y = x + naturals_to_semiring N R z0
{z : N & y = x + 1 + naturals_to_semiring N R z}
  destruct (naturals.case z0) as [E1|[z E1]];rewrite E1 in *;clear z0 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
Ez: y = x + naturals_to_semiring N R 0
{z : N & y = x + 1 + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
z: N
Ez: y = x + naturals_to_semiring N R (1 + z)
{z0 : N & y = x + 1 + naturals_to_semiring N R z0}
  +
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
Ez: y = x + naturals_to_semiring N R 0
{z : N & y = x + 1 + naturals_to_semiring N R z} rewrite preserves_0, plus_0_r in 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
Ez: y = x
{z : N & y = x + 1 + naturals_to_semiring N R z}
    destruct (lt_ne_flip x y);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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
z: N
Ez: y = x + naturals_to_semiring N R (1 + z)
{z0 : N & y = x + 1 + naturals_to_semiring N R z0} 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
z: N
Ez: y = x + naturals_to_semiring N R (1 + z)
y = x + 1 + naturals_to_semiring N R z
    rewrite (preserves_plus (A:=N)), preserves_1, plus_assoc in 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y
z: N
Ez: y = x + 1 + naturals_to_semiring N R z
y = x + 1 + naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
{z : N & y = x + 1 + naturals_to_semiring N R z} -> x < y intros [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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
z: N
Ez: y = x + 1 + naturals_to_semiring N R z
x < y rewrite 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
z: N
Ez: y = x + 1 + naturals_to_semiring N R z
x < x + 1 + naturals_to_semiring N R z
  apply nonneg_plus_lt_compat_r.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
z: N
Ez: y = x + 1 + naturals_to_semiring N R z
0 ≤ naturals_to_semiring N R 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
z: N
Ez: y = x + 1 + naturals_to_semiring N R z
x < x + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
z: N
Ez: y = x + 1 + naturals_to_semiring N R z
0 ≤ naturals_to_semiring N R z apply to_semiring_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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
z: N
Ez: y = x + 1 + naturals_to_semiring N R z
x < x + 1 apply pos_plus_lt_compat_r; solve_propholds.
Qed.

Lemma lt_iff_plus_1_le x y : x < y <-> x + 1 ≤ 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> x + 1 ≤ 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> x + 1 ≤ y
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> ?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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
?Goal <-> x + 1 ≤ 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> ?Goal apply nat_int_lt_plus.
-
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
{z : N & y = x + 1 + naturals_to_semiring N R z} <-> x + 1 ≤ y apply symmetry,nat_int_le_plus.
Qed.

Lemma lt_iff_S_le x y : x < y <-> 1 + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> 1 + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> 1 + x ≤ y
rewrite plus_comm.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x < y <-> x + 1 ≤ y apply lt_iff_plus_1_le.
Qed.

Lemma pos_ge_1 x : 0 < x <-> 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
0 < x <-> 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
0 < x <-> 1 ≤ x
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
E: 0 < x
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
E: 1 ≤ x
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
E: 0 < x
1 ≤ x rewrite <-(plus_0_l 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
E: 0 < x
0 + 1 ≤ x apply lt_iff_plus_1_le.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
E: 0 < x
0 < x 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x: R
E: 1 ≤ x
0 < x apply lt_le_trans with 1; [solve_propholds | trivial].
Qed.

Lemma le_iff_lt_plus_1 x y : x ≤ y <-> x < y + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y <-> x < y + 1
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y <-> x < y + 1
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
x < y + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y + 1
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
x < y + 1 apply lt_iff_plus_1_le.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
x + 1 ≤ y + 1 apply (order_preserving (+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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x ≤ y
x ≤ y 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y + 1
x ≤ y apply (order_reflecting (+1)), lt_iff_plus_1_le.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
E: x < y + 1
x < y + 1 trivial.
Qed.

Lemma le_iff_lt_S x y : x ≤ y <-> x < 1 + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y <-> x < 1 + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y <-> x < 1 + y rewrite plus_comm.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
x, y: R
x ≤ y <-> x < y + 1 apply le_iff_lt_plus_1. Qed.

Section another_semiring.
  Context `{FullPseudoSemiRingOrder R2} `{!IsSemiCRing R2}
    `{PropHolds ((1 : R2) ≶ 0)}
    `{!IsSemiRingPreserving (f : R -> R2)}.

  Instance orderpreserving_semiring_homomorphism : OrderPreserving f.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
OrderPreserving f
  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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
OrderPreserving f
  repeat (split; try exact _).
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
OrderPreserving f
  intros x y 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
E: x ≤ y
f x ≤ f y apply nat_int_le_plus in 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
E: {z : N & y = x + naturals_to_semiring N R z}
f x ≤ f y destruct E as [z 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + naturals_to_semiring N R z
f x ≤ f y
  rewrite E, (preserves_plus (f:=f)), (naturals.to_semiring_twice f _ _).
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + naturals_to_semiring N R z
f x ≤ f x + naturals_to_semiring N R2 z
  apply nonneg_plus_le_compat_r.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + naturals_to_semiring N R z
0 ≤ naturals_to_semiring N R2 z apply to_semiring_nonneg.
  Qed.

  #[export] Instance strictlyorderpreserving_semiring_homomorphism : StrictlyOrderPreserving f | 50.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
StrictlyOrderPreserving f
  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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
StrictlyOrderPreserving f
  repeat (split; try exact _).
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
StrictlyOrderPreserving f
  intros x y 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
E: x < y
f x < f y apply nat_int_lt_plus in 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
E: {z : N & y = x + 1 + naturals_to_semiring N R z}
f x < f y destruct E as [z 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + 1 + naturals_to_semiring N R z
f x < f y
  rewrite E, !(preserves_plus (f:=f)), preserves_1,
  (naturals.to_semiring_twice f _ _).
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + 1 + naturals_to_semiring N R z
f x < f x + 1 + naturals_to_semiring N R2 z
  apply nonneg_plus_lt_compat_r.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + 1 + naturals_to_semiring N R z
0 ≤ naturals_to_semiring N R2 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + 1 + naturals_to_semiring N R z
f x < f x + 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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + 1 + naturals_to_semiring N R z
0 ≤ naturals_to_semiring N R2 z apply to_semiring_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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
x, y: R
z: N
E: y = x + 1 + naturals_to_semiring N R z
f x < f x + 1 apply pos_plus_lt_compat_r; solve_propholds.
  Qed.

  #[export] Instance nat_morphism_order_embedding : OrderEmbedding f | 50.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
OrderEmbedding f
  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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
OrderEmbedding f split; try exact _.
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
H2: Apart N
H3: Le N
H4: Lt N
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder le lt
R: Type
H5: Apart R
H6: Plus R
H7: Mult R
H8: Zero R
H9: One R
Ale0: Le R
Alt0: Lt R
H10: FullPseudoSemiRingOrder Ale0 Alt0
IsSemiCRing0: IsSemiCRing R
Biinduction0: Biinduction R
H11: PropHolds (1 ≶ 0)
R2: Type
H12: Apart R2
H13: Plus R2
H14: Mult R2
H15: Zero R2
H16: One R2
Ale1: Le R2
Alt1: Lt R2
H17: FullPseudoSemiRingOrder Ale1 Alt1
IsSemiCRing1: IsSemiCRing R2
H18: PropHolds ((1 : R2) ≶ 0)
f: R -> R2
IsSemiRingPreserving0: IsSemiRingPreserving (f : R -> R2)
OrderReflecting f exact full_pseudo_order_reflecting. Qed.
End another_semiring.
End nat_int_order.
End Univ.