Require Import
  HoTT.Basics.Decidable.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import
  HoTT.Classes.interfaces.orders
  HoTT.Classes.implementations.peano_naturals
  HoTT.Classes.theory.rings
  HoTT.Classes.isomorphisms.rings.
Require Export
  HoTT.Classes.interfaces.naturals.

Generalizable Variables A N R SR f.

(* This grabs a coercion. *)
Import SemiRings.

Lemma to_semiring_unique `{Naturals N} `{IsSemiCRing SR} (f: N -> SR)
  `{!IsSemiRingPreserving f} x
  : f x = naturals_to_semiring N SR x.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
f: N -> SR
IsSemiRingPreserving0: IsSemiRingPreserving f
x: N
f x = naturals_to_semiring N SR x
Proof.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
f: N -> SR
IsSemiRingPreserving0: IsSemiRingPreserving f
x: N
f x = naturals_to_semiring N SR x
symmetry.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
f: N -> SR
IsSemiRingPreserving0: IsSemiRingPreserving f
x: N
naturals_to_semiring N SR x = f x apply naturals_initial.
Qed.

Lemma to_semiring_unique_alt `{Naturals N} `{IsSemiCRing SR} (f g: N -> SR)
  `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} x
  : f x = g x.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
f, g: N -> SR
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x: N
f x = g x
Proof.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
f, g: N -> SR
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x: N
f x = g x
rewrite (to_semiring_unique f), (to_semiring_unique g);reflexivity.
Qed.

Lemma to_semiring_involutive N `{Naturals N} N2 `{Naturals N2} x :
  naturals_to_semiring N2 N (naturals_to_semiring N N2 x) = x.
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
H: Naturals N
N2: Type
Aap0: Apart N2
Aplus0: Plus N2
Amult0: Mult N2
Azero0: Zero N2
Aone0: One N2
Ale0: Le N2
Alt0: Lt N2
U0: NaturalsToSemiRing N2
H0: Naturals N2
x: N
naturals_to_semiring N2 N
  (naturals_to_semiring N N2 x) = x
Proof.
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
H: Naturals N
N2: Type
Aap0: Apart N2
Aplus0: Plus N2
Amult0: Mult N2
Azero0: Zero N2
Aone0: One N2
Ale0: Le N2
Alt0: Lt N2
U0: NaturalsToSemiRing N2
H0: Naturals N2
x: N
naturals_to_semiring N2 N
  (naturals_to_semiring N N2 x) = x
change (Compose (naturals_to_semiring N2 N) (naturals_to_semiring N N2) x = id x).
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
H: Naturals N
N2: Type
Aap0: Apart N2
Aplus0: Plus N2
Amult0: Mult N2
Azero0: Zero N2
Aone0: One N2
Ale0: Le N2
Alt0: Lt N2
U0: NaturalsToSemiRing N2
H0: Naturals N2
x: N
(naturals_to_semiring N2 N ∘ naturals_to_semiring N N2)
  x = id x
apply to_semiring_unique_alt;apply _.
Qed.

