int_abs.v

Require Import
  HoTT.Classes.interfaces.naturals
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.orders.nat_int
  HoTT.Classes.theory.integers
  HoTT.Classes.theory.rings
  HoTT.Classes.theory.groups
  HoTT.Classes.orders.rings.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Generalizable Variables N Z Zle Zlt R f.

Section contents.
Context `{Funext} `{Univalence}.
Context `{Integers Z} `{Apart Z} `{!TrivialApart Z}
  `{!FullPseudoSemiRingOrder Zle Zlt} `{Naturals N}.

(* Add Ring Z : (rings.stdlib_ring_theory Z). *)

Lemma int_abs_unique (a b : IntAbs Z N) (z : Z) :
  int_abs Z N (ia:=a) z = int_abs Z N (ia:=b) 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
int_abs Z N z = int_abs Z N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
int_abs Z N z = int_abs Z N z
unfold int_abs.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
match int_abs_sig Z N z with
| inl s => s.1
| inr s => s.1
end =
match int_abs_sig Z N z with
| inl s => s.1
| inr s => s.1
end
destruct (int_abs_sig Z N (IntAbs:=a) z) as [[n1 E1]|[n1 E1]];
destruct (int_abs_sig Z N (IntAbs:=b) z) as [[n2 E2]|[n2 E2]].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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = z
n1 = n2
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = - z
n1 = n2
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = z
n1 = n2
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = - z
n1 = n2
-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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = z
n1 = n2 apply (injective (naturals_to_semiring N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = z
naturals_to_semiring N Z n1 =
naturals_to_semiring N Z n2 path_via 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = - z
n1 = n2 assert (E : n1 + n2 = 0);[|path_via 0;[|symmetry];
  apply (naturals.zero_sum _ _ 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = - z
n1 + n2 = 0
  apply (injective (naturals_to_semiring N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = - z
naturals_to_semiring N Z (n1 + n2) =
naturals_to_semiring N Z 0
  rewrite preserves_0,preserves_plus.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = - z
naturals_to_semiring N Z n1 +
naturals_to_semiring N Z n2 = 0
  rewrite E1,E2.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = z
n2: N
E2: naturals_to_semiring N Z n2 = - z
z - z = 0
  apply plus_negate_r.
-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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = z
n1 = n2 assert (E : n1 + n2 = 0);[|path_via 0;[|symmetry];
  apply (naturals.zero_sum _ _ 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = z
n1 + n2 = 0
  apply (injective (naturals_to_semiring N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = z
naturals_to_semiring N Z (n1 + n2) =
naturals_to_semiring N Z 0
  rewrite preserves_0,preserves_plus.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = z
naturals_to_semiring N Z n1 +
naturals_to_semiring N Z n2 = 0
  rewrite E1,E2.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = z
- z + z = 0
  apply plus_negate_l.
-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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = - z
n1 = n2 apply (injective (naturals_to_semiring N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
a, b: IntAbs Z N
z: Z
n1: N
E1: naturals_to_semiring N Z n1 = - z
n2: N
E2: naturals_to_semiring N Z n2 = - z
naturals_to_semiring N Z n1 =
naturals_to_semiring N Z n2 path_via (- z).
Qed.

Context `{!IntAbs Z N}.

