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

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

Section integers.
Context `{Funext} `{Univalence}.
Context `{Integers Z} `{!TrivialApart Z}.

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

Lemma induction
  (P: Z -> Type):
  P 0 -> (forall n, 0 ≤ n -> P n -> P (1 + n)) -> (forall n, n ≤ 0 -> P n -> P (n - 1)) ->
  forall n, P 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P 0 ->
(forall n : Z, 0 ≤ n -> P n -> P (1 + n)) ->
(forall n : Z, n ≤ 0 -> P n -> P (n - 1)) ->
forall n : Z, P 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P 0 ->
(forall n : Z, 0 ≤ n -> P n -> P (1 + n)) ->
(forall n : Z, n ≤ 0 -> P n -> P (n - 1)) ->
forall n : Z, P n
intros P0 Psuc1 Psuc2 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
P n
destruct (int_abs_sig Z nat n) as [[a A]|[a A]].
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
a: nat
A: naturals_to_semiring nat Z a = n
P 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
a: nat
A: naturals_to_semiring nat Z a = - n
P 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
a: nat
A: naturals_to_semiring nat Z a = n
P n rewrite <-A.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
a: nat
A: naturals_to_semiring nat Z a = n
P (naturals_to_semiring nat Z a) clear A.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
a: nat
P (naturals_to_semiring nat Z a) revert a.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
forall a : nat, P (naturals_to_semiring nat Z a)
  apply naturals.induction.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