Lemma morphisms_involutive `{Naturals N} `{IsSemiCRing R} (f : R -> N) (g : N -> R)
  `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} x : f (g x) = x.
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
H: Naturals N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
H0: IsSemiCRing R
f: R -> N
g: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x: N
f (g x) = x
Proof.
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
H: Naturals N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
H0: IsSemiCRing R
f: R -> N
g: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x: N
f (g x) = x exact (to_semiring_unique_alt (f ∘ g) id _). Qed.

Lemma to_semiring_twice `{Naturals N} `{IsSemiCRing R1} `{IsSemiCRing R2}
  (f : R1 -> R2) (g : N -> R1) (h : N -> R2)
  `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} `{!IsSemiRingPreserving h} x
  : f (g x) = h x.
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
H: Naturals N
R1: Type
Aplus0: Plus R1
Amult0: Mult R1
Azero0: Zero R1
Aone0: One R1
H0: IsSemiCRing R1
R2: Type
Aplus1: Plus R2
Amult1: Mult R2
Azero1: Zero R2
Aone1: One R2
H1: IsSemiCRing R2
f: R1 -> R2
g: N -> R1
h: N -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
IsSemiRingPreserving2: IsSemiRingPreserving h
x: N
f (g x) = h x
Proof.
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
H: Naturals N
R1: Type
Aplus0: Plus R1
Amult0: Mult R1
Azero0: Zero R1
Aone0: One R1
H0: IsSemiCRing R1
R2: Type
Aplus1: Plus R2
Amult1: Mult R2
Azero1: Zero R2
Aone1: One R2
H1: IsSemiCRing R2
f: R1 -> R2
g: N -> R1
h: N -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
IsSemiRingPreserving2: IsSemiRingPreserving h
x: N
f (g x) = h x exact (to_semiring_unique_alt (f ∘ g) h _). Qed.

Lemma to_semiring_self `{Naturals N} (f : N -> N) `{!IsSemiRingPreserving f} x
  : f x = x.
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
H: Naturals N
f: N -> N
IsSemiRingPreserving0: IsSemiRingPreserving f
x: N
f x = x
Proof.
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
H: Naturals N
f: N -> N
IsSemiRingPreserving0: IsSemiRingPreserving f
x: N
f x = x exact (to_semiring_unique_alt f id _). Qed.

Lemma to_semiring_injective `{Naturals N} `{IsSemiCRing A}
   (f: A -> N) (g: N -> A) `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g}
   : IsInjective g.
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
H: Naturals N
A: Type
Aplus0: Plus A
Amult0: Mult A
Azero0: Zero A
Aone0: One A
H0: IsSemiCRing A
f: A -> N
g: N -> A
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
IsInjective g
Proof.
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
H: Naturals N
A: Type
Aplus0: Plus A
Amult0: Mult A
Azero0: Zero A
Aone0: One A
H0: IsSemiCRing A
f: A -> N
g: N -> A
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
IsInjective g
intros x y E.
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
H: Naturals N
A: Type
Aplus0: Plus A
Amult0: Mult A
Azero0: Zero A
Aone0: One A
H0: IsSemiCRing A
f: A -> N
g: N -> A
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x, y: N
E: g x = g y
x = y
change (id x = id y).
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
H: Naturals N
A: Type
Aplus0: Plus A
Amult0: Mult A
Azero0: Zero A
Aone0: One A
H0: IsSemiCRing A
f: A -> N
g: N -> A
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x, y: N
E: g x = g y
id x = id y
rewrite <-(to_semiring_twice f g id x), <-(to_semiring_twice f g id y).
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
H: Naturals N
A: Type
Aplus0: Plus A
Amult0: Mult A
Azero0: Zero A
Aone0: One A
H0: IsSemiCRing A
f: A -> N
g: N -> A
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x, y: N
E: g x = g y
f (g x) = f (g y)
apply ap,E.
Qed.

Global Instance naturals_to_naturals_injective `{Naturals N} `{Naturals N2}
  (f: N -> N2) `{!IsSemiRingPreserving f}
  : IsInjective f | 15.
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
H: Naturals N
N2: Type
Aap0: Apart N2
Aplus0: Plus N2
Amult0: Mult N2
Azero0: Zero N2
Aone0: One N2
Ale0: Le N2
Alt0: Lt N2
U0: NaturalsToSemiRing N2
H0: Naturals N2
f: N -> N2
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective f
Proof.
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
H: Naturals N
N2: Type
Aap0: Apart N2
Aplus0: Plus N2
Amult0: Mult N2
Azero0: Zero N2
Aone0: One N2
Ale0: Le N2
Alt0: Lt N2
U0: NaturalsToSemiRing N2
H0: Naturals N2
f: N -> N2
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective f exact (to_semiring_injective (naturals_to_semiring N2 N) _). Qed.