Context `{!IsSemiRingPreserving (f : N -> Z)}.

Lemma int_abs_spec x :
  (0 ≤ x /\ f (int_abs Z N x) = x) |_| (x ≤ 0 /\ f (int_abs Z N x) = -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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
((0 ≤ x) * (f (int_abs Z N x) = x) +
 (x ≤ 0) * (f (int_abs Z N x) = - x))%type
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
((0 ≤ x) * (f (int_abs Z N x) = x) +
 (x ≤ 0) * (f (int_abs Z N x) = - x))%type
unfold int_abs.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
((0 ≤ x) *
 (f
    match int_abs_sig Z N x with
    | inl s => s.1
    | inr s => s.1
    end = x) +
 (x ≤ 0) *
 (f
    match int_abs_sig Z N x with
    | inl s => s.1
    | inr s => s.1
    end = - x))%type destruct (int_abs_sig Z N x) as [[n E]|[n 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = x
((0 ≤ x) * (f n = x) + (x ≤ 0) * (f n = - x))%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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
((0 ≤ x) * (f n = x) + (x ≤ 0) * (f n = - x))%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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = x
((0 ≤ x) * (f n = x) + (x ≤ 0) * (f n = - x))%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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = x
((0 ≤ x) * (f n = x))%type 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = x
((0 ≤ naturals_to_semiring N Z n) *
 (f n = naturals_to_semiring N Z n))%type split.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = x
0 ≤ naturals_to_semiring N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = x
f n = naturals_to_semiring N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = x
0 ≤ naturals_to_semiring N Z n eapply @to_semiring_nonneg;apply _.
  +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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = x
f n = naturals_to_semiring N Z n apply (naturals.to_semiring_unique_alt _ _).
-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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
((0 ≤ x) * (f n = x) + (x ≤ 0) * (f n = - x))%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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
((x ≤ 0) * (f n = - x))%type split.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
x ≤ 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
f 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
x ≤ 0 apply flip_nonpos_negate.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
0 ≤ - 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
0 ≤ naturals_to_semiring N Z n eapply @to_semiring_nonneg;apply _.
  +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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
f 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
n: N
E: naturals_to_semiring N Z n = - x
f n = naturals_to_semiring N Z n apply (naturals.to_semiring_unique_alt _ _).
Qed.

Lemma int_abs_sig_alt x :
  (sig (fun n : N => f n = x)) |_| (sig (fun n : N => f 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
({n : N & f n = x} + {n : N & f n = - x})%type
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
({n : N & f n = x} + {n : N & f n = - x})%type destruct (int_abs_spec x) as [[??]|[??]]; eauto. Qed.

Lemma int_abs_nat n :
  int_abs Z N (f n) = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
int_abs Z N (f n) = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
int_abs Z N (f n) = n
apply (injective 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
f (int_abs Z N (f n)) = f n
destruct (int_abs_spec (f n)) as [[? E]|[? E]];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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: f n ≤ 0
E: f (int_abs Z N (f n)) = - f n
f (int_abs Z N (f n)) = f n
apply naturals.negate_to_ring.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: f n ≤ 0
E: f (int_abs Z N (f n)) = - f n
- f (int_abs Z N (f n)) = f n rewrite E, involutive.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: f n ≤ 0
E: f (int_abs Z N (f n)) = - f n
f n = f n trivial.
Qed.

Lemma int_abs_negate_nat n :
  int_abs Z N (-f n) = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
int_abs Z N (- f n) = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
int_abs Z N (- f n) = n
apply (injective 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
f (int_abs Z N (- f n)) = f n destruct (int_abs_spec (-f n)) as [[? E]|[? 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: 0 ≤ - f n
E: f (int_abs Z N (- f n)) = - f n
f (int_abs Z N (- f n)) = f 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: - f n ≤ 0
E: f (int_abs Z N (- f n)) = - - f n
f (int_abs Z N (- f n)) = f 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: 0 ≤ - f n
E: f (int_abs Z N (- f n)) = - f n
f (int_abs Z N (- f n)) = f n symmetry.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: 0 ≤ - f n
E: f (int_abs Z N (- f n)) = - f n
f n = f (int_abs Z N (- f n)) apply naturals.negate_to_ring.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: 0 ≤ - f n
E: f (int_abs Z N (- f n)) = - f n
- f n = f (int_abs Z N (- f n)) apply symmetry; 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: - f n ≤ 0
E: f (int_abs Z N (- f n)) = - - f n
f (int_abs Z N (- f n)) = f n rewrite involutive in 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
n: N
fst: - f n ≤ 0
E: f (int_abs Z N (- f n)) = f n
f (int_abs Z N (- f n)) = f n trivial.
Qed.

Lemma int_abs_negate x :
  int_abs Z N (-x) = int_abs 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
int_abs Z N (- x) = int_abs Z N x
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
int_abs Z N (- x) = int_abs Z N x
destruct (int_abs_spec x) as [[_ E]|[_ 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: f (int_abs Z N x) = x
int_abs Z N (- x) = int_abs 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: f (int_abs Z N x) = - x
int_abs Z N (- x) = int_abs 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: f (int_abs Z N x) = x
int_abs Z N (- x) = int_abs Z N x path_via (int_abs Z N (- f (int_abs 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: f (int_abs Z N x) = x
int_abs Z N (- f (int_abs Z N x)) = int_abs Z N x
  apply int_abs_negate_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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: f (int_abs Z N x) = - x
int_abs Z N (- x) = int_abs 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: f (int_abs Z N x) = - x
int_abs Z N (f (int_abs Z N x)) = int_abs Z N x apply int_abs_nat.
Qed.

Lemma int_abs_0_alt x : int_abs Z N x = 0 <-> x = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
int_abs Z N x = 0 <-> x = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
int_abs Z N x = 0 <-> x = 0
split; intros E1.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: int_abs Z N x = 0
x = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: x = 0
int_abs Z N x = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: int_abs Z N x = 0
x = 0 destruct (int_abs_spec x) as [[_ E2]|[_ E2]];[|apply flip_negate_0];
  rewrite <-E2, E1, (preserves_0 (f:=f)); 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: x = 0
int_abs Z N x = 0 rewrite E1, <-(preserves_0 (f:=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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: x = 0
int_abs Z N (f 0) = 0 apply int_abs_nat.
Qed.

Lemma int_abs_ne_0 x : int_abs Z N x <> 0 <-> x <> 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
int_abs Z N x <> 0 <-> x <> 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
int_abs Z N x <> 0 <-> x <> 0
destruct (int_abs_0_alt 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
fst: int_abs Z N x = 0 -> x = 0
snd: x = 0 -> int_abs Z N x = 0
int_abs Z N x <> 0 <-> x <> 0
split;intros E1 E2;auto.
Qed.

Lemma int_abs_0 : int_abs Z N 0 = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
int_abs Z N 0 = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
int_abs Z N 0 = 0 apply int_abs_0_alt;trivial. Qed.

Lemma int_abs_nonneg x :
  0 ≤ x -> f (int_abs Z N x) = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
0 ≤ x -> f (int_abs Z N x) = x
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
0 ≤ x -> f (int_abs Z N x) = x
intros E1.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: 0 ≤ x
f (int_abs Z N x) = x destruct (int_abs_spec x) as [[n E2]|[n E2]];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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: 0 ≤ x
n: x ≤ 0
E2: f (int_abs Z N x) = - x
f (int_abs Z N x) = x
assert (Hrw : x = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: 0 ≤ x
n: x ≤ 0
E2: f (int_abs Z N x) = - x
x = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: 0 ≤ x
n: x ≤ 0
E2: f (int_abs Z N x) = - x
Hrw: x = 0
f (int_abs Z N x) = 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: 0 ≤ x
n: x ≤ 0
E2: f (int_abs Z N x) = - x
x = 0 apply (antisymmetry (<=));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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: 0 ≤ x
n: x ≤ 0
E2: f (int_abs Z N x) = - x
Hrw: x = 0
f (int_abs Z N x) = x rewrite Hrw,int_abs_0, (preserves_0 (f:=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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E1: 0 ≤ x
n: x ≤ 0
E2: f (int_abs Z N x) = - x
Hrw: x = 0
0 = 0 trivial.
Qed.

Lemma int_abs_nonpos x :
  x ≤ 0 -> f (int_abs Z N x) = -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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
x ≤ 0 -> f (int_abs Z N x) = - x
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
x ≤ 0 -> f (int_abs Z N x) = - x
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: x ≤ 0
f (int_abs Z N x) = - x rewrite <-int_abs_negate, int_abs_nonneg; auto.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: x ≤ 0
0 ≤ - x
apply flip_nonpos_negate.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x: Z
E: x ≤ 0
x ≤ 0 trivial.
Qed.

Lemma int_abs_1 : int_abs Z N 1 = 1.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
int_abs Z N 1 = 1
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
int_abs Z N 1 = 1
apply (injective 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
f (int_abs Z N 1) = f 1 rewrite (preserves_1 (f:=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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
f (int_abs Z N 1) = 1
apply int_abs_nonneg; solve_propholds.
Qed.

Lemma int_abs_nonneg_plus x y :
  0 ≤ x -> 0 ≤ y -> int_abs Z N (x + y) = int_abs Z N x + int_abs Z N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
0 ≤ x ->
0 ≤ y ->
int_abs Z N (x + y) = int_abs Z N x + int_abs Z N y
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
0 ≤ x ->
0 ≤ y ->
int_abs Z N (x + y) = int_abs Z N x + int_abs Z N y
intros.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
X: 0 ≤ x
X0: 0 ≤ y
int_abs Z N (x + y) = int_abs Z N x + int_abs Z N y apply (injective 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
X: 0 ≤ x
X0: 0 ≤ y
f (int_abs Z N (x + y)) =
f (int_abs Z N x + int_abs Z N y)
rewrite (preserves_plus (f:=f)), !int_abs_nonneg;auto.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
X: 0 ≤ x
X0: 0 ≤ y
0 ≤ x + y
apply nonneg_plus_compat;trivial.
Qed.

Lemma int_abs_mult x y :
  int_abs Z N (x * y) = int_abs Z N x * int_abs Z N 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
int_abs Z N (x * y) = int_abs Z N x * int_abs Z N y
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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
int_abs Z N (x * y) = int_abs Z N x * int_abs Z N y
apply (injective 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
f (int_abs Z N (x * y)) =
f (int_abs Z N x * int_abs Z N y) rewrite (preserves_mult (f:=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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
f (int_abs Z N (x * y)) =
f (int_abs Z N x) * f (int_abs Z N y)
destruct (int_abs_spec x) as [[? Ex]|[? Ex]],
   (int_abs_spec y) as [[? Ey]|[? Ey]]; rewrite Ex, Ey.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
f (int_abs Z N (x * y)) = x * 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
f (int_abs Z N (x * y)) = x * - 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
f (int_abs Z N (x * y)) = - x * 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
f (int_abs Z N (x * y)) = - x * - 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
f (int_abs Z N (x * y)) = x * y rewrite int_abs_nonneg;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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
0 ≤ x * y apply nonneg_mult_compat;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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
f (int_abs Z N (x * y)) = x * - y rewrite int_abs_nonpos.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
- (x * y) = x * - 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
x * 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
- (x * y) = x * - y apply negate_mult_distr_r.
  +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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: 0 ≤ x
Ex: f (int_abs Z N x) = x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
x * y ≤ 0 apply nonneg_nonpos_mult;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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
f (int_abs Z N (x * y)) = - x * y rewrite int_abs_nonpos.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
- (x * y) = - x * 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
x * 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
- (x * y) = - x * y apply negate_mult_distr_l.
  +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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: 0 ≤ y
Ey: f (int_abs Z N y) = y
x * y ≤ 0 apply nonpos_nonneg_mult;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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
f (int_abs Z N (x * y)) = - x * - y rewrite int_abs_nonneg.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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
x * y = - x * - 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
0 ≤ x * 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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
x * y = - x * - y symmetry;apply negate_mult_negate.
  +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
H2: Apart Z
TrivialApart0: TrivialApart Z
Zle: Le Z
Zlt: Lt Z
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Zle
  Zlt
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
H3: Naturals N
IntAbs0: IntAbs Z N
f: N -> Z
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : N -> Z)
x, y: Z
fst: x ≤ 0
Ex: f (int_abs Z N x) = - x
fst0: y ≤ 0
Ey: f (int_abs Z N y) = - y
0 ≤ x * y apply nonpos_mult;trivial.
Qed.
End contents.