P (naturals_to_semiring nat 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
forall n : nat,
P (naturals_to_semiring nat Z n) ->
P (naturals_to_semiring nat Z (1 + 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
P (naturals_to_semiring nat Z 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
P 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
forall n : nat,
P (naturals_to_semiring nat Z n) ->
P (naturals_to_semiring nat Z (1 + n)) intros m 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (naturals_to_semiring nat Z m)
P (naturals_to_semiring nat Z (1 + m))
    rewrite rings.preserves_plus, rings.preserves_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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (naturals_to_semiring nat Z m)
P (1 + naturals_to_semiring nat Z m)
    apply Psuc1.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (naturals_to_semiring nat Z m)
0 ≤ naturals_to_semiring nat Z m
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (naturals_to_semiring nat Z m)
P (naturals_to_semiring nat Z m)
    *
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (naturals_to_semiring nat Z m)
0 ≤ naturals_to_semiring nat Z m apply to_semiring_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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (naturals_to_semiring nat Z m)
P (naturals_to_semiring nat Z m) 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
a: nat
A: naturals_to_semiring nat Z a = - n
P n rewrite <-(negate_involutive n), <-A.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
a: nat
A: naturals_to_semiring nat Z a = - n
P (- naturals_to_semiring nat Z a)
  clear A.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
a: nat
P (- naturals_to_semiring nat Z a) revert a.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
forall a : nat, P (- naturals_to_semiring nat Z a) apply naturals.induction.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
P (- naturals_to_semiring nat 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
forall n : nat,
P (- naturals_to_semiring nat Z n) ->
P (- naturals_to_semiring nat Z (1 + 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
P (- naturals_to_semiring nat Z 0) rewrite rings.preserves_0, rings.negate_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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
P 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
forall n : nat,
P (- naturals_to_semiring nat Z n) ->
P (- naturals_to_semiring nat Z (1 + n)) intros m 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (- naturals_to_semiring nat Z m)
P (- naturals_to_semiring nat Z (1 + m))
    rewrite rings.preserves_plus, rings.preserves_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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (- naturals_to_semiring nat Z m)
P (- (1 + naturals_to_semiring nat Z m))
    rewrite rings.negate_plus_distr, commutativity.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (- naturals_to_semiring nat Z m)
P (- naturals_to_semiring nat Z m - 1)
    apply Psuc2.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (- naturals_to_semiring nat Z m)
- naturals_to_semiring nat Z m ≤ 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (- naturals_to_semiring nat Z m)
P (- naturals_to_semiring nat Z m)
    *
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (- naturals_to_semiring nat Z m)
- naturals_to_semiring nat Z m ≤ 0 apply naturals.negate_to_ring_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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc1: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
Psuc2: forall n : Z, n ≤ 0 -> P n -> P (n - 1)
n: Z
m: nat
E: P (- naturals_to_semiring nat Z m)
P (- naturals_to_semiring nat Z m) trivial.
Qed.

Lemma induction_nonneg
  (P: Z -> Type):
  P 0 -> (forall n, 0 ≤ n -> P n -> P (1 + n)) -> forall n, 0 ≤ n -> P 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P 0 ->
(forall n : Z, 0 ≤ n -> P n -> P (1 + n)) ->
forall n : Z, 0 ≤ n -> P 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P 0 ->
(forall n : Z, 0 ≤ n -> P n -> P (1 + n)) ->
forall n : Z, 0 ≤ n -> P n
intros P0 PS.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
forall n : Z, 0 ≤ n -> P n refine (induction _ _ _ _); 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
forall n : Z,
n ≤ 0 -> (0 ≤ n -> P n) -> 0 ≤ n - 1 -> P (n - 1)
intros n 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
P (n - 1)
destruct (rings.is_ne_0 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
1 = 0
apply (antisymmetry (≤)).
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
1 ≤ 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
0 ≤ 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
1 ≤ 0 apply (order_reflecting ((n - 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
n - 1 + 1 ≤ n - 1 + 0
  rewrite <-plus_assoc,plus_negate_l,2!plus_0_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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
n ≤ n - 1
  transitivity 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
0 ≤ 1 transitivity (n - 1);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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
n - 1 ≤ 1
  apply (order_reflecting (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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
1 + (n - 1) ≤ 2
  rewrite plus_comm,<-plus_assoc,plus_negate_l,plus_0_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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
n ≤ 2
  transitivity 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
n ≤ 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
0 ≤ 2
  +
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
n ≤ 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
PS: forall n : Z, 0 ≤ n -> P n -> P (1 + n)
n: Z
E1: n ≤ 0
X: 0 ≤ n -> P n
E2: 0 ≤ n - 1
0 ≤ 2 apply le_0_2.
Qed.

#[export] Instance: Biinduction 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
TrivialApart0: TrivialApart Z
Biinduction 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
TrivialApart0: TrivialApart Z
Biinduction Z
intros P P0 Psuc.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc: forall n : Z, P n <-> P (1 + n)
forall n : Z, P n apply induction; 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc: forall n : Z, P n <-> P (1 + n)
forall n : Z, 0 ≤ n -> P n -> P (1 + 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc: forall n : Z, P n <-> P (1 + n)
forall n : Z, n ≤ 0 -> P n -> P (n - 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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc: forall n : Z, P n <-> P (1 + n)
forall n : Z, 0 ≤ n -> P n -> P (1 + n) intros ??;apply Psuc.
-
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc: forall n : Z, P n <-> P (1 + n)
forall n : Z, n ≤ 0 -> P n -> P (n - 1) intros;apply Psuc.
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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc: forall n : Z, P n <-> P (1 + n)
n: Z
X: n ≤ 0
X0: P n
P (1 + (n - 1))
  rewrite plus_comm,<-plus_assoc,plus_negate_l,plus_0_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
TrivialApart0: TrivialApart Z
P: Z -> Type
P0: P 0
Psuc: forall n : Z, P n <-> P (1 + n)
n: Z
X: n ≤ 0
X0: P n
P n
  trivial.
Qed.

#[export] Instance slow_int_le_dec : forall x y: Z, Decidable (x ≤ y) | 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
TrivialApart0: TrivialApart Z
forall x y : Z, Decidable (x ≤ 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
TrivialApart0: TrivialApart Z
forall x y : Z, Decidable (x ≤ y)
intros 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
TrivialApart0: TrivialApart Z
x, y: Z
Decidable (x ≤ y)
(* otherwise Z_le gets defined using peano.nat_ring
   but we only know order_reflecting when using naturals.nat_ring *)
pose (naturals_ring) as E0.
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
TrivialApart0: TrivialApart Z
x, y: Z
E0:= naturals_ring: IsSemiCRing nat
Decidable (x ≤ y)
destruct (dec (integers_to_ring _ (NatPair.Z nat) x ≤
    integers_to_ring _ (NatPair.Z nat) y)) 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
TrivialApart0: TrivialApart Z
x, y: Z
E0:= naturals_ring: IsSemiCRing nat
E: integers_to_ring Z (NatPair.Z nat) x
≤ integers_to_ring Z (NatPair.Z nat) y
Decidable (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
TrivialApart0: TrivialApart Z
x, y: Z
E0:= naturals_ring: IsSemiCRing nat
E: ~
(integers_to_ring Z (NatPair.Z nat) x
 ≤ integers_to_ring Z (NatPair.Z nat) y)
Decidable (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
TrivialApart0: TrivialApart Z
x, y: Z
E0:= naturals_ring: IsSemiCRing nat
E: integers_to_ring Z (NatPair.Z nat) x
≤ integers_to_ring Z (NatPair.Z nat) y
Decidable (x ≤ y) 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
TrivialApart0: TrivialApart Z
x, y: Z
E0:= naturals_ring: IsSemiCRing nat
E: integers_to_ring Z (NatPair.Z nat) x
≤ integers_to_ring Z (NatPair.Z nat) y
x ≤ y apply (order_reflecting _) 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
TrivialApart0: TrivialApart Z
x, y: Z
E0:= naturals_ring: IsSemiCRing nat
E: x ≤ y
x ≤ y 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
TrivialApart0: TrivialApart Z
x, y: Z
E0:= naturals_ring: IsSemiCRing nat
E: ~
(integers_to_ring Z (NatPair.Z nat) x
 ≤ integers_to_ring Z (NatPair.Z nat) y)
Decidable (x ≤ y) 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
TrivialApart0: TrivialApart Z
x, y: Z
E0:= naturals_ring: IsSemiCRing nat
E: ~
(integers_to_ring Z (NatPair.Z nat) x
 ≤ integers_to_ring Z (NatPair.Z nat) y)
~ (x ≤ y) intro;apply E;apply (order_preserving _);trivial.
Qed.
End integers.