(* General results about arbitrary integer implementations. *)
Require Import
  HoTT.Basics.Decidable.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import
 HoTT.Classes.theory.nat_distance
 HoTT.Classes.implementations.peano_naturals
 HoTT.Classes.interfaces.naturals
 HoTT.Classes.interfaces.orders
 HoTT.Classes.implementations.natpair_integers
 HoTT.Classes.theory.rings
 HoTT.Classes.isomorphisms.rings.
Require Export
 HoTT.Classes.interfaces.integers.

Import NatPair.Instances.
Generalizable Variables N Z R f.

Lemma to_ring_unique `{Integers Z} `{IsCRing R} (f: Z -> R)
  {h: IsSemiRingPreserving f} x
  : f x = integers_to_ring Z R x.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: Z -> R
h: IsSemiRingPreserving f
x: Z
f x = integers_to_ring Z R x
Proof.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: Z -> R
h: IsSemiRingPreserving f
x: Z
f x = integers_to_ring Z R x
symmetry.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: Z -> R
h: IsSemiRingPreserving f
x: Z
integers_to_ring Z R x = f x apply integers_initial.
Qed.

Lemma to_ring_unique_alt `{Integers Z} `{IsCRing R} (f g: Z -> R)
  `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} x :
  f x = g x.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f, g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x: Z
f x = g x
Proof.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f, g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x: Z
f x = g x
rewrite (to_ring_unique f), (to_ring_unique g);reflexivity.
Qed.

Lemma to_ring_involutive Z `{Integers Z} Z2 `{Integers Z2} x :
  integers_to_ring Z2 Z (integers_to_ring Z Z2 x) = x.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
Z2: Type
Aap0: Apart Z2
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
Ale0: Le Z2
Alt0: Lt Z2
U0: IntegersToRing Z2
H0: Integers Z2
x: Z
integers_to_ring Z2 Z (integers_to_ring Z Z2 x) = x
Proof.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
Z2: Type
Aap0: Apart Z2
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
Ale0: Le Z2
Alt0: Lt Z2
U0: IntegersToRing Z2
H0: Integers Z2
x: Z
integers_to_ring Z2 Z (integers_to_ring Z Z2 x) = x
change (Compose (integers_to_ring Z2 Z) (integers_to_ring Z Z2) x = id x).
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
Z2: Type
Aap0: Apart Z2
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
Ale0: Le Z2
Alt0: Lt Z2
U0: IntegersToRing Z2
H0: Integers Z2
x: Z
(integers_to_ring Z2 Z ∘ integers_to_ring Z Z2) x =
id x
apply to_ring_unique_alt;apply _.
Qed.

Lemma morphisms_involutive `{Integers Z} `{IsCRing R} (f: R -> Z) (g: Z -> R)
  `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} x : f (g x) = x.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: R -> Z
g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x: Z
f (g x) = x
Proof.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: R -> Z
g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x: Z
f (g x) = x exact (to_ring_unique_alt (f ∘ g) id _). Qed.