Section retract_is_nat.
  Context `{Naturals N} `{IsSemiCRing SR}
    {SRap : Apart SR} {SRle SRlt} `{!FullPseudoSemiRingOrder (A:=SR) SRle SRlt}.
  Context (f : N -> SR) `{!IsEquiv f}
    `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving (f^-1)}.

  (* If we make this an instance, instance resolution will loop *)
  Definition retract_is_nat_to_sr : NaturalsToSemiRing SR
    := fun R _ _ _ _ _ => naturals_to_semiring N R ∘ f^-1.

  Section for_another_semirings.
    Context `{IsSemiCRing R}.

    Instance: IsSemiRingPreserving (naturals_to_semiring N R ∘ f^-1) := {}.

    Context (h :  SR -> R) `{!IsSemiRingPreserving h}.

    Lemma same_morphism x : (naturals_to_semiring N R ∘ f^-1) x = h x.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
H1: IsSemiCRing R
h: SR -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: SR
(naturals_to_semiring N R ∘ f^-1) x = h x
    Proof.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
H1: IsSemiCRing R
h: SR -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: SR
(naturals_to_semiring N R ∘ f^-1) x = h x
    transitivity ((h ∘ (f ∘ f^-1)) x).
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
H1: IsSemiCRing R
h: SR -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: SR
(naturals_to_semiring N R ∘ f^-1) x =
(h ∘ (f ∘ f^-1)) x
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
H1: IsSemiCRing R
h: SR -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: SR
(h ∘ (f ∘ f^-1)) x = h x
    -
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
H1: IsSemiCRing R
h: SR -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: SR
(naturals_to_semiring N R ∘ f^-1) x =
(h ∘ (f ∘ f^-1)) x symmetry.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
H1: IsSemiCRing R
h: SR -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: SR
(h ∘ (f ∘ f^-1)) x =
(naturals_to_semiring N R ∘ f^-1) x apply (to_semiring_unique (h ∘ f)).
    -
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
H1: IsSemiCRing R
h: SR -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: SR
(h ∘ (f ∘ f^-1)) x = h x unfold Compose.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
H1: IsSemiCRing R
h: SR -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: SR
h (f (f^-1 x)) = h x apply ap, eisretr.
    Qed.
  End for_another_semirings.

  (* If we make this an instance, instance resolution will loop *)
  Lemma retract_is_nat : Naturals SR (U:=retract_is_nat_to_sr).
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
Naturals SR
  Proof.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
Naturals SR
  split;try apply _.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
forall (B : Type) (Aplus1 : Plus B) (Amult1 : Mult B)
(Azero1 : Zero B) (Aone1 : One B) (H : IsSemiCRing B),
IsSemiRingPreserving (naturals_to_semiring SR B)
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
forall (B : Type) (Aplus1 : Plus B) 
(Amult1 : Mult B) (Azero1 : Zero B) 
(Aone1 : One B) (H : IsSemiCRing B) 
(h : SR -> B),
IsSemiRingPreserving h ->
forall x : SR, naturals_to_semiring SR B x = h x
  -
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
forall (B : Type) (Aplus1 : Plus B) (Amult1 : Mult B)
(Azero1 : Zero B) (Aone1 : One B) (H : IsSemiCRing B),
IsSemiRingPreserving (naturals_to_semiring SR B) unfold naturals_to_semiring, retract_is_nat_to_sr.
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
forall (B : Type) (Aplus1 : Plus B) (Amult1 : Mult B)
(Azero1 : Zero B) (Aone1 : One B) (H : IsSemiCRing B),
IsSemiRingPreserving (naturals_to_semiring N B ∘ f^-1) apply _.
  -
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
H: Naturals N
SR: Type
Aplus0: Plus SR
Amult0: Mult SR
Azero0: Zero SR
Aone0: One SR
H0: IsSemiCRing SR
SRap: Apart SR
SRle: Le SR
SRlt: Lt SR
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  SRle SRlt
f: N -> SR
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
forall (B : Type) (Aplus1 : Plus B) (Amult1 : Mult B)
(Azero1 : Zero B) (Aone1 : One B) (H : IsSemiCRing B)
(h : SR -> B),
IsSemiRingPreserving h ->
forall x : SR, naturals_to_semiring SR B x = h x intros;apply same_morphism;apply _.
  Qed.
End retract_is_nat.

Section nat_to_nat_iso.

Context `{Naturals N1} `{Naturals N2}.

Global Instance nat_to_nat_equiv : IsEquiv (naturals_to_semiring N1 N2).
N1: Type
Aap: Apart N1
Aplus: Plus N1
Amult: Mult N1
Azero: Zero N1
Aone: One N1
Ale: Le N1
Alt: Lt N1
U: NaturalsToSemiRing N1
H: Naturals N1
N2: Type
Aap0: Apart N2
Aplus0: Plus N2
Amult0: Mult N2
Azero0: Zero N2
Aone0: One N2
Ale0: Le N2
Alt0: Lt N2
U0: NaturalsToSemiRing N2
H0: Naturals N2
IsEquiv (naturals_to_semiring N1 N2)
Proof.
N1: Type
Aap: Apart N1
Aplus: Plus N1
Amult: Mult N1
Azero: Zero N1
Aone: One N1
Ale: Le N1
Alt: Lt N1
U: NaturalsToSemiRing N1
H: Naturals N1
N2: Type
Aap0: Apart N2
Aplus0: Plus N2
Amult0: Mult N2
Azero0: Zero N2
Aone0: One N2
Ale0: Le N2
Alt0: Lt N2
U0: NaturalsToSemiRing N2
H0: Naturals N2
IsEquiv (naturals_to_semiring N1 N2)
apply Equivalences.isequiv_adjointify with (naturals_to_semiring N2 N1);
red;apply (to_semiring_involutive _ _).
Defined.

End nat_to_nat_iso.

Section contents.
Universe U.

(* {U U} because we do forall n : N, {id} n = nat_to_sr N N n *)
Context `{Funext} `{Univalence} {N : Type@{U} } `{Naturals@{U U U U U U U U} N}.

Lemma from_nat_stmt  (N':Type@{U}) `{Naturals@{U U U U U U U U} N'}
  : forall (P : SemiRings.Operations -> Type),
  P (SemiRings.BuildOperations N') -> P (SemiRings.BuildOperations 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
N': Type
Aap0: Apart N'
Aplus0: Plus N'
Amult0: Mult N'
Azero0: Zero N'
Aone0: One N'
Ale0: Le N'
Alt0: Lt N'
U0: NaturalsToSemiRing N'
H2: Naturals N'
forall P : Operations -> Type,
P (BuildOperations N') -> P (BuildOperations N)
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
N': Type
Aap0: Apart N'
Aplus0: Plus N'
Amult0: Mult N'
Azero0: Zero N'
Aone0: One N'
Ale0: Le N'
Alt0: Lt N'
U0: NaturalsToSemiRing N'
H2: Naturals N'
forall P : Operations -> Type,
P (BuildOperations N') -> P (BuildOperations N)
apply SemiRings.iso_leibnitz with (naturals_to_semiring N' N);apply _.
Qed.

Section borrowed_from_nat.

  Lemma induction
    : forall (P: N -> Type),
    P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P 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
forall P : N -> Type,
P 0 ->
(forall n : N, P n -> P (1 + n)) -> forall n : N, P n
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
forall P : N -> Type,
P 0 ->
(forall n : N, P n -> P (1 + n)) -> forall n : N, P n
  pose (Q := fun s : SemiRings.Operations =>
    forall P : s -> Type, P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P 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
Q:= fun s : Operations =>
forall P : s -> Type,
P 0 ->
(forall n : s, P n -> P (1 + n)) ->
forall n : s, P n: Operations -> Type
forall P : N -> Type,
P 0 ->
(forall n : N, P n -> P (1 + n)) -> forall n : N, P n
  change (Q (SemiRings.BuildOperations 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
Q:= fun s : Operations =>
forall P : s -> Type,
P 0 ->
(forall n : s, P n -> P (1 + n)) ->
forall n : s, P n: Operations -> Type
Q (BuildOperations N)
  apply (from_nat_stmt nat).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
Q:= fun s : Operations =>
forall P : s -> Type,
P 0 ->
(forall n : s, P n -> P (1 + n)) ->
forall n : s, P n: Operations -> Type
Q (BuildOperations nat)
  unfold Q;clear Q.
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
forall P : BuildOperations nat -> Type,
P 0 ->
(forall n : BuildOperations nat, P n -> P (1 + n)) ->
forall n : BuildOperations nat, P n
  simpl.
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
forall P : nat -> Type,
P 0 ->
(forall n : nat, P n -> P (1 + n)) ->
forall n : nat, P n
  exact nat_induction.
  Qed.

  Lemma case : forall x : N, x = 0 |_| exists y : N, (x = 1 + y)%mc.
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
forall x : N,
((x = 0) + {y : N & x = (1 + y)%mc})%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
forall x : N,
((x = 0) + {y : N & x = (1 + y)%mc})%type
  refine (from_nat_stmt nat
    (fun s => forall x : s, x = 0 |_| exists y : s, (x = 1 + y)%mc) _).
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
forall x : BuildOperations nat,
((x = 0) + {y : BuildOperations nat & x = (1 + y)%mc})%type
  simpl.
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
forall x : nat,
((x = 0) + {y : nat & x = (1 + y)%mc})%type intros [|x];eauto.
  Qed.

  Global Instance: Biinduction 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
Biinduction N
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
Biinduction N
  hnf.
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
forall P : N -> Type,
P 0 ->
(forall n : N, P n <-> P (1 + n)) -> forall n : N, P n intros P E0 ES.
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
P: N -> Type
E0: P 0
ES: forall n : N, P n <-> P (1 + n)
forall n : N, P n
  apply induction;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
P: N -> Type
E0: P 0
ES: forall n : N, P n <-> P (1 + n)
forall n : N, P n -> P (1 + n)
  apply ES.
  Qed.

  Global Instance nat_plus_cancel_l : forall z : N, LeftCancellation (+) 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
forall z : N, LeftCancellation plus 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
forall z : N, LeftCancellation plus z
  refine (from_nat_stmt@{i U}
    nat (fun s => forall z : s, LeftCancellation plus 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
forall z : BuildOperations nat,
LeftCancellation plus z
  simpl.
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
forall z : nat, LeftCancellation plus z first [exact nat_plus_cancel_l@{U i}|exact nat_plus_cancel_l@{U}].
  Qed.

  Global Instance: forall z : N, RightCancellation (+) 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
forall z : N, RightCancellation plus 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
forall z : N, RightCancellation plus z intro.
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
z: N
RightCancellation plus z apply (right_cancel_from_left (+)). Qed.

  Global Instance: forall z : N, PropHolds (z <> 0) -> LeftCancellation (.*.) 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
forall z : N,
PropHolds (z <> 0) -> LeftCancellation mult z
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
forall z : N,
PropHolds (z <> 0) -> LeftCancellation mult z
  refine (from_nat_stmt nat (fun s =>
    forall z : s, PropHolds (z <> 0) -> LeftCancellation mult 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
forall z : BuildOperations nat,
PropHolds (z <> 0) -> LeftCancellation mult z
  simpl.
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
forall z : nat,
PropHolds (z <> 0) -> LeftCancellation mult z apply nat_mult_cancel_l.
  Qed.

  Global Instance: forall z : N, PropHolds (z <> 0) -> RightCancellation (.*.) 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
forall z : N,
PropHolds (z <> 0) -> RightCancellation mult z
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
forall z : N,
PropHolds (z <> 0) -> RightCancellation mult z 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
z: N
X: PropHolds (z <> 0)
RightCancellation mult z apply (right_cancel_from_left (.*.)). Qed.

  Instance nat_nontrivial: PropHolds ((1:N) <> 0).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
PropHolds ((1 : N) <> 0)
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
PropHolds ((1 : N) <> 0)
  refine (from_nat_stmt nat (fun s => PropHolds ((1:s) <> 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
PropHolds (1 <> 0)
  apply _.
  Qed.

  Instance nat_nontrivial_apart `{Apart N} `{!TrivialApart N} :
    PropHolds ((1:N) ≶ 0).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
H2: Apart N
TrivialApart0: TrivialApart N
PropHolds ((1 : N) ≶ 0)
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
H2: Apart N
TrivialApart0: TrivialApart N
PropHolds ((1 : N) ≶ 0) apply apartness.ne_apart.
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
TrivialApart0: TrivialApart N
PropHolds (1 <> 0) solve_propholds. Qed.

  Lemma zero_sum : forall (x y : N), x + y = 0 -> x = 0 /\ y = 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
forall x y : N, x + y = 0 -> ((x = 0) * (y = 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
forall x y : N, x + y = 0 -> ((x = 0) * (y = 0))%type
  refine (from_nat_stmt nat
    (fun s => forall x y : s, x + y = 0 -> x = 0 /\ y = 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
forall x y : BuildOperations nat,
x + y = 0 -> ((x = 0) * (y = 0))%type
  simpl.
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
forall x y : nat,
x + y = 0 -> ((x = 0) * (y = 0))%type apply plus_eq_zero.
  Qed.

  Lemma one_sum : forall (x y : N), x + y = 1 -> (x = 1 /\ y = 0) |_| (x = 0 /\ 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
forall x y : N,
x + y = 1 ->
((x = 1) * (y = 0) + (x = 0) * (y = 1))%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
forall x y : N,
x + y = 1 ->
((x = 1) * (y = 0) + (x = 0) * (y = 1))%type
  refine (from_nat_stmt nat (fun s =>
    forall (x y : s), x + y = 1 -> (x = 1 /\ y = 0) |_| (x = 0 /\ 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
forall x y : BuildOperations nat,
x + y = 1 ->
((x = 1) * (y = 0) + (x = 0) * (y = 1))%type
  simpl.
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
forall x y : nat,
x + y = 1 ->
((x = 1) * (y = 0) + (x = 0) * (y = 1))%type
  intros [|x] [|y];auto.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
x: nat
(x.+1)%nat + 0%nat = 1 ->
(((x.+1)%nat = 1) * (0%nat = 0) +
 ((x.+1)%nat = 0) * (0%nat = 1))%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
x, y: nat
(x.+1)%nat + (y.+1)%nat = 1 ->
(((x.+1)%nat = 1) * ((y.+1)%nat = 0) +
 ((x.+1)%nat = 0) * ((y.+1)%nat = 1))%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
x: nat
(x.+1)%nat + 0%nat = 1 ->
(((x.+1)%nat = 1) * (0%nat = 0) +
 ((x.+1)%nat = 0) * (0%nat = 1))%type 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
x: nat
E: (x.+1)%nat + 0%nat = 1
(((x.+1)%nat = 1) * (0%nat = 0) +
 ((x.+1)%nat = 0) * (0%nat = 1))%type rewrite add_S_l,add_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
x: nat
E: (x.+1)%nat = 1
(((x.+1)%nat = 1) * (0%nat = 0) +
 ((x.+1)%nat = 0) * (0%nat = 1))%type
    apply S_inj 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
x: nat
E: x = 0%nat
(((x.+1)%nat = 1) * (0%nat = 0) +
 ((x.+1)%nat = 0) * (0%nat = 1))%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
x: nat
E: x = 0%nat
((1%nat = 1) * (0%nat = 0) + (1%nat = 0) * (0%nat = 1))%type
    auto.
  -
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
x, y: nat
(x.+1)%nat + (y.+1)%nat = 1 ->
(((x.+1)%nat = 1) * ((y.+1)%nat = 0) +
 ((x.+1)%nat = 0) * ((y.+1)%nat = 1))%type 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
x, y: nat
E: (x.+1)%nat + (y.+1)%nat = 1
(((x.+1)%nat = 1) * ((y.+1)%nat = 0) +
 ((x.+1)%nat = 0) * ((y.+1)%nat = 1))%type
    rewrite add_S_l,add_S_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
x, y: nat
E: ((x + y).+2)%nat = 1
(((x.+1)%nat = 1) * ((y.+1)%nat = 0) +
 ((x.+1)%nat = 0) * ((y.+1)%nat = 1))%type
    apply S_inj 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
x, y: nat
E: ((x + y).+1)%nat = 0%nat
(((x.+1)%nat = 1) * ((y.+1)%nat = 0) +
 ((x.+1)%nat = 0) * ((y.+1)%nat = 1))%type destruct (S_neq_0 _ E).
  Qed.

  Global Instance: ZeroProduct 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
ZeroProduct N
  Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
ZeroProduct N
  refine (from_nat_stmt nat (fun s => ZeroProduct s) _).
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
ZeroProduct (BuildOperations nat)
  simpl.
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
ZeroProduct nat red.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
forall x y : nat,
x * y = 0 -> ((x = 0) + (y = 0))%type apply mult_eq_zero.
  Qed.
End borrowed_from_nat.

Lemma nat_1_plus_ne_0 x : 1 + x <> 0.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
x: N
1 + x <> 0
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
x: N
1 + x <> 0
intro 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
x: N
E: 1 + x = 0
Empty destruct (zero_sum 1 x 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
x: N
E: 1 + x = 0
fst: 1 = 0
snd: x = 0
Empty apply nat_nontrivial.
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
x: N
E: 1 + x = 0
fst: 1 = 0
snd: x = 0
1 = 0 trivial.
Qed.

Global Instance slow_naturals_dec : DecidablePaths 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
DecidablePaths N
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
DecidablePaths N
apply decidablepaths_equiv with nat (naturals_to_semiring nat N);apply _.
Qed.

Section with_a_ring.
  Context `{IsCRing R} `{!IsSemiRingPreserving (f : N -> R)} `{!IsInjective f}.

  Lemma to_ring_zero_sum x y :
    -f x = f y -> x = 0 /\ y = 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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
- f x = f y -> ((x = 0) * (y = 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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
- f x = f y -> ((x = 0) * (y = 0))%type
  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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
E: - f x = f y
((x = 0) * (y = 0))%type apply zero_sum, (injective 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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
E: - f x = f y
f (x + y) = f 0
  rewrite rings.preserves_0, rings.preserves_plus, <-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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
E: - f x = f y
f x - f x = 0
  apply plus_negate_r.
  Qed.

  Lemma negate_to_ring x y :
    -f x = f y -> f x = f 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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
- f x = f y -> f x = f 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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
- f x = f y -> f x = f y
  intros E.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
E: - f x = f y
f x = f y destruct (to_ring_zero_sum x y E) as [E2 E3].
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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
E: - f x = f y
E2: x = 0
E3: y = 0
f x = f y
  rewrite E2, E3.
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
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate: Negate R
H2: IsCRing R
f: N -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> R)
IsInjective0: IsInjective f
x, y: N
E: - f x = f y
E2: x = 0
E3: y = 0
f 0 = f 0 reflexivity.
  Qed.
End with_a_ring.
End contents.

(* Due to bug #2528 *)
#[export]
Hint Extern 6 (PropHolds (1 <> 0)) =>
  eapply @nat_nontrivial : typeclass_instances.
#[export]
Hint Extern 6 (PropHolds (1 ≶ 0)) =>
  eapply @nat_nontrivial_apart : typeclass_instances.