Lemma to_ring_twice `{Integers Z} `{IsCRing R1} `{IsCRing R2}
  (f : R1 -> R2) (g : Z -> R1) (h : Z -> R2)
  `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} `{!IsSemiRingPreserving h} x
  : f (g x) = h x.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R1: Type
Aplus0: Plus R1
Amult0: Mult R1
Azero0: Zero R1
Aone0: One R1
Anegate0: Negate R1
H0: IsCRing R1
R2: Type
Aplus1: Plus R2
Amult1: Mult R2
Azero1: Zero R2
Aone1: One R2
Anegate1: Negate R2
H1: IsCRing R2
f: R1 -> R2
g: Z -> R1
h: Z -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z
f (g x) = h x
Proof.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R1: Type
Aplus0: Plus R1
Amult0: Mult R1
Azero0: Zero R1
Aone0: One R1
Anegate0: Negate R1
H0: IsCRing R1
R2: Type
Aplus1: Plus R2
Amult1: Mult R2
Azero1: Zero R2
Aone1: One R2
Anegate1: Negate R2
H1: IsCRing R2
f: R1 -> R2
g: Z -> R1
h: Z -> R2
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z
f (g x) = h x exact (to_ring_unique_alt (f ∘ g) h _). Qed.

Lemma to_ring_self `{Integers Z} (f : Z -> Z) `{!IsSemiRingPreserving f} x : f x = x.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
f: Z -> Z
IsSemiRingPreserving0: IsSemiRingPreserving f
x: Z
f x = x
Proof.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
f: Z -> Z
IsSemiRingPreserving0: IsSemiRingPreserving f
x: Z
f x = x exact (to_ring_unique_alt f id _). Qed.

(* A ring morphism from integers to another ring is injective
   if there's an injection in the other direction: *)
Lemma to_ring_injective `{Integers Z} `{IsCRing R} (f: R -> Z) (g: Z -> R)
  `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g}
  : IsInjective g.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: R -> Z
g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
IsInjective g
Proof.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: R -> Z
g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
IsInjective g
intros x y E.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: R -> Z
g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x, y: Z
E: g x = g y
x = y
change (id x = id y).
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: R -> Z
g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x, y: Z
E: g x = g y
id x = id y
rewrite <-(to_ring_twice f g id x), <-(to_ring_twice f g id y).
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H0: IsCRing R
f: R -> Z
g: Z -> R
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving g
x, y: Z
E: g x = g y
f (g x) = f (g y)
apply ap,E.
Qed.

Global Instance integers_to_integers_injective `{Integers Z} `{Integers Z2}
  (f: Z -> Z2) `{!IsSemiRingPreserving f}
  : IsInjective f.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
Z2: Type
Aap0: Apart Z2
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
Ale0: Le Z2
Alt0: Lt Z2
U0: IntegersToRing Z2
H0: Integers Z2
f: Z -> Z2
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective f
Proof.
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H: Integers Z
Z2: Type
Aap0: Apart Z2
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
Ale0: Le Z2
Alt0: Lt Z2
U0: IntegersToRing Z2
H0: Integers Z2
f: Z -> Z2
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective f exact (to_ring_injective (integers_to_ring Z2 Z) _). Qed.

Global Instance naturals_to_integers_injective `{Funext} `{Univalence}
  `{Integers@{i i i i i i i i} Z} `{Naturals@{i i i i i i i i} N}
  (f: N -> Z) `{!IsSemiRingPreserving f}
  : IsInjective f.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective f
Proof.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving f
IsInjective f
intros x y E.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: N
E: f x = f y
x = y
apply (injective (cast N (NatPair.Z N))).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: N
E: f x = f y
' x = ' y
rewrite <-2!(naturals.to_semiring_twice (integers_to_ring Z (NatPair.Z N))
  f (cast N (NatPair.Z N))).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: N
E: f x = f y
integers_to_ring Z (NatPair.Z N) (f x) =
integers_to_ring Z (NatPair.Z N) (f y)
apply ap,E.
Qed.

Section retract_is_int.
  Context `{Funext}.
  Context `{Integers Z} `{IsCRing Z2}
    {Z2ap : Apart Z2} {Z2le Z2lt} `{!FullPseudoSemiRingOrder (A:=Z2) Z2le Z2lt}.
  Context (f : Z -> Z2) `{!IsEquiv f} `{!IsSemiRingPreserving f}
    `{!IsSemiRingPreserving (f^-1)}.

  (* If we make this an instance, then instance resolution will often loop *)
  Definition retract_is_int_to_ring : IntegersToRing Z2 := fun Z2 _ _ _ _ _ _ =>
    integers_to_ring Z Z2 ∘ f^-1.

  Section for_another_ring.
    Context `{IsCRing R}.

    Instance: IsSemiRingPreserving (integers_to_ring Z R ∘ f^-1) := {}.
    Context (h :  Z2 -> R) `{!IsSemiRingPreserving h}.

    Lemma same_morphism x : (integers_to_ring Z R ∘ f^-1) x = h x.
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
(integers_to_ring Z R ∘ f^-1) x = h x
    Proof.
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
(integers_to_ring Z R ∘ f^-1) x = h x
    transitivity ((h ∘ (f ∘ f^-1)) x).
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
(integers_to_ring Z R ∘ f^-1) x = (h ∘ (f ∘ f^-1)) x
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
(h ∘ (f ∘ f^-1)) x = h x
    -
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
(integers_to_ring Z R ∘ f^-1) x = (h ∘ (f ∘ f^-1)) x symmetry.
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
(h ∘ (f ∘ f^-1)) x = (integers_to_ring Z R ∘ f^-1) x apply (to_ring_unique (h ∘ f)).
    -
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
(h ∘ (f ∘ f^-1)) x = h x unfold Compose.
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
h (f (f^-1 x)) = h x apply ap.
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
R: Type
Aplus1: Plus R
Amult1: Mult R
Azero1: Zero R
Aone1: One R
Anegate1: Negate R
H2: IsCRing R
h: Z2 -> R
IsSemiRingPreserving2: IsSemiRingPreserving h
x: Z2
f (f^-1 x) = x
      apply eisretr.
    Qed.
  End for_another_ring.

  (* If we make this an instance, then instance resolution will often loop *)
  Lemma retract_is_int: Integers Z2 (U:=retract_is_int_to_ring).
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
Integers Z2
  Proof.
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
IsSemiRingPreserving1: IsSemiRingPreserving f^-1
Integers Z2
  split;try apply _.
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
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)
(Anegate0 : Negate B) (H : IsCRing B),
IsSemiRingPreserving (integers_to_ring Z2 B)
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
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) (Anegate0 : Negate B) 
(H : IsCRing B) (h : Z2 -> B),
IsSemiRingPreserving h ->
forall x : Z2, integers_to_ring Z2 B x = h x
  -
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
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)
(Anegate0 : Negate B) (H : IsCRing B),
IsSemiRingPreserving (integers_to_ring Z2 B) unfold integers_to_ring, retract_is_int_to_ring.
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
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)
(Anegate0 : Negate B) (H : IsCRing B),
IsSemiRingPreserving (integers_to_ring Z B ∘ f^-1) apply _.
  -
H: Funext
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H0: Integers Z
Z2: Type
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
H1: IsCRing Z2
Z2ap: Apart Z2
Z2le: Le Z2
Z2lt: Lt Z2
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder
  Z2le Z2lt
f: Z -> Z2
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)
(Anegate0 : Negate B) (H : IsCRing B) (h : Z2 -> B),
IsSemiRingPreserving h ->
forall x : Z2, integers_to_ring Z2 B x = h x intros;apply same_morphism;apply _.
  Qed.
End retract_is_int.

Section int_to_int_iso.

Context `{Integers Z1} `{Integers Z2}.

Global Instance int_to_int_equiv : IsEquiv (integers_to_ring Z1 Z2).
Z1: Type
Aap: Apart Z1
Aplus: Plus Z1
Amult: Mult Z1
Azero: Zero Z1
Aone: One Z1
Anegate: Negate Z1
Ale: Le Z1
Alt: Lt Z1
U: IntegersToRing Z1
H: Integers Z1
Z2: Type
Aap0: Apart Z2
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
Ale0: Le Z2
Alt0: Lt Z2
U0: IntegersToRing Z2
H0: Integers Z2
IsEquiv (integers_to_ring Z1 Z2)
Proof.
Z1: Type
Aap: Apart Z1
Aplus: Plus Z1
Amult: Mult Z1
Azero: Zero Z1
Aone: One Z1
Anegate: Negate Z1
Ale: Le Z1
Alt: Lt Z1
U: IntegersToRing Z1
H: Integers Z1
Z2: Type
Aap0: Apart Z2
Aplus0: Plus Z2
Amult0: Mult Z2
Azero0: Zero Z2
Aone0: One Z2
Anegate0: Negate Z2
Ale0: Le Z2
Alt0: Lt Z2
U0: IntegersToRing Z2
H0: Integers Z2
IsEquiv (integers_to_ring Z1 Z2)
apply Equivalences.isequiv_adjointify with (integers_to_ring Z2 Z1);
red;apply (to_ring_involutive _ _).
Defined.

End int_to_int_iso.


Section contents.
Universe U.

Context `{Funext} `{Univalence}.
Context (Z : Type@{U}) `{Integers@{U U U U U U U U} Z}.

Lemma from_int_stmt  (Z':Type@{U}) `{Integers@{U U U U U U U U} Z'}
  : forall (P : Rings.Operations -> Type),
  P (Rings.BuildOperations Z') -> P (Rings.BuildOperations Z).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
Z': Type
Aap0: Apart Z'
Aplus0: Plus Z'
Amult0: Mult Z'
Azero0: Zero Z'
Aone0: One Z'
Anegate0: Negate Z'
Ale0: Le Z'
Alt0: Lt Z'
U0: IntegersToRing Z'
H2: Integers Z'
forall P : Rings.Operations -> Type,
P (Rings.BuildOperations Z') ->
P (Rings.BuildOperations Z)
Proof.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
Z': Type
Aap0: Apart Z'
Aplus0: Plus Z'
Amult0: Mult Z'
Azero0: Zero Z'
Aone0: One Z'
Anegate0: Negate Z'
Ale0: Le Z'
Alt0: Lt Z'
U0: IntegersToRing Z'
H2: Integers Z'
forall P : Rings.Operations -> Type,
P (Rings.BuildOperations Z') ->
P (Rings.BuildOperations Z)
apply Rings.iso_leibnitz with (integers_to_ring Z' Z);apply _.
Qed.

Global Instance int_dec : DecidablePaths Z | 10.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
DecidablePaths Z
Proof.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
DecidablePaths Z
apply decidablepaths_equiv with (NatPair.Z nat)
  (integers_to_ring (NatPair.Z nat) Z);apply _.
Qed.

Global Instance slow_int_abs `{Naturals N} : IntAbs Z N | 10.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
IntAbs Z N
Proof.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
IntAbs Z N
intros x.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
({n : N & naturals_to_semiring N Z n = x} +
 {n : N & naturals_to_semiring N Z n = - x})%type
destruct (int_abs_sig (NatPair.Z N) N (integers_to_ring Z (NatPair.Z N) x))
as [[n E]|[n E]];[left|right];exists n.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
n: N
E: naturals_to_semiring N (NatPair.Z N) n =
integers_to_ring Z (NatPair.Z N) x
naturals_to_semiring N Z n = x
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
n: N
E: naturals_to_semiring N (NatPair.Z N) n =
- integers_to_ring Z (NatPair.Z N) x
naturals_to_semiring N Z n = - x
-
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
n: N
E: naturals_to_semiring N (NatPair.Z N) n =
integers_to_ring Z (NatPair.Z N) x
naturals_to_semiring N Z n = x apply (injective (integers_to_ring Z (NatPair.Z N))).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
n: N
E: naturals_to_semiring N (NatPair.Z N) n =
integers_to_ring Z (NatPair.Z N) x
integers_to_ring Z (NatPair.Z N)
  (naturals_to_semiring N Z n) =
integers_to_ring Z (NatPair.Z N) x
  rewrite <-E.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
n: N
E: naturals_to_semiring N (NatPair.Z N) n =
integers_to_ring Z (NatPair.Z N) x
integers_to_ring Z (NatPair.Z N)
  (naturals_to_semiring N Z n) =
naturals_to_semiring N (NatPair.Z N) n apply (naturals.to_semiring_twice _ _ _).
-
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
n: N
E: naturals_to_semiring N (NatPair.Z N) n =
- integers_to_ring Z (NatPair.Z N) x
naturals_to_semiring N Z n = - x apply (injective (integers_to_ring Z (NatPair.Z N))).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
n: N
E: naturals_to_semiring N (NatPair.Z N) n =
- integers_to_ring Z (NatPair.Z N) x
integers_to_ring Z (NatPair.Z N)
  (naturals_to_semiring N Z n) =
integers_to_ring Z (NatPair.Z N) (- x)
  rewrite rings.preserves_negate, <-E.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
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
x: Z
n: N
E: naturals_to_semiring N (NatPair.Z N) n =
- integers_to_ring Z (NatPair.Z N) x
integers_to_ring Z (NatPair.Z N)
  (naturals_to_semiring N Z n) =
naturals_to_semiring N (NatPair.Z N) n
  apply (naturals.to_semiring_twice _ _ _).
Qed.

Instance int_nontrivial : PropHolds ((1:Z) <>0).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
PropHolds ((1 : Z) <> 0)
Proof.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
PropHolds ((1 : Z) <> 0)
intros E.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
E: 1 = 0
Empty
apply (rings.is_ne_0 (1:nat)).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
E: 1 = 0
1 = 0
apply (injective (naturals_to_semiring nat Z)).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
E: 1 = 0
naturals_to_semiring nat Z 1 =
naturals_to_semiring nat Z 0
exact E. (* because [naturals_to_semiring nat] plays nice with 1 *)
Qed.

Global Instance int_zero_product : ZeroProduct Z.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
ZeroProduct Z
Proof.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
ZeroProduct Z
intros x y E.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
((x = 0) + (y = 0))%type
destruct (zero_product (integers_to_ring Z (NatPair.Z nat) x)
  (integers_to_ring Z (NatPair.Z nat) y)).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
integers_to_ring Z (NatPair.Z nat) x *
integers_to_ring Z (NatPair.Z nat) y = 0
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) x = 0
((x = 0) + (y = 0))%type
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) y = 0
((x = 0) + (y = 0))%type
-
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
integers_to_ring Z (NatPair.Z nat) x *
integers_to_ring Z (NatPair.Z nat) y = 0 rewrite <-(rings.preserves_mult (A:=Z)), E, (rings.preserves_0 (A:=Z)).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
0 = 0
  trivial.
-
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) x = 0
((x = 0) + (y = 0))%type left.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) x = 0
x = 0 apply (injective (integers_to_ring Z (NatPair.Z nat))).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) x = 0
integers_to_ring Z (NatPair.Z nat) x =
integers_to_ring Z (NatPair.Z nat) 0
  rewrite rings.preserves_0.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) x = 0
integers_to_ring Z (NatPair.Z nat) x = 0 trivial.
-
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) y = 0
((x = 0) + (y = 0))%type right.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) y = 0
y = 0 apply (injective (integers_to_ring Z (NatPair.Z nat))).
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) y = 0
integers_to_ring Z (NatPair.Z nat) y =
integers_to_ring Z (NatPair.Z nat) 0
  rewrite rings.preserves_0.
H: Funext
H0: Univalence
Z: Type
Aap: Apart Z
Aplus: Plus Z
Amult: Mult Z
Azero: Zero Z
Aone: One Z
Anegate: Negate Z
Ale: Le Z
Alt: Lt Z
U: IntegersToRing Z
H1: Integers Z
x, y: Z
E: x * y = 0
p: integers_to_ring Z (NatPair.Z nat) y = 0
integers_to_ring Z (NatPair.Z nat) y = 0 trivial.
Qed.

Global Instance int_integral_domain : IsIntegralDomain Z := {}.

End contents.