peano_naturals.v

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

Local Open Scope nat_scope.
Local Open Scope mc_scope.

Local Set Universe Minimization ToSet.

(* This should go away one Coq has universe cumulativity through inductives. *)
Section nat_lift.

Universe N.
(* It's important that the universe [N] be free.  Occasionally, Coq will choose universe variables in proofs that force [N] to be [Set].  To pinpoint where this happens, you can add the line [Constraint Set < N.] here, and see what fails below. *)

Let natpaths := @paths@{N} nat.
Infix "=N=" := natpaths.

Definition natpaths_symm : Symmetric@{N N} natpaths.natpaths:= paths: nat -> nat -> Type
Symmetric natpaths
Proof.natpaths:= paths: nat -> nat -> Type
Symmetric natpaths
  unfold natpaths; apply _.
Defined.

Global Instance nat_0: Zero@{N} nat := 0%nat.
Global Instance nat_1: One@{N} nat := 1%nat.

Global Instance nat_plus: Plus@{N} nat := Nat.Core.add.

Notation mul := Nat.Core.mul.

Global Instance nat_mult: Mult@{N} nat := Nat.Core.mul.

Ltac simpl_nat :=
  change (@plus nat _) with Nat.Core.add;
  change (@mult nat _) with Nat.Core.mul;
  simpl;
  change Nat.Core.add with (@plus nat Nat.Core.add);
  change Nat.Core.mul with (@mult nat Nat.Core.mul).

(** [0 + a =N= a] *)
Local Instance add_0_l : LeftIdentity@{N N} (plus : Plus nat) 0 := fun _ => idpath.

Definition add_S_l a b : S a + b =N= S (a + b) := idpath.

(** [a + 0 =N= a] *)
Local Instance add_0_r : RightIdentity@{N N} (plus : Plus nat) (zero : Zero nat).natpaths:= paths: nat -> nat -> Type
RightIdentity (plus : Plus nat) (0 : Zero nat)
Proof.natpaths:= paths: nat -> nat -> Type
RightIdentity (plus : Plus nat) (0 : Zero nat)
  intros a; induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
0 + 0 = 0
natpaths:= paths: nat -> nat -> Type
a: nat
IHa: a + 0 = a
a.+1 + 0 = a.+1
  -natpaths:= paths: nat -> nat -> Type
0 + 0 = 0 reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a: nat
IHa: a + 0 = a
a.+1 + 0 = a.+1 apply (ap S), IHa.
Qed.

Lemma add_S_r : forall a b, a + S b =N= S (a + b).natpaths:= paths: nat -> nat -> Type
forall a b : nat, a + b.+1 =N= (a + b).+1
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a + b.+1 =N= (a + b).+1
  intros a b; induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
b: nat
0 + b.+1 =N= (0 + b).+1
natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a + b.+1 =N= (a + b).+1
a.+1 + b.+1 =N= (a.+1 + b).+1
  -natpaths:= paths: nat -> nat -> Type
b: nat
0 + b.+1 =N= (0 + b).+1 reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a + b.+1 =N= (a + b).+1
a.+1 + b.+1 =N= (a.+1 + b).+1 apply (ap S), IHa.
Qed.

(** [forall a b c : nat, a + (b + c) = (a + b) + c].  The RHS is written [a + b + c]. *)
Local Instance add_assoc : Associative@{N} (plus : Plus nat).natpaths:= paths: nat -> nat -> Type
Associative (plus : Plus nat)
Proof.natpaths:= paths: nat -> nat -> Type
Associative (plus : Plus nat)
  intros a b c; induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
b, c: nat
0 + (b + c) = 0 + b + c
natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a + (b + c) = a + b + c
a.+1 + (b + c) = a.+1 + b + c
  -natpaths:= paths: nat -> nat -> Type
b, c: nat
0 + (b + c) = 0 + b + c reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a + (b + c) = a + b + c
a.+1 + (b + c) = a.+1 + b + c change (S (a + (b + c)) = S (a + b + c)).natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a + (b + c) = a + b + c
(a + (b + c)).+1 = (a + b + c).+1
    apply (ap S), IHa.
Qed.

Local Instance add_comm : Commutative@{N N} (plus : Plus nat).natpaths:= paths: nat -> nat -> Type
Commutative (plus : Plus nat)
Proof.natpaths:= paths: nat -> nat -> Type
Commutative (plus : Plus nat)
  intros a b; induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
b: nat
0 + b = b + 0
natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a + b = b + a
a.+1 + b = b + a.+1
  -natpaths:= paths: nat -> nat -> Type
b: nat
0 + b = b + 0 rhs apply add_0_r.natpaths:= paths: nat -> nat -> Type
b: nat
0 + b = b
    reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a + b = b + a
a.+1 + b = b + a.+1 rhs apply add_S_r.natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a + b = b + a
a.+1 + b = (b + a).+1
    apply (ap S), IHa.
Qed.

Local Instance mul_0_l : LeftAbsorb@{N N} (mult : Mult nat) (zero : Zero nat)
  := fun _ => idpath.

Definition mul_S_l a b : (S a) * b =N= b + a * b := idpath.

(** [1 * a =N= a]. *)
Local Instance mul_1_l : LeftIdentity@{N N} (mult : Mult nat) (one : One nat)
  := add_0_r.

Local Instance mul_0_r : RightAbsorb@{N N} (mult : Mult nat) (zero : Zero nat).natpaths:= paths: nat -> nat -> Type
RightAbsorb (mult : Mult nat) (0 : Zero nat)
Proof.natpaths:= paths: nat -> nat -> Type
RightAbsorb (mult : Mult nat) (0 : Zero nat)
  intros a; induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
0 * 0 = 0
natpaths:= paths: nat -> nat -> Type
a: nat
IHa: a * 0 = 0
a.+1 * 0 = 0
  -natpaths:= paths: nat -> nat -> Type
0 * 0 = 0 reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a: nat
IHa: a * 0 = 0
a.+1 * 0 = 0 change (a * 0 = 0).natpaths:= paths: nat -> nat -> Type
a: nat
IHa: a * 0 = 0
a * 0 = 0
    exact IHa.
Qed.

Lemma mul_S_r a b : a * S b =N= a + a * b.natpaths:= paths: nat -> nat -> Type
a, b: nat
a * b.+1 =N= a + a * b
Proof.natpaths:= paths: nat -> nat -> Type
a, b: nat
a * b.+1 =N= a + a * b
  induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
b: nat
0 * b.+1 =N= 0 + 0 * b
natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b.+1 =N= a + a * b
a.+1 * b.+1 =N= a.+1 + a.+1 * b
  -natpaths:= paths: nat -> nat -> Type
b: nat
0 * b.+1 =N= 0 + 0 * b reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b.+1 =N= a + a * b
a.+1 * b.+1 =N= a.+1 + a.+1 * b change (S (b + a * S b) = S (a + (b + a * b))).natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b.+1 =N= a + a * b
(b + a * b.+1).+1 = (a + (b + a * b)).+1
    apply (ap S).natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b.+1 =N= a + a * b
b + a * b.+1 = a + (b + a * b)
    rhs rapply add_assoc.natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b.+1 =N= a + a * b
b + a * b.+1 = a + b + a * b
    rhs rapply (ap (fun x => x + _) (add_comm _ _)).natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b.+1 =N= a + a * b
b + a * b.+1 = b + a + a * b
    rhs rapply (add_assoc _ _ _)^.natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b.+1 =N= a + a * b
b + a * b.+1 = b + (a + a * b)
    exact (ap (plus b) IHa).
Qed.

(** [a * 1 =N= a]. *)
Local Instance mul_1_r : RightIdentity@{N N} (mult : Mult nat) (one : One nat).natpaths:= paths: nat -> nat -> Type
RightIdentity (mult : Mult nat) (1 : One nat)
Proof.natpaths:= paths: nat -> nat -> Type
RightIdentity (mult : Mult nat) (1 : One nat)
  intros a.natpaths:= paths: nat -> nat -> Type
a: nat
a * 1 = a
  lhs nrapply mul_S_r.natpaths:= paths: nat -> nat -> Type
a: nat
a + a * 0 = a
  lhs nrapply (ap _ (mul_0_r a)).natpaths:= paths: nat -> nat -> Type
a: nat
a + 0 = a
  apply add_0_r.
Qed.

Local Instance mul_comm : Commutative@{N N} (mult : Mult nat).natpaths:= paths: nat -> nat -> Type
Commutative (mult : Mult nat)
Proof.natpaths:= paths: nat -> nat -> Type
Commutative (mult : Mult nat)
  intros a b; induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
b: nat
0 * b = b * 0
natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b = b * a
a.+1 * b = b * a.+1
  -natpaths:= paths: nat -> nat -> Type
b: nat
0 * b = b * 0 rhs apply mul_0_r.natpaths:= paths: nat -> nat -> Type
b: nat
0 * b = 0
    reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b = b * a
a.+1 * b = b * a.+1 rhs apply mul_S_r.natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b = b * a
a.+1 * b = b + b * a
    change (b + a * b = b + b * a).natpaths:= paths: nat -> nat -> Type
a, b: nat
IHa: a * b = b * a
b + a * b = b + b * a
    apply (ap (fun x => b + x)), IHa.
Qed.

(** [a * (b + c) =N= a * b + a * c]. *)
Local Instance add_mul_distr_l
  : LeftDistribute@{N} (mult : Mult nat) (plus : Plus nat).natpaths:= paths: nat -> nat -> Type
LeftDistribute (mult : Mult nat) (plus : Plus nat)
Proof.natpaths:= paths: nat -> nat -> Type
LeftDistribute (mult : Mult nat) (plus : Plus nat)
  intros a b c; induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
b, c: nat
0 * (b + c) = 0 * b + 0 * c
natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
a.+1 * (b + c) = a.+1 * b + a.+1 * c
  -natpaths:= paths: nat -> nat -> Type
b, c: nat
0 * (b + c) = 0 * b + 0 * c reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
a.+1 * (b + c) = a.+1 * b + a.+1 * c change ((b + c) + a * (b + c) = (b + a * b) + (c + a * c)).natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
b + c + a * (b + c) = b + a * b + (c + a * c)
    lhs rapply (add_assoc _ _ _)^.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
b + (c + a * (b + c)) = b + a * b + (c + a * c)
    rhs rapply (add_assoc _ _ _)^.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
b + (c + a * (b + c)) = b + (a * b + (c + a * c))
    apply (ap (plus b)).natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
c + a * (b + c) = a * b + (c + a * c)
    rhs rapply add_assoc.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
c + a * (b + c) = a * b + c + a * c
    rhs rapply (ap (fun x => x + _) (add_comm _ _)).natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
c + a * (b + c) = c + a * b + a * c
    rhs rapply (add_assoc _ _ _)^.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b + c) = a * b + a * c
c + a * (b + c) = c + (a * b + a * c)
    apply (ap (plus c)), IHa.
Qed.

(** [(a + b) * c =N= a * c + b * c].  This also follows from [plus_mult_distr_r], which currently requires that we already have a semiring.  It should be adjusted to not require associativity. *)
Local Instance add_mul_distr_r
  : RightDistribute@{N} (mult : Mult nat) (plus : Plus nat).natpaths:= paths: nat -> nat -> Type
RightDistribute (mult : Mult nat) (plus : Plus nat)
Proof.natpaths:= paths: nat -> nat -> Type
RightDistribute (mult : Mult nat) (plus : Plus nat)
  intros a b c.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
(a + b) * c = a * c + b * c
  lhs apply mul_comm.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
c * (a + b) = a * c + b * c
  lhs apply add_mul_distr_l.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
c * a + c * b = a * c + b * c
  apply ap011; apply mul_comm.
Defined.

Local Instance mul_assoc : Associative@{N} (mult : Mult nat).natpaths:= paths: nat -> nat -> Type
Associative (mult : Mult nat)
Proof.natpaths:= paths: nat -> nat -> Type
Associative (mult : Mult nat)
 intros a b c; induction a as [| a IHa].natpaths:= paths: nat -> nat -> Type
b, c: nat
0 * (b * c) = 0 * b * c
natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b * c) = a * b * c
a.+1 * (b * c) = a.+1 * b * c
  -natpaths:= paths: nat -> nat -> Type
b, c: nat
0 * (b * c) = 0 * b * c reflexivity.
  -natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b * c) = a * b * c
a.+1 * (b * c) = a.+1 * b * c simpl_nat.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b * c) = a * b * c
b * c + a * (b * c) = (b + a * b) * c
    rhs apply add_mul_distr_r.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
IHa: a * (b * c) = a * b * c
b * c + a * (b * c) = b * c + a * b * c
    apply ap, IHa.
Qed.

Global Instance S_neq_0 x : PropHolds (~ (S x =N= 0)).natpaths:= paths: nat -> nat -> Type
x: nat
PropHolds (~ (x.+1 =N= 0))
Proof.natpaths:= paths: nat -> nat -> Type
x: nat
PropHolds (~ (x.+1 =N= 0))
intros E.natpaths:= paths: nat -> nat -> Type
x: nat
E: x.+1 =N= 0
Empty
change ((fun a => match a with S _ => Unit | 0%nat => Empty end) 0).natpaths:= paths: nat -> nat -> Type
x: nat
E: x.+1 =N= 0
(fun a : nat =>
 match a with
 | 0 => Empty
 | _.+1 => Unit
 end) 0
eapply transport.natpaths:= paths: nat -> nat -> Type
x: nat
E: x.+1 =N= 0
?a = 0
natpaths:= paths: nat -> nat -> Type
x: nat
E: x.+1 =N= 0
match ?a with
| 0 => Empty
| _.+1 => Unit
end
-natpaths:= paths: nat -> nat -> Type
x: nat
E: x.+1 =N= 0
?a = 0 exact E.
-natpaths:= paths: nat -> nat -> Type
x: nat
E: x.+1 =N= 0
match x.+1 with
| 0 => Empty
| _.+1 => Unit
end split.
Qed.

Definition pred x := match x with | 0%nat => 0 | S k => k end.

Global Instance S_inj : IsInjective@{N N} S
  := { injective := fun a b E => ap pred E }.

(** This is also in Spaces.Nat.Core. *)
Global Instance nat_dec: DecidablePaths@{N} nat.natpaths:= paths: nat -> nat -> Type
DecidablePaths nat
Proof.natpaths:= paths: nat -> nat -> Type
DecidablePaths nat
hnf.natpaths:= paths: nat -> nat -> Type
forall x y : nat, Decidable (x = y)
apply (nat_rect@{N} (fun x => forall y, _)).natpaths:= paths: nat -> nat -> Type
forall y : nat, Decidable (0 = y)
natpaths:= paths: nat -> nat -> Type
forall n : nat,
(forall y : nat, Decidable (n = y)) ->
forall y : nat, Decidable (n.+1 = y)
-natpaths:= paths: nat -> nat -> Type
forall y : nat, Decidable (0 = y) intros [|b].natpaths:= paths: nat -> nat -> Type
Decidable (0 = 0)
natpaths:= paths: nat -> nat -> Type
b: nat
Decidable (0 = b.+1)
  +natpaths:= paths: nat -> nat -> Type
Decidable (0 = 0) left;reflexivity.
  +natpaths:= paths: nat -> nat -> Type
b: nat
Decidable (0 = b.+1) right;apply symmetric_neq,S_neq_0.
-natpaths:= paths: nat -> nat -> Type
forall n : nat,
(forall y : nat, Decidable (n = y)) ->
forall y : nat, Decidable (n.+1 = y) intros a IHa [|b].natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
Decidable (a.+1 = 0)
natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
Decidable (a.+1 = b.+1)
  +natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
Decidable (a.+1 = 0) right;apply S_neq_0.
  +natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
Decidable (a.+1 = b.+1) destruct (IHa b).natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
p: a = b
Decidable (a.+1 = b.+1)
natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
n: a <> b
Decidable (a.+1 = b.+1)
    *natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
p: a = b
Decidable (a.+1 = b.+1) left.natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
p: a = b
a.+1 = b.+1 apply ap;trivial.
    *natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
n: a <> b
Decidable (a.+1 = b.+1) right;intros E.natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
n: a <> b
E: a.+1 = b.+1
Empty apply (injective S) in E.natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall y : nat, Decidable (a = y)
b: nat
n: a <> b
E: a = b
Empty auto.
Defined.

Global Instance nat_set : IsTrunc@{N} 0 nat.natpaths:= paths: nat -> nat -> Type
IsHSet nat
Proof.natpaths:= paths: nat -> nat -> Type
IsHSet nat
apply hset_pathcoll, pathcoll_decpaths, nat_dec.
Qed.

Instance nat_semiring : IsSemiCRing@{N} nat.natpaths:= paths: nat -> nat -> Type
IsSemiCRing nat
Proof.natpaths:= paths: nat -> nat -> Type
IsSemiCRing nat
  repeat (split; try exact _).
Qed.

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

(* Close Scope nat_scope. *)

Lemma O_nat_0 : O =N= 0.natpaths:= paths: nat -> nat -> Type
0 =N= 0
Proof.natpaths:= paths: nat -> nat -> Type
0 =N= 0 reflexivity. Qed.

Lemma S_nat_plus_1 x : S x =N= x + 1.natpaths:= paths: nat -> nat -> Type
x: nat
x.+1 =N= x + 1
Proof.natpaths:= paths: nat -> nat -> Type
x: nat
x.+1 =N= x + 1
rewrite add_comm.natpaths:= paths: nat -> nat -> Type
x: nat
x.+1 =N= 1 + x reflexivity.
Qed.

Lemma S_nat_1_plus x : S x =N= 1 + x.natpaths:= paths: nat -> nat -> Type
x: nat
x.+1 =N= 1 + x
Proof.natpaths:= paths: nat -> nat -> Type
x: nat
x.+1 =N= 1 + x reflexivity. Qed.

Lemma nat_induction (P : nat -> Type) :
  P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P n.natpaths:= paths: nat -> nat -> Type
P: nat -> Type
P 0 ->
(forall n : nat, P n -> P (1 + n)) ->
forall n : nat, P n
Proof.natpaths:= paths: nat -> nat -> Type
P: nat -> Type
P 0 ->
(forall n : nat, P n -> P (1 + n)) ->
forall n : nat, P n apply nat_rect. Qed.

Lemma plus_eq_zero : forall a b : nat, a + b =N= 0 -> a =N= 0 /\ b =N= 0.natpaths:= paths: nat -> nat -> Type
forall a b : nat,
a + b =N= 0 -> ((a =N= 0) * (b =N= 0))%type
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat,
a + b =N= 0 -> ((a =N= 0) * (b =N= 0))%type
intros [|a];[intros [|b];auto|].natpaths:= paths: nat -> nat -> Type
b: nat
0 + b.+1 =N= 0 -> ((0 =N= 0) * (b.+1 =N= 0))%type
natpaths:= paths: nat -> nat -> Type
a: nat
forall b : nat,
a.+1 + b =N= 0 -> ((a.+1 =N= 0) * (b =N= 0))%type
-natpaths:= paths: nat -> nat -> Type
b: nat
0 + b.+1 =N= 0 -> ((0 =N= 0) * (b.+1 =N= 0))%type intros E.natpaths:= paths: nat -> nat -> Type
b: nat
E: 0 + b.+1 =N= 0
((0 =N= 0) * (b.+1 =N= 0))%type destruct (S_neq_0 _ E).
-natpaths:= paths: nat -> nat -> Type
a: nat
forall b : nat,
a.+1 + b =N= 0 -> ((a.+1 =N= 0) * (b =N= 0))%type intros ? E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a.+1 + b =N= 0
((a.+1 =N= 0) * (b =N= 0))%type destruct (S_neq_0 _ E).
Qed.

Lemma mult_eq_zero : forall a b : nat, a * b =N= 0 -> a =N= 0 |_| b =N= 0.natpaths:= paths: nat -> nat -> Type
forall a b : nat,
a * b =N= 0 -> ((a =N= 0) + (b =N= 0))%type
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat,
a * b =N= 0 -> ((a =N= 0) + (b =N= 0))%type
intros [|a] [|b];auto.natpaths:= paths: nat -> nat -> Type
a: nat
a.+1 * 0 =N= 0 -> ((a.+1 =N= 0) + (0 =N= 0))%type
natpaths:= paths: nat -> nat -> Type
a, b: nat
a.+1 * b.+1 =N= 0 ->
((a.+1 =N= 0) + (b.+1 =N= 0))%type
-natpaths:= paths: nat -> nat -> Type
a: nat
a.+1 * 0 =N= 0 -> ((a.+1 =N= 0) + (0 =N= 0))%type intros _;right;reflexivity.
-natpaths:= paths: nat -> nat -> Type
a, b: nat
a.+1 * b.+1 =N= 0 ->
((a.+1 =N= 0) + (b.+1 =N= 0))%type simpl_nat.natpaths:= paths: nat -> nat -> Type
a, b: nat
(b + a * b.+1).+1 =N= 0 ->
((a.+1 =N= 0) + (b.+1 =N= 0))%type
  intros E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: (b + a * b.+1).+1 =N= 0
((a.+1 =N= 0) + (b.+1 =N= 0))%type
  destruct (S_neq_0 _ E).
Defined.

Instance nat_zero_divisors : NoZeroDivisors nat.natpaths:= paths: nat -> nat -> Type
NoZeroDivisors nat
Proof.natpaths:= paths: nat -> nat -> Type
NoZeroDivisors nat
intros x [Ex [y [Ey1 Ey2]]].natpaths:= paths: nat -> nat -> Type
x: nat
Ex: x <> 0
y: nat
Ey1: y <> 0
Ey2: x * y = 0
Empty
apply mult_eq_zero in Ey2.natpaths:= paths: nat -> nat -> Type
x: nat
Ex: x <> 0
y: nat
Ey1: y <> 0
Ey2: ((x =N= 0) + (y =N= 0))%type
Empty
destruct Ey2;auto.
Qed.

Instance nat_plus_cancel_l : forall z:nat, LeftCancellation@{N} plus z.natpaths:= paths: nat -> nat -> Type
forall z : nat, LeftCancellation plus z
Proof.natpaths:= paths: nat -> nat -> Type
forall z : nat, LeftCancellation plus z
red.natpaths:= paths: nat -> nat -> Type
forall z x y : nat, z + x = z + y -> x = y intros a;induction a as [|a IHa];simpl_nat;intros b c E.natpaths:= paths: nat -> nat -> Type
b, c: nat
E: b = c
b = c
natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall x y : nat, a + x = a + y -> x = y
b, c: nat
E: (a + b).+1 = (a + c).+1
b = c
-natpaths:= paths: nat -> nat -> Type
b, c: nat
E: b = c
b = c trivial.
-natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall x y : nat, a + x = a + y -> x = y
b, c: nat
E: (a + b).+1 = (a + c).+1
b = c apply IHa.natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall x y : nat, a + x = a + y -> x = y
b, c: nat
E: (a + b).+1 = (a + c).+1
a + b = a + c apply (injective S).natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall x y : nat, a + x = a + y -> x = y
b, c: nat
E: (a + b).+1 = (a + c).+1
(a + b).+1 = (a + c).+1 assumption.
Qed.

Instance nat_mult_cancel_l
  : forall z : nat, PropHolds (~ (z =N= 0)) -> LeftCancellation@{N} (.*.) z.natpaths:= paths: nat -> nat -> Type
forall z : nat,
PropHolds (~ (z =N= 0)) -> LeftCancellation mult z
Proof.natpaths:= paths: nat -> nat -> Type
forall z : nat,
PropHolds (~ (z =N= 0)) -> LeftCancellation mult z
unfold PropHolds.natpaths:= paths: nat -> nat -> Type
forall z : nat, ~ (z =N= 0) -> LeftCancellation mult z unfold LeftCancellation.natpaths:= paths: nat -> nat -> Type
forall z : nat,
~ (z =N= 0) ->
forall x y : nat, z * x = z * y -> x = y
intros a Ea b c E;revert b c a Ea E.natpaths:= paths: nat -> nat -> Type
forall b c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
induction b as [|b IHb];intros [|c];simpl_nat;intros a Ea E.natpaths:= paths: nat -> nat -> Type
a: nat
Ea: ~ (a =N= 0)
E: a * 0 = a * 0
0 = 0
natpaths:= paths: nat -> nat -> Type
c, a: nat
Ea: ~ (a =N= 0)
E: a * 0 = a * c.+1
0 = c.+1
natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
a: nat
Ea: ~ (a =N= 0)
E: a * b.+1 = a * 0
b.+1 = 0
natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
c, a: nat
Ea: ~ (a =N= 0)
E: a * b.+1 = a * c.+1
b.+1 = c.+1
-natpaths:= paths: nat -> nat -> Type
a: nat
Ea: ~ (a =N= 0)
E: a * 0 = a * 0
0 = 0 reflexivity.
-natpaths:= paths: nat -> nat -> Type
c, a: nat
Ea: ~ (a =N= 0)
E: a * 0 = a * c.+1
0 = c.+1 rewrite mul_0_r in E.natpaths:= paths: nat -> nat -> Type
c, a: nat
Ea: ~ (a =N= 0)
E: 0 = a * c.+1
0 = c.+1
  rewrite mul_S_r in E;apply symmetry in E.natpaths:= paths: nat -> nat -> Type
c, a: nat
Ea: ~ (a =N= 0)
E: a + a * c = 0
0 = c.+1
  apply plus_eq_zero in E.natpaths:= paths: nat -> nat -> Type
c, a: nat
Ea: ~ (a =N= 0)
E: ((a =N= 0) * ((a * c)%mc =N= 0))%type
0 = c.+1 destruct (Ea (fst E)).
-natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
a: nat
Ea: ~ (a =N= 0)
E: a * b.+1 = a * 0
b.+1 = 0 rewrite mul_0_r,mul_S_r in E.natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
a: nat
Ea: ~ (a =N= 0)
E: a + a * b = 0
b.+1 = 0 apply plus_eq_zero in E.natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
a: nat
Ea: ~ (a =N= 0)
E: ((a =N= 0) * ((a * b)%mc =N= 0))%type
b.+1 = 0
  destruct (Ea (fst E)).
-natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
c, a: nat
Ea: ~ (a =N= 0)
E: a * b.+1 = a * c.+1
b.+1 = c.+1 rewrite 2!mul_S_r in E.natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
c, a: nat
Ea: ~ (a =N= 0)
E: a + a * b = a + a * c
b.+1 = c.+1
  apply (left_cancellation _ _) in E.natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
c, a: nat
Ea: ~ (a =N= 0)
E: a * b = a * c
b.+1 = c.+1
  apply ap.natpaths:= paths: nat -> nat -> Type
b: nat
IHb: forall c a : nat,
~ (a =N= 0) -> a * b = a * c -> b = c
c, a: nat
Ea: ~ (a =N= 0)
E: a * b = a * c
b = c apply IHb with a;trivial.
Qed.

(* Order *)
Global Instance nat_le: Le@{N N} nat := Nat.Core.leq.
Global Instance nat_lt: Lt@{N N} nat := Nat.Core.lt.

Lemma le_plus : forall n k, n <= k + n.natpaths:= paths: nat -> nat -> Type
forall n k : nat, n ≤ k + n
Proof.natpaths:= paths: nat -> nat -> Type
forall n k : nat, n ≤ k + n
induction k.natpaths:= paths: nat -> nat -> Type
n: nat
n ≤ 0 + n
natpaths:= paths: nat -> nat -> Type
n, k: nat
IHk: n ≤ k + n
n ≤ k.+1 + n
-natpaths:= paths: nat -> nat -> Type
n: nat
n ≤ 0 + n apply Nat.Core.leq_n.
-natpaths:= paths: nat -> nat -> Type
n, k: nat
IHk: n ≤ k + n
n ≤ k.+1 + n simpl_nat.natpaths:= paths: nat -> nat -> Type
n, k: nat
IHk: n ≤ k + n
n ≤ (k + n).+1 constructor.natpaths:= paths: nat -> nat -> Type
n, k: nat
IHk: n ≤ k + n
Core.leq n (k + n) assumption.
Qed.

Lemma le_exists : forall n m : nat,
  iff@{N N N} (n <= m) (sig@{N N} (fun k => m =N= k + n)).natpaths:= paths: nat -> nat -> Type
forall n m : nat, n ≤ m <-> {k : nat & m =N= k + n}
Proof.natpaths:= paths: nat -> nat -> Type
forall n m : nat, n ≤ m <-> {k : nat & m =N= k + n}
intros n m;split.natpaths:= paths: nat -> nat -> Type
n, m: nat
n ≤ m -> {k : nat & m =N= k + n}
natpaths:= paths: nat -> nat -> Type
n, m: nat
{k : nat & m =N= k + n} -> n ≤ m
-natpaths:= paths: nat -> nat -> Type
n, m: nat
n ≤ m -> {k : nat & m =N= k + n} intros E;induction E as [|m E IH].natpaths:= paths: nat -> nat -> Type
n: nat
{k : nat & n =N= k + n}
natpaths:= paths: nat -> nat -> Type
n, m: nat
E: Core.leq n m
IH: {k : nat & m =N= k + n}
{k : nat & m.+1 =N= k + n}
  +natpaths:= paths: nat -> nat -> Type
n: nat
{k : nat & n =N= k + n} exists 0;split.
  +natpaths:= paths: nat -> nat -> Type
n, m: nat
E: Core.leq n m
IH: {k : nat & m =N= k + n}
{k : nat & m.+1 =N= k + n} destruct IH as [k IH].natpaths:= paths: nat -> nat -> Type
n, m: nat
E: Core.leq n m
k: nat
IH: m =N= k + n
{k : nat & m.+1 =N= k + n}
    exists (S k).natpaths:= paths: nat -> nat -> Type
n, m: nat
E: Core.leq n m
k: nat
IH: m =N= k + n
m.+1 =N= k.+1 + n rewrite IH;reflexivity.
-natpaths:= paths: nat -> nat -> Type
n, m: nat
{k : nat & m =N= k + n} -> n ≤ m intros [k Hk].natpaths:= paths: nat -> nat -> Type
n, m, k: nat
Hk: m =N= k + n
n ≤ m
  rewrite Hk.natpaths:= paths: nat -> nat -> Type
n, m, k: nat
Hk: m =N= k + n
n ≤ k + n apply le_plus.
Qed.

Lemma zero_least : forall a, 0 <= a.natpaths:= paths: nat -> nat -> Type
forall a : nat, 0 ≤ a
Proof.natpaths:= paths: nat -> nat -> Type
forall a : nat, 0 ≤ a
induction a;constructor;auto.
Qed.

Lemma le_S_S : forall a b : nat, iff@{N N N} (a <= b) (S a <= S b).natpaths:= paths: nat -> nat -> Type
forall a b : nat, a ≤ b <-> a.+1 ≤ b.+1
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a ≤ b <-> a.+1 ≤ b.+1
intros.natpaths:= paths: nat -> nat -> Type
a, b: nat
a ≤ b <-> a.+1 ≤ b.+1 etransitivity;[apply le_exists|].natpaths:= paths: nat -> nat -> Type
a, b: nat
{k : nat & b =N= k + a} <-> a.+1 ≤ b.+1
etransitivity;[|apply symmetry,le_exists].natpaths:= paths: nat -> nat -> Type
a, b: nat
{k : nat & b =N= k + a} <->
{k : nat & b.+1 =N= k + a.+1}
split;intros [k E];exists k.natpaths:= paths: nat -> nat -> Type
a, b, k: nat
E: b =N= k + a
b.+1 =N= k + a.+1
natpaths:= paths: nat -> nat -> Type
a, b, k: nat
E: b.+1 =N= k + a.+1
b =N= k + a
-natpaths:= paths: nat -> nat -> Type
a, b, k: nat
E: b =N= k + a
b.+1 =N= k + a.+1 rewrite E,add_S_r.natpaths:= paths: nat -> nat -> Type
a, b, k: nat
E: b =N= k + a
(k + a).+1 =N= (k + a).+1 reflexivity.
-natpaths:= paths: nat -> nat -> Type
a, b, k: nat
E: b.+1 =N= k + a.+1
b =N= k + a rewrite add_S_r in E;apply (injective _) in E.natpaths:= paths: nat -> nat -> Type
a, b, k: nat
E: b = k + a
b =N= k + a trivial.
Qed.

Lemma lt_0_S : forall a : nat, 0 < S a.natpaths:= paths: nat -> nat -> Type
forall a : nat, 0 < a.+1
Proof.natpaths:= paths: nat -> nat -> Type
forall a : nat, 0 < a.+1
intros.natpaths:= paths: nat -> nat -> Type
a: nat
0 < a.+1 apply le_S_S.natpaths:= paths: nat -> nat -> Type
a: nat
0 ≤ a apply zero_least.
Qed.

Lemma le_S_either : forall a b, a <= S b -> a <= b |_| a = S b.natpaths:= paths: nat -> nat -> Type
forall a b : nat,
a ≤ b.+1 -> ((a ≤ b) + (a = b.+1))%type
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat,
a ≤ b.+1 -> ((a ≤ b) + (a = b.+1))%type
intros [|a] b.natpaths:= paths: nat -> nat -> Type
b: nat
0 ≤ b.+1 -> ((0 ≤ b) + (0 = b.+1))%type
natpaths:= paths: nat -> nat -> Type
a, b: nat
a.+1 ≤ b.+1 -> ((a.+1 ≤ b) + (a.+1 = b.+1))%type
-natpaths:= paths: nat -> nat -> Type
b: nat
0 ≤ b.+1 -> ((0 ≤ b) + (0 = b.+1))%type intros;left;apply zero_least.
-natpaths:= paths: nat -> nat -> Type
a, b: nat
a.+1 ≤ b.+1 -> ((a.+1 ≤ b) + (a.+1 = b.+1))%type intros E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a.+1 ≤ b.+1
((a.+1 ≤ b) + (a.+1 = b.+1))%type apply (snd (le_S_S _ _)) in E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a ≤ b
((a.+1 ≤ b) + (a.+1 = b.+1))%type destruct E as [|b E];auto.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: Core.leq a b
((a.+1 ≤ b.+1) + (a.+1 = b.+2))%type
  left.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: Core.leq a b
a.+1 ≤ b.+1 apply le_S_S.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: Core.leq a b
a ≤ b trivial.
Defined.

Lemma le_lt_dec : forall a b : nat, a <= b |_| b < a.natpaths:= paths: nat -> nat -> Type
forall a b : nat, ((a ≤ b) + (b < a))%type
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat, ((a ≤ b) + (b < a))%type
induction a as [|a IHa].natpaths:= paths: nat -> nat -> Type
forall b : nat, ((0 ≤ b) + (b < 0))%type
natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
forall b : nat, ((a.+1 ≤ b) + (b < a.+1))%type
-natpaths:= paths: nat -> nat -> Type
forall b : nat, ((0 ≤ b) + (b < 0))%type intros;left;apply zero_least.
-natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
forall b : nat, ((a.+1 ≤ b) + (b < a.+1))%type intros [|b].natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
((a.+1 ≤ 0) + (0 < a.+1))%type
natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
((a.+1 ≤ b.+1) + (b.+1 < a.+1))%type
  +natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
((a.+1 ≤ 0) + (0 < a.+1))%type right.natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
0 < a.+1 apply lt_0_S.
  +natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
((a.+1 ≤ b.+1) + (b.+1 < a.+1))%type destruct (IHa b).natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
l: a ≤ b
((a.+1 ≤ b.+1) + (b.+1 < a.+1))%type
natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
l: b < a
((a.+1 ≤ b.+1) + (b.+1 < a.+1))%type
    *natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
l: a ≤ b
((a.+1 ≤ b.+1) + (b.+1 < a.+1))%type left.natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
l: a ≤ b
a.+1 ≤ b.+1 apply le_S_S;trivial.
    *natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
l: b < a
((a.+1 ≤ b.+1) + (b.+1 < a.+1))%type right.natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
l: b < a
b.+1 < a.+1 apply le_S_S.natpaths:= paths: nat -> nat -> Type
a: nat
IHa: forall b : nat, ((a ≤ b) + (b < a))%type
b: nat
l: b < a
b.+1 ≤ a trivial.
Defined.

Lemma not_lt_0 : forall a, ~ (a < 0).natpaths:= paths: nat -> nat -> Type
forall a : nat, ~ (a < 0)
Proof.natpaths:= paths: nat -> nat -> Type
forall a : nat, ~ (a < 0)
intros a E.natpaths:= paths: nat -> nat -> Type
a: nat
E: a < 0
Empty apply le_exists in E.natpaths:= paths: nat -> nat -> Type
a: nat
E: {k : nat & 0 =N= k + a.+1}
Empty
destruct E as [k E].natpaths:= paths: nat -> nat -> Type
a, k: nat
E: 0 =N= k + a.+1
Empty
apply natpaths_symm,plus_eq_zero in E.natpaths:= paths: nat -> nat -> Type
a, k: nat
E: ((k =N= 0) * (a.+1 =N= 0))%type
Empty
apply (S_neq_0 _ (snd E)).
Qed.

Lemma lt_le : forall a b, a < b -> a <= b.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a < b -> a ≤ b
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a < b -> a ≤ b
intros.natpaths:= paths: nat -> nat -> Type
a, b: nat
X: a < b
a ≤ b
destruct b.natpaths:= paths: nat -> nat -> Type
a: nat
X: a < 0
a ≤ 0
natpaths:= paths: nat -> nat -> Type
a, b: nat
X: a < b.+1
a ≤ b.+1
-natpaths:= paths: nat -> nat -> Type
a: nat
X: a < 0
a ≤ 0 destruct (not_lt_0 a).natpaths:= paths: nat -> nat -> Type
a: nat
X: a < 0
a < 0 trivial.
-natpaths:= paths: nat -> nat -> Type
a, b: nat
X: a < b.+1
a ≤ b.+1 constructor.natpaths:= paths: nat -> nat -> Type
a, b: nat
X: a < b.+1
Core.leq a b apply le_S_S.natpaths:= paths: nat -> nat -> Type
a, b: nat
X: a < b.+1
a.+1 ≤ b.+1 trivial.
Qed.

Local Instance nat_le_total : TotalRelation@{N N} (_:Le nat).natpaths:= paths: nat -> nat -> Type
TotalRelation (nat_le : Le nat)
Proof.natpaths:= paths: nat -> nat -> Type
TotalRelation (nat_le : Le nat)
hnf.natpaths:= paths: nat -> nat -> Type
forall x y : nat, (nat_le x y + nat_le y x)%type intros a b.natpaths:= paths: nat -> nat -> Type
a, b: nat
(nat_le a b + nat_le b a)%type
destruct (le_lt_dec a b);[left|right].natpaths:= paths: nat -> nat -> Type
a, b: nat
l: a ≤ b
nat_le a b
natpaths:= paths: nat -> nat -> Type
a, b: nat
l: b < a
nat_le b a
-natpaths:= paths: nat -> nat -> Type
a, b: nat
l: a ≤ b
nat_le a b trivial.
-natpaths:= paths: nat -> nat -> Type
a, b: nat
l: b < a
nat_le b a apply lt_le;trivial.
Qed.

Local Instance nat_lt_irrefl : Irreflexive@{N N} (_:Lt nat).natpaths:= paths: nat -> nat -> Type
Irreflexive (nat_lt : Lt nat)
Proof.natpaths:= paths: nat -> nat -> Type
Irreflexive (nat_lt : Lt nat)
hnf.natpaths:= paths: nat -> nat -> Type
forall x : nat, complement nat_lt x x intros x E.natpaths:= paths: nat -> nat -> Type
x: nat
E: nat_lt x x
Empty
apply le_exists in E.natpaths:= paths: nat -> nat -> Type
x: nat
E: {k : nat & x =N= k + x.+1}
Empty
destruct E as [k E].natpaths:= paths: nat -> nat -> Type
x, k: nat
E: x =N= k + x.+1
Empty
apply (S_neq_0 k).natpaths:= paths: nat -> nat -> Type
x, k: nat
E: x =N= k + x.+1
k.+1 =N= 0
apply (left_cancellation@{N} (+) x).natpaths:= paths: nat -> nat -> Type
x, k: nat
E: x =N= k + x.+1
x + k.+1 = x + 0
fold natpaths.natpaths:= paths: nat -> nat -> Type
x, k: nat
E: x =N= k + x.+1
x + k.+1 =N= x + 0
rewrite add_0_r, add_S_r,<-add_S_l.natpaths:= paths: nat -> nat -> Type
x, k: nat
E: x =N= k + x.+1
x.+1 + k =N= x
rewrite add_comm.natpaths:= paths: nat -> nat -> Type
x, k: nat
E: x =N= k + x.+1
k + x.+1 =N= x apply natpaths_symm,E.
Qed.

Local Instance nat_le_hprop : is_mere_relation nat le.natpaths:= paths: nat -> nat -> Type
is_mere_relation nat le
Proof.natpaths:= paths: nat -> nat -> Type
is_mere_relation nat le
intros m n;apply Trunc.hprop_allpath.natpaths:= paths: nat -> nat -> Type
m, n: nat
forall x y : m ≤ n, x = y
generalize (idpath (S n) : S n =N= S n).natpaths:= paths: nat -> nat -> Type
m, n: nat
n.+1 =N= n.+1 -> forall x y : m ≤ n, x = y
generalize n at 2 3 4 5.natpaths:= paths: nat -> nat -> Type
m, n: nat
forall n0 : nat,
n.+1 =N= n0.+1 -> forall x y : m ≤ n0, x = y
change (forall n0 : nat,
S n =N= S n0 -> forall le_mn1 le_mn2 : m <= n0, le_mn1 = le_mn2).natpaths:= paths: nat -> nat -> Type
m, n: nat
forall n0 : nat,
n.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
induction (S n) as [|n0 IHn0].natpaths:= paths: nat -> nat -> Type
m, n: nat
forall n0 : nat,
0 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
natpaths:= paths: nat -> nat -> Type
m, n, n0: nat
IHn0: forall n1 : nat,
n0 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
forall n1 : nat,
n0.+1 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
-natpaths:= paths: nat -> nat -> Type
m, n: nat
forall n0 : nat,
0 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2 intros ? E;destruct (S_neq_0 _ (natpaths_symm _ _ E)).
-natpaths:= paths: nat -> nat -> Type
m, n, n0: nat
IHn0: forall n1 : nat,
n0 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
forall n1 : nat,
n0.+1 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2 clear n; intros n H.natpaths:= paths: nat -> nat -> Type
m, n0: nat
IHn0: forall n1 : nat,
n0 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
n: nat
H: n0.+1 =N= n.+1
forall le_mn1 le_mn2 : m ≤ n, le_mn1 = le_mn2
  apply (injective S) in H.natpaths:= paths: nat -> nat -> Type
m, n0: nat
IHn0: forall n1 : nat,
n0 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
n: nat
H: n0 = n
forall le_mn1 le_mn2 : m ≤ n, le_mn1 = le_mn2
  rewrite <- H; intros le_mn1 le_mn2; clear n H.natpaths:= paths: nat -> nat -> Type
m, n0: nat
IHn0: forall n1 : nat,
n0 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
le_mn1, le_mn2: m ≤ n0
le_mn1 = le_mn2
  pose (def_n2 := idpath n0);
  path_via (paths_ind n0 (fun n _ => le m _) le_mn2 n0 def_n2).natpaths:= paths: nat -> nat -> Type
m, n0: nat
IHn0: forall n1 : nat,
n0 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
le_mn1, le_mn2: m ≤ n0
def_n2:= 1%path: n0 = n0
le_mn1 =
paths_ind n0 (fun (n : nat) (_ : n0 = n) => m ≤ n)
  le_mn2 n0 def_n2
  generalize def_n2; revert le_mn1 le_mn2.natpaths:= paths: nat -> nat -> Type
m, n0: nat
IHn0: forall n1 : nat,
n0 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
def_n2:= 1%path: n0 = n0
forall (le_mn1 le_mn2 : m ≤ n0) (def_n2 : n0 = n0),
le_mn1 =
paths_ind n0 (fun (n : nat) (_ : n0 = n) => m ≤ n)
  le_mn2 n0 def_n2
  generalize n0 at 1 4 5 8; intros n1 le_mn1.natpaths:= paths: nat -> nat -> Type
m, n0: nat
IHn0: forall n1 : nat,
n0 =N= n1.+1 ->
forall le_mn1 le_mn2 : m ≤ n1, le_mn1 = le_mn2
def_n2:= 1%path: n0 = n0
n1: nat
le_mn1: m ≤ n1
forall (le_mn2 : m ≤ n0) (def_n2 : n0 = n1),
le_mn1 =
paths_ind n0 (fun (n : nat) (_ : n0 = n) => m ≤ n)
  le_mn2 n1 def_n2
  destruct le_mn1; intros le_mn2; destruct le_mn2.natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
forall def_n2 : m = m,
Core.leq_n m =
paths_ind m (fun (n : nat) (_ : m = n) => m ≤ n)
  (Core.leq_n m) m def_n2
natpaths:= paths: nat -> nat -> Type
m, m0: nat
IHn0: forall n0 : nat,
m0.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m0.+1 = m0.+1
le_mn2: Core.leq m m0
forall def_n2 : m0.+1 = m,
Core.leq_n m =
paths_ind m0.+1
  (fun (n : nat) (_ : m0.+1 = n) => m ≤ n)
  (Core.leq_S m m0 le_mn2) m def_n2
natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
m0: nat
le_mn1: Core.leq m m0
forall def_n2 : m = m0.+1,
Core.leq_S m m0 le_mn1 =
paths_ind m (fun (n : nat) (_ : m = n) => m ≤ n)
  (Core.leq_n m) m0.+1 def_n2
natpaths:= paths: nat -> nat -> Type
m, m1: nat
IHn0: forall n0 : nat,
m1.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m1.+1 = m1.+1
m0: nat
le_mn1: Core.leq m m0
le_mn2: Core.leq m m1
forall def_n2 : m1.+1 = m0.+1,
Core.leq_S m m0 le_mn1 =
paths_ind m1.+1
  (fun (n : nat) (_ : m1.+1 = n) => m ≤ n)
  (Core.leq_S m m1 le_mn2) m0.+1 def_n2
  +natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
forall def_n2 : m = m,
Core.leq_n m =
paths_ind m (fun (n : nat) (_ : m = n) => m ≤ n)
  (Core.leq_n m) m def_n2 intros def_n0.natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
def_n0: m = m
Core.leq_n m =
paths_ind m (fun (n : nat) (_ : m = n) => m ≤ n)
  (Core.leq_n m) m def_n0
    rewrite (Trunc.path_ishprop def_n0 idpath).natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
def_n0: m = m
Core.leq_n m =
paths_ind m (fun (n : nat) (_ : m = n) => m ≤ n)
  (Core.leq_n m) m 1
    simpl.natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
def_n0: m = m
Core.leq_n m = Core.leq_n m reflexivity.
  +natpaths:= paths: nat -> nat -> Type
m, m0: nat
IHn0: forall n0 : nat,
m0.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m0.+1 = m0.+1
le_mn2: Core.leq m m0
forall def_n2 : m0.+1 = m,
Core.leq_n m =
paths_ind m0.+1
  (fun (n : nat) (_ : m0.+1 = n) => m ≤ n)
  (Core.leq_S m m0 le_mn2) m def_n2 intros def_n0; generalize le_mn2; rewrite <-def_n0; intros le_mn0.natpaths:= paths: nat -> nat -> Type
m, m0: nat
IHn0: forall n0 : nat,
m0.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m0.+1 = m0.+1
le_mn2: Core.leq m m0
def_n0: m0.+1 = m
le_mn0: Core.leq m0.+1 m0
Core.leq_n m0.+1 =
paths_ind m0.+1
  (fun (n : nat) (_ : m0.+1 = n) => m0.+1 ≤ n)
  (Core.leq_S m0.+1 m0 le_mn0) m0.+1 1
    destruct (irreflexivity nat_lt _ le_mn0).
  +natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
m0: nat
le_mn1: Core.leq m m0
forall def_n2 : m = m0.+1,
Core.leq_S m m0 le_mn1 =
paths_ind m (fun (n : nat) (_ : m = n) => m ≤ n)
  (Core.leq_n m) m0.+1 def_n2 intros def_n0.natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
m0: nat
le_mn1: Core.leq m m0
def_n0: m = m0.+1
Core.leq_S m m0 le_mn1 =
paths_ind m (fun (n : nat) (_ : m = n) => m ≤ n)
  (Core.leq_n m) m0.+1 def_n0
    destruct (irreflexivity nat_lt m0).natpaths:= paths: nat -> nat -> Type
m: nat
IHn0: forall n0 : nat,
m =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m = m
m0: nat
le_mn1: Core.leq m m0
def_n0: m = m0.+1
nat_lt m0 m0
    rewrite def_n0 in le_mn1;trivial.
  +natpaths:= paths: nat -> nat -> Type
m, m1: nat
IHn0: forall n0 : nat,
m1.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m1.+1 = m1.+1
m0: nat
le_mn1: Core.leq m m0
le_mn2: Core.leq m m1
forall def_n2 : m1.+1 = m0.+1,
Core.leq_S m m0 le_mn1 =
paths_ind m1.+1
  (fun (n : nat) (_ : m1.+1 = n) => m ≤ n)
  (Core.leq_S m m1 le_mn2) m0.+1 def_n2 intros def_n0.natpaths:= paths: nat -> nat -> Type
m, m1: nat
IHn0: forall n0 : nat,
m1.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m1.+1 = m1.+1
m0: nat
le_mn1: Core.leq m m0
le_mn2: Core.leq m m1
def_n0: m1.+1 = m0.+1
Core.leq_S m m0 le_mn1 =
paths_ind m1.+1
  (fun (n : nat) (_ : m1.+1 = n) => m ≤ n)
  (Core.leq_S m m1 le_mn2) m0.+1 def_n0 pose proof (injective S _ _ def_n0) as E.natpaths:= paths: nat -> nat -> Type
m, m1: nat
IHn0: forall n0 : nat,
m1.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m1.+1 = m1.+1
m0: nat
le_mn1: Core.leq m m0
le_mn2: Core.leq m m1
def_n0: m1.+1 = m0.+1
E: m1 = m0
Core.leq_S m m0 le_mn1 =
paths_ind m1.+1
  (fun (n : nat) (_ : m1.+1 = n) => m ≤ n)
  (Core.leq_S m m1 le_mn2) m0.+1 def_n0
    destruct E.natpaths:= paths: nat -> nat -> Type
m, m1: nat
IHn0: forall n0 : nat,
m1.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m1.+1 = m1.+1
le_mn1, le_mn2: Core.leq m m1
def_n0: m1.+1 = m1.+1
Core.leq_S m m1 le_mn1 =
paths_ind m1.+1
  (fun (n : nat) (_ : m1.+1 = n) => m ≤ n)
  (Core.leq_S m m1 le_mn2) m1.+1 def_n0
    rewrite (Trunc.path_ishprop def_n0 idpath).natpaths:= paths: nat -> nat -> Type
m, m1: nat
IHn0: forall n0 : nat,
m1.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m1.+1 = m1.+1
le_mn1, le_mn2: Core.leq m m1
def_n0: m1.+1 = m1.+1
Core.leq_S m m1 le_mn1 =
paths_ind m1.+1
  (fun (n : nat) (_ : m1.+1 = n) => m ≤ n)
  (Core.leq_S m m1 le_mn2) m1.+1 1 simpl.natpaths:= paths: nat -> nat -> Type
m, m1: nat
IHn0: forall n0 : nat,
m1.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m1.+1 = m1.+1
le_mn1, le_mn2: Core.leq m m1
def_n0: m1.+1 = m1.+1
Core.leq_S m m1 le_mn1 = Core.leq_S m m1 le_mn2
    apply ap.natpaths:= paths: nat -> nat -> Type
m, m1: nat
IHn0: forall n0 : nat,
m1.+1 =N= n0.+1 ->
forall le_mn1 le_mn2 : m ≤ n0, le_mn1 = le_mn2
def_n2:= 1%path: m1.+1 = m1.+1
le_mn1, le_mn2: Core.leq m m1
def_n0: m1.+1 = m1.+1
le_mn1 = le_mn2 apply IHn0;trivial.
Qed.

Local Instance nat_le_po : PartialOrder nat_le.natpaths:= paths: nat -> nat -> Type
PartialOrder nat_le
Proof.natpaths:= paths: nat -> nat -> Type
PartialOrder nat_le
repeat split.natpaths:= paths: nat -> nat -> Type
IsHSet nat
natpaths:= paths: nat -> nat -> Type
is_mere_relation nat nat_le
natpaths:= paths: nat -> nat -> Type
Reflexive le
natpaths:= paths: nat -> nat -> Type
Transitive le
natpaths:= paths: nat -> nat -> Type
AntiSymmetric le
-natpaths:= paths: nat -> nat -> Type
IsHSet nat apply _.
-natpaths:= paths: nat -> nat -> Type
is_mere_relation nat nat_le apply _.
-natpaths:= paths: nat -> nat -> Type
Reflexive le hnf;intros; constructor.
-natpaths:= paths: nat -> nat -> Type
Transitive le hnf.natpaths:= paths: nat -> nat -> Type
forall x y z : nat, x ≤ y -> y ≤ z -> x ≤ z intros a b c E1 E2.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
E1: a ≤ b
E2: b ≤ c
a ≤ c
  apply le_exists in E1;apply le_exists in E2.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
E1: {k : nat & b =N= k + a}
E2: {k : nat & c =N= k + b}
a ≤ c
  destruct E1 as [k1 E1], E2 as [k2 E2].natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a
k2: nat
E2: c =N= k2 + b
a ≤ c
  rewrite E2,E1,add_assoc.natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a
k2: nat
E2: c =N= k2 + b
a ≤ k2 + k1 + a apply le_plus.
-natpaths:= paths: nat -> nat -> Type
AntiSymmetric le hnf.natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≤ y -> y ≤ x -> x = y intros a b E1 E2.natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a ≤ b
E2: b ≤ a
a = b
  apply le_exists in E1;apply le_exists in E2.natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: {k : nat & b =N= k + a}
E2: {k : nat & a =N= k + b}
a = b
  destruct E1 as [k1 E1], E2 as [k2 E2].natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
a = b
  assert (k1 + k2 = 0) as E.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
k1 + k2 = 0
natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
E: k1 + k2 = 0
a = b
  +natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
k1 + k2 = 0 apply (left_cancellation (+) a).natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
a + (k1 + k2) = a + 0
    rewrite plus_0_r.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
a + (k1 + k2) = a
    path_via (k2 + b).natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
a + (k1 + k2) = k2 + b
    rewrite E1.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
a + (k1 + k2) = k2 + (k1 + a)
    rewrite (plus_comm a), (plus_assoc k2), (plus_comm k2).natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
k1 + k2 + a = k1 + k2 + a
    reflexivity.
  +natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
E: k1 + k2 = 0
a = b apply plus_eq_zero in E.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
E: ((k1 =N= 0) * (k2 =N= 0))%type
a = b destruct E as [Ek1 Ek2].natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= k2 + b
Ek1: k1 =N= 0
Ek2: k2 =N= 0
a = b
    rewrite Ek2,plus_0_l in E2.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a
k2: nat
E2: a =N= b
Ek1: k1 =N= 0
Ek2: k2 =N= 0
a = b
    trivial.
Qed.

Local Instance nat_strict : StrictOrder (_:Lt nat).natpaths:= paths: nat -> nat -> Type
StrictOrder (nat_lt : Lt nat)
Proof.natpaths:= paths: nat -> nat -> Type
StrictOrder (nat_lt : Lt nat)
split.natpaths:= paths: nat -> nat -> Type
is_mere_relation nat lt
natpaths:= paths: nat -> nat -> Type
Irreflexive lt
natpaths:= paths: nat -> nat -> Type
Transitive lt
-natpaths:= paths: nat -> nat -> Type
is_mere_relation nat lt cbv; exact _.
-natpaths:= paths: nat -> nat -> Type
Irreflexive lt apply _.
-natpaths:= paths: nat -> nat -> Type
Transitive lt hnf.natpaths:= paths: nat -> nat -> Type
forall x y z : nat, x < y -> y < z -> x < z intros a b c E1 E2.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
E1: a < b
E2: b < c
a < c
  apply le_exists;apply le_exists in E1;apply le_exists in E2.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
E1: {k : nat & b =N= k + a.+1}
E2: {k : nat & c =N= k + b.+1}
{k : nat & c =N= k + a.+1}
  destruct E1 as [k1 E1], E2 as [k2 E2].natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: c =N= k2 + b.+1
{k : nat & c =N= k + a.+1}
  exists (S (k1+k2)).natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: c =N= k2 + b.+1
c =N= (k1 + k2).+1 + a.+1
  rewrite E2,E1.natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: c =N= k2 + b.+1
k2 + (k1 + a.+1).+1 =N= (k1 + k2).+1 + a.+1
  rewrite !add_S_r,add_S_l.natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: c =N= k2 + b.+1
(k2 + (k1 + a)).+2 =N= (k1 + k2 + a).+2
  rewrite (add_assoc k2), (add_comm k2).natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: c =N= k2 + b.+1
(k1 + k2 + a).+2 =N= (k1 + k2 + a).+2
  reflexivity.
Qed.

Instance nat_trichotomy : Trichotomy@{N N i} (lt:Lt nat).natpaths:= paths: nat -> nat -> Type
Trichotomy (lt : Lt nat)
Proof.natpaths:= paths: nat -> nat -> Type
Trichotomy (lt : Lt nat)
hnf.natpaths:= paths: nat -> nat -> Type
forall x y : nat, ((x < y) + ((x = y) + (y < x)))%type fold natpaths.natpaths:= paths: nat -> nat -> Type
forall x y : nat,
((x < y) + ((x =N= y) + (y < x)))%type
intros a b.natpaths:= paths: nat -> nat -> Type
a, b: nat
((a < b) + ((a =N= b) + (b < a)))%type destruct (le_lt_dec a b) as [[|]|E];auto.natpaths:= paths: nat -> nat -> Type
a, b: nat
((a < a) + ((a =N= a) + (a < a)))%type
natpaths:= paths: nat -> nat -> Type
a, b, m: nat
l: Core.leq a m
((a < m.+1) + ((a =N= m.+1) + (m.+1 < a)))%type
-natpaths:= paths: nat -> nat -> Type
a, b: nat
((a < a) + ((a =N= a) + (a < a)))%type right;left;split.
-natpaths:= paths: nat -> nat -> Type
a, b, m: nat
l: Core.leq a m
((a < m.+1) + ((a =N= m.+1) + (m.+1 < a)))%type left.natpaths:= paths: nat -> nat -> Type
a, b, m: nat
l: Core.leq a m
a < m.+1 apply le_S_S.natpaths:= paths: nat -> nat -> Type
a, b, m: nat
l: Core.leq a m
a ≤ m trivial.
Qed.

Global Instance nat_apart : Apart@{N N} nat := fun n m => n < m |_| m < n.

Instance nat_apart_mere : is_mere_relation nat nat_apart.natpaths:= paths: nat -> nat -> Type
is_mere_relation nat nat_apart
Proof.natpaths:= paths: nat -> nat -> Type
is_mere_relation nat nat_apart
intros;apply ishprop_sum;try apply _.natpaths:= paths: nat -> nat -> Type
x, y: nat
x < y -> y < x -> Empty
intros E1 E2.natpaths:= paths: nat -> nat -> Type
x, y: nat
E1: x < y
E2: y < x
Empty apply (irreflexivity nat_lt x).natpaths:= paths: nat -> nat -> Type
x, y: nat
E1: x < y
E2: y < x
nat_lt x x
transitivity y;trivial.
Qed.

Instance decidable_nat_apart x y : Decidable (nat_apart x y).natpaths:= paths: nat -> nat -> Type
x, y: nat
Decidable (nat_apart x y)
Proof.natpaths:= paths: nat -> nat -> Type
x, y: nat
Decidable (nat_apart x y)
  rapply decidable_sum@{N N N}; apply Nat.Core.decidable_lt.
Defined.

Global Instance nat_trivial_apart : TrivialApart nat.natpaths:= paths: nat -> nat -> Type
TrivialApart nat
Proof.natpaths:= paths: nat -> nat -> Type
TrivialApart nat
split.natpaths:= paths: nat -> nat -> Type
is_mere_relation nat apart
natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≶ y <-> x <> y
-natpaths:= paths: nat -> nat -> Type
is_mere_relation nat apart apply _.
-natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≶ y <-> x <> y intros a b;split;intros E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a ≶ b
a <> b
natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a <> b
a ≶ b
  +natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a ≶ b
a <> b destruct E as [E|E];apply irrefl_neq in E;trivial.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: b <> a
a <> b
    apply symmetric_neq;trivial.
  +natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a <> b
a ≶ b hnf.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a <> b
((a < b) + (b < a))%type destruct (trichotomy _ a b) as [?|[?|?]];auto.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: a <> b
p: a = b
((a < b) + (b < a))%type
    destruct E;trivial.
Qed.

Lemma nat_not_lt_le : forall a b, ~ (a < b) -> b <= a.natpaths:= paths: nat -> nat -> Type
forall a b : nat, ~ (a < b) -> b ≤ a
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat, ~ (a < b) -> b ≤ a
intros ?? E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: ~ (a < b)
b ≤ a
destruct (le_lt_dec b a);auto.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: ~ (a < b)
l: a < b
b ≤ a
destruct E;auto.
Qed.

Lemma nat_lt_not_le : forall a b : nat, a < b -> ~ (b <= a).natpaths:= paths: nat -> nat -> Type
forall a b : nat, a < b -> ~ (b ≤ a)
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a < b -> ~ (b ≤ a)
intros a b E1 E2.natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
E2: b ≤ a
Empty
apply le_exists in E1;apply le_exists in E2.natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: {k : nat & b =N= k + a.+1}
E2: {k : nat & a =N= k + b}
Empty
destruct E1 as [k1 E1], E2 as [k2 E2].natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= k2 + b
Empty
apply (S_neq_0 (k1 + k2)).natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= k2 + b
(k1 + k2).+1 =N= 0
apply (left_cancellation (+) a).natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= k2 + b
a + (k1 + k2).+1 = a + 0
fold natpaths.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= k2 + b
a + (k1 + k2).+1 =N= a + 0 rewrite add_0_r.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= k2 + b
a + (k1 + k2).+1 =N= a
rewrite E1 in E2.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= k2 + (k1 + a.+1)
a + (k1 + k2).+1 =N= a
rewrite add_S_r;rewrite !add_S_r in E2.natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= (k2 + (k1 + a)).+1
(a + (k1 + k2)).+1 =N= a
rewrite (add_assoc a), (add_comm a), <-(add_assoc k1), (add_comm a).natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= (k2 + (k1 + a)).+1
(k1 + (k2 + a)).+1 =N= a
rewrite (add_assoc k1), (add_comm k1), <-(add_assoc k2).natpaths:= paths: nat -> nat -> Type
a, b, k1: nat
E1: b =N= k1 + a.+1
k2: nat
E2: a =N= (k2 + (k1 + a)).+1
(k2 + (k1 + a)).+1 =N= a
apply natpaths_symm,E2.
Qed.

Global Instance nat_le_dec: forall x y : nat, Decidable (x ≤ y).natpaths:= paths: nat -> nat -> Type
forall x y : nat, Decidable (x ≤ y)
Proof.natpaths:= paths: nat -> nat -> Type
forall x y : nat, Decidable (x ≤ y)
intros a b.natpaths:= paths: nat -> nat -> Type
a, b: nat
Decidable (a ≤ b) destruct (le_lt_dec a b).natpaths:= paths: nat -> nat -> Type
a, b: nat
l: a ≤ b
Decidable (a ≤ b)
natpaths:= paths: nat -> nat -> Type
a, b: nat
l: b < a
Decidable (a ≤ b)
-natpaths:= paths: nat -> nat -> Type
a, b: nat
l: a ≤ b
Decidable (a ≤ b) left;trivial.
-natpaths:= paths: nat -> nat -> Type
a, b: nat
l: b < a
Decidable (a ≤ b) right.natpaths:= paths: nat -> nat -> Type
a, b: nat
l: b < a
~ (a ≤ b) apply nat_lt_not_le.natpaths:= paths: nat -> nat -> Type
a, b: nat
l: b < a
b < a trivial.
Defined.

Lemma S_gt_0 : forall a, 0 < S a.natpaths:= paths: nat -> nat -> Type
forall a : nat, 0 < a.+1
Proof.natpaths:= paths: nat -> nat -> Type
forall a : nat, 0 < a.+1
intros;apply le_S_S,zero_least.
Qed.

Lemma nonzero_gt_0 : forall a, ~ (a =N= 0) -> 0 < a.natpaths:= paths: nat -> nat -> Type
forall a : nat, ~ (a =N= 0) -> 0 < a
Proof.natpaths:= paths: nat -> nat -> Type
forall a : nat, ~ (a =N= 0) -> 0 < a
intros [|a] E.natpaths:= paths: nat -> nat -> Type
E: ~ (0 =N= 0)
0 < 0
natpaths:= paths: nat -> nat -> Type
a: nat
E: ~ (a.+1 =N= 0)
0 < a.+1
-natpaths:= paths: nat -> nat -> Type
E: ~ (0 =N= 0)
0 < 0 destruct E;split.
-natpaths:= paths: nat -> nat -> Type
a: nat
E: ~ (a.+1 =N= 0)
0 < a.+1 apply S_gt_0.
Qed.

Lemma nat_le_lt_trans : forall a b c : nat, a <= b -> b < c -> a < c.natpaths:= paths: nat -> nat -> Type
forall a b c : nat, a ≤ b -> b < c -> a < c
Proof.natpaths:= paths: nat -> nat -> Type
forall a b c : nat, a ≤ b -> b < c -> a < c
intros a b c E1 E2.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
E1: a ≤ b
E2: b < c
a < c
apply le_exists in E1;apply le_exists in E2.natpaths:= paths: nat -> nat -> Type
a, b, c: nat
E1: {k : nat & b =N= k + a}
E2: {k : nat & c =N= k + b.+1}
a < c
destruct E1 as [k1 E1],E2 as [k2 E2];rewrite E2,E1.natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a
k2: nat
E2: c =N= k2 + b.+1
a < k2 + (k1 + a).+1
rewrite add_S_r,add_assoc.natpaths:= paths: nat -> nat -> Type
a, b, c, k1: nat
E1: b =N= k1 + a
k2: nat
E2: c =N= k2 + b.+1
a < (k2 + k1 + a).+1 apply le_S_S,le_plus.
Qed.

Lemma lt_strong_cotrans : forall a b : nat, a < b -> forall c, a < c |_| c < b.natpaths:= paths: nat -> nat -> Type
forall a b : nat,
a < b -> forall c : nat, ((a < c) + (c < b))%type
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat,
a < b -> forall c : nat, ((a < c) + (c < b))%type
intros a b E1 c.natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
c: nat
((a < c) + (c < b))%type
destruct (le_lt_dec c a) as [E2|E2].natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
c: nat
E2: c ≤ a
((a < c) + (c < b))%type
natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
c: nat
E2: a < c
((a < c) + (c < b))%type
-natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
c: nat
E2: c ≤ a
((a < c) + (c < b))%type right.natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
c: nat
E2: c ≤ a
c < b apply nat_le_lt_trans with a;trivial.
-natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
c: nat
E2: a < c
((a < c) + (c < b))%type left;trivial.
Defined.

Lemma nat_full' : FullPseudoSemiRingOrder nat_le nat_lt.natpaths:= paths: nat -> nat -> Type
FullPseudoSemiRingOrder nat_le nat_lt
Proof.natpaths:= paths: nat -> nat -> Type
FullPseudoSemiRingOrder nat_le nat_lt
split;[apply _|split|].natpaths:= paths: nat -> nat -> Type
PseudoOrder nat_lt
natpaths:= paths: nat -> nat -> Type
forall x y : nat, ~ (y < x) -> {z : nat & y = x + z}
natpaths:= paths: nat -> nat -> Type
forall z : nat, StrictOrderEmbedding (plus z)
natpaths:= paths: nat -> nat -> Type
StrongBinaryExtensionality mult
natpaths:= paths: nat -> nat -> Type
forall x y : nat,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y)
natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≤ y <-> ~ (y < x)
-natpaths:= paths: nat -> nat -> Type
PseudoOrder nat_lt split;try apply _.natpaths:= paths: nat -> nat -> Type
forall x y : nat, ~ (x < y < x)
natpaths:= paths: nat -> nat -> Type
CoTransitive lt
natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≶ y <-> (x < y) + (y < x)
  +natpaths:= paths: nat -> nat -> Type
forall x y : nat, ~ (x < y < x) intros a b [E1 E2].natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
E2: b < a
Empty
    destruct (irreflexivity lt a).natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a < b
E2: b < a
a < a
    transitivity b;trivial.
  +natpaths:= paths: nat -> nat -> Type
CoTransitive lt hnf.natpaths:= paths: nat -> nat -> Type
forall x y : nat,
x < y -> forall z : nat, hor (x < z) (z < y)
    intros a b E c;apply tr;apply lt_strong_cotrans;trivial.
  +natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≶ y <-> (x < y) + (y < x) reflexivity.
-natpaths:= paths: nat -> nat -> Type
forall x y : nat, ~ (y < x) -> {z : nat & y = x + z} intros a b E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: ~ (b < a)
{z : nat & b = a + z} apply nat_not_lt_le,le_exists in E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: {k : nat & b =N= k + a}
{z : nat & b = a + z}
  destruct E as [k E];exists k;rewrite plus_comm;auto.
-natpaths:= paths: nat -> nat -> Type
forall z : nat, StrictOrderEmbedding (plus z) split.natpaths:= paths: nat -> nat -> Type
z: nat
StrictlyOrderPreserving (plus z)
natpaths:= paths: nat -> nat -> Type
z: nat
StrictlyOrderReflecting (plus z)
  +natpaths:= paths: nat -> nat -> Type
z: nat
StrictlyOrderPreserving (plus z) intros a b E.natpaths:= paths: nat -> nat -> Type
z, a, b: nat
E: a < b
z + a < z + b
    apply le_exists in E;destruct E as [k Hk].natpaths:= paths: nat -> nat -> Type
z, a, b, k: nat
Hk: b =N= k + a.+1
z + a < z + b
    rewrite Hk.natpaths:= paths: nat -> nat -> Type
z, a, b, k: nat
Hk: b =N= k + a.+1
z + a < z + (k + a.+1) rewrite add_S_r,<-add_S_l.natpaths:= paths: nat -> nat -> Type
z, a, b, k: nat
Hk: b =N= k + a.+1
z + a < z + (k.+1 + a)
    rewrite plus_assoc,(plus_comm z (S k)), <-plus_assoc.natpaths:= paths: nat -> nat -> Type
z, a, b, k: nat
Hk: b =N= k + a.+1
z + a < k.+1 + (z + a)
    apply le_S_S,le_plus.
  +natpaths:= paths: nat -> nat -> Type
z: nat
StrictlyOrderReflecting (plus z) intros a b E.natpaths:= paths: nat -> nat -> Type
z, a, b: nat
E: z + a < z + b
a < b
    apply le_exists in E;destruct E as [k E].natpaths:= paths: nat -> nat -> Type
z, a, b, k: nat
E: z + b =N= k + (z + a).+1
a < b
    rewrite <-add_S_r,plus_assoc,(plus_comm k z),<-plus_assoc in E.natpaths:= paths: nat -> nat -> Type
z, a, b, k: nat
E: z + b =N= z + (k + a.+1)
a < b
    apply (left_cancellation plus _) in E.natpaths:= paths: nat -> nat -> Type
z, a, b, k: nat
E: b = k + a.+1
a < b
    rewrite E;apply le_plus.
-natpaths:= paths: nat -> nat -> Type
StrongBinaryExtensionality mult intros ???? E.natpaths:= paths: nat -> nat -> Type
x₁, y₁, x₂, y₂: nat
E: x₁ * y₁ ≶ x₂ * y₂
hor (x₁ ≶ x₂) (y₁ ≶ y₂)
  apply trivial_apart in E.natpaths:= paths: nat -> nat -> Type
x₁, y₁, x₂, y₂: nat
E: x₁ * y₁ <> x₂ * y₂
hor (x₁ ≶ x₂) (y₁ ≶ y₂)
  destruct (dec (apart x₁ x₂)) as [?|ex];apply tr;auto.natpaths:= paths: nat -> nat -> Type
x₁, y₁, x₂, y₂: nat
E: x₁ * y₁ <> x₂ * y₂
ex: ~ (x₁ ≶ x₂)
((x₁ ≶ x₂) + (y₁ ≶ y₂))%type
  right.natpaths:= paths: nat -> nat -> Type
x₁, y₁, x₂, y₂: nat
E: x₁ * y₁ <> x₂ * y₂
ex: ~ (x₁ ≶ x₂)
y₁ ≶ y₂ apply tight_apart in ex.natpaths:= paths: nat -> nat -> Type
x₁, y₁, x₂, y₂: nat
E: x₁ * y₁ <> x₂ * y₂
ex: x₁ = x₂
y₁ ≶ y₂
  apply trivial_apart.natpaths:= paths: nat -> nat -> Type
x₁, y₁, x₂, y₂: nat
E: x₁ * y₁ <> x₂ * y₂
ex: x₁ = x₂
y₁ <> y₂ intros ey.natpaths:= paths: nat -> nat -> Type
x₁, y₁, x₂, y₂: nat
E: x₁ * y₁ <> x₂ * y₂
ex: x₁ = x₂
ey: y₁ = y₂
Empty
  apply E.natpaths:= paths: nat -> nat -> Type
x₁, y₁, x₂, y₂: nat
E: x₁ * y₁ <> x₂ * y₂
ex: x₁ = x₂
ey: y₁ = y₂
x₁ * y₁ = x₂ * y₂ apply ap011;trivial.
-natpaths:= paths: nat -> nat -> Type
forall x y : nat,
PropHolds (0 < x) ->
PropHolds (0 < y) -> PropHolds (0 < x * y) unfold PropHolds.natpaths:= paths: nat -> nat -> Type
forall x y : nat, 0 < x -> 0 < y -> 0 < x * y
  intros a b Ea Eb.natpaths:= paths: nat -> nat -> Type
a, b: nat
Ea: 0 < a
Eb: 0 < b
0 < a * b
  apply nonzero_gt_0.natpaths:= paths: nat -> nat -> Type
a, b: nat
Ea: 0 < a
Eb: 0 < b
~ (a * b =N= 0) intros E.natpaths:= paths: nat -> nat -> Type
a, b: nat
Ea: 0 < a
Eb: 0 < b
E: a * b =N= 0
Empty
  apply mult_eq_zero in E.natpaths:= paths: nat -> nat -> Type
a, b: nat
Ea: 0 < a
Eb: 0 < b
E: ((a =N= 0) + (b =N= 0))%type
Empty
  destruct E as [E|E];[rewrite E in Ea|rewrite E in Eb];
  apply (irreflexivity lt 0);trivial.
-natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≤ y <-> ~ (y < x) intros a b;split.natpaths:= paths: nat -> nat -> Type
a, b: nat
a ≤ b -> ~ (b < a)
natpaths:= paths: nat -> nat -> Type
a, b: nat
~ (b < a) -> a ≤ b
  +natpaths:= paths: nat -> nat -> Type
a, b: nat
a ≤ b -> ~ (b < a) intros E1 E2.natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a ≤ b
E2: b < a
Empty apply nat_lt_not_le in E2.natpaths:= paths: nat -> nat -> Type
a, b: nat
E1: a ≤ b
E2: ~ (a ≤ b)
Empty
    auto.
  +natpaths:= paths: nat -> nat -> Type
a, b: nat
~ (b < a) -> a ≤ b intros E.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: ~ (b < a)
a ≤ b
    destruct (le_lt_dec a b);auto.natpaths:= paths: nat -> nat -> Type
a, b: nat
E: ~ (b < a)
l: b < a
a ≤ b
    destruct E;auto.
Qed.

(* Coq pre 8.8 produces phantom universes, see GitHub Coq/Coq#1033. *)
Definition nat_full@{} := ltac:(first[exact nat_full'@{Ularge Ularge}|
                                      exact nat_full'@{Ularge Ularge N}|
                                      exact nat_full'@{}]).
Local Existing Instance nat_full.

Lemma le_nat_max_l n m : n <= Nat.Core.max n m.natpaths:= paths: nat -> nat -> Type
n, m: nat
n ≤ Core.max n m
Proof.natpaths:= paths: nat -> nat -> Type
n, m: nat
n ≤ Core.max n m
  revert m.natpaths:= paths: nat -> nat -> Type
n: nat
forall m : nat, n ≤ Core.max n m
  induction n as [|n' IHn];
  intros m; induction m as [|m' IHm]; try reflexivity; cbn.natpaths:= paths: nat -> nat -> Type
m': nat
IHm: 0 ≤ Core.max 0 m'
0 ≤ m'.+1
natpaths:= paths: nat -> nat -> Type
n': nat
IHn: forall m : nat, n' ≤ Core.max n' m
m': nat
IHm: n'.+1 ≤ Core.max n'.+1 m'
n'.+1 ≤ (Core.max n' m').+1
  -natpaths:= paths: nat -> nat -> Type
m': nat
IHm: 0 ≤ Core.max 0 m'
0 ≤ m'.+1 apply zero_least.
  -natpaths:= paths: nat -> nat -> Type
n': nat
IHn: forall m : nat, n' ≤ Core.max n' m
m': nat
IHm: n'.+1 ≤ Core.max n'.+1 m'
n'.+1 ≤ (Core.max n' m').+1 apply le_S_S.natpaths:= paths: nat -> nat -> Type
n': nat
IHn: forall m : nat, n' ≤ Core.max n' m
m': nat
IHm: n'.+1 ≤ Core.max n'.+1 m'
n' ≤ Core.max n' m' exact (IHn m').
Qed.
Lemma le_nat_max_r n m : m <= Nat.Core.max n m.natpaths:= paths: nat -> nat -> Type
n, m: nat
m ≤ Core.max n m
Proof.natpaths:= paths: nat -> nat -> Type
n, m: nat
m ≤ Core.max n m
  revert m.natpaths:= paths: nat -> nat -> Type
n: nat
forall m : nat, m ≤ Core.max n m
  induction n as [|n' IHn];
  intros m; induction m as [|m' IHm]; try reflexivity; cbn.natpaths:= paths: nat -> nat -> Type
n': nat
IHn: forall m : nat, m ≤ Core.max n' m
0 ≤ n'.+1
natpaths:= paths: nat -> nat -> Type
n': nat
IHn: forall m : nat, m ≤ Core.max n' m
m': nat
IHm: m' ≤ Core.max n'.+1 m'
m'.+1 ≤ (Core.max n' m').+1
  -natpaths:= paths: nat -> nat -> Type
n': nat
IHn: forall m : nat, m ≤ Core.max n' m
0 ≤ n'.+1 apply zero_least.
  -natpaths:= paths: nat -> nat -> Type
n': nat
IHn: forall m : nat, m ≤ Core.max n' m
m': nat
IHm: m' ≤ Core.max n'.+1 m'
m'.+1 ≤ (Core.max n' m').+1 apply le_S_S.natpaths:= paths: nat -> nat -> Type
n': nat
IHn: forall m : nat, m ≤ Core.max n' m
m': nat
IHm: m' ≤ Core.max n'.+1 m'
m' ≤ Core.max n' m' exact (IHn m').
Qed.
Instance S_embedding : OrderEmbedding S.natpaths:= paths: nat -> nat -> Type
OrderEmbedding S
Proof.natpaths:= paths: nat -> nat -> Type
OrderEmbedding S
split.natpaths:= paths: nat -> nat -> Type
OrderPreserving S
natpaths:= paths: nat -> nat -> Type
OrderReflecting S
-natpaths:= paths: nat -> nat -> Type
OrderPreserving S intros ??;apply le_S_S.
-natpaths:= paths: nat -> nat -> Type
OrderReflecting S intros ??;apply le_S_S.
Qed.

Global Instance S_strict_embedding : StrictOrderEmbedding S.natpaths:= paths: nat -> nat -> Type
StrictOrderEmbedding S
Proof.natpaths:= paths: nat -> nat -> Type
StrictOrderEmbedding S
split;apply _.
Qed.

Global Instance nat_naturals_to_semiring : NaturalsToSemiRing@{N i} nat :=
  fun _ _ _ _ _ _ => fix f (n: nat) := match n with 0%nat => 0 | 1%nat => 1 |
   S n' => 1 + f n' end.

Section for_another_semiring.
  Universe U.
  Context {R:Type@{U} } `{IsSemiCRing@{U} R}.

  Notation toR := (naturals_to_semiring nat R).

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

  Local Definition f_S : forall x, toR (S x) = 1 + toR x.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
forall x : nat, toR x.+1 = 1 + toR x
  Proof.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
forall x : nat, toR x.+1 = 1 + toR x
  intros [|x].natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
toR 1 = 1 + toR 0
natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x: nat
toR x.+2 = 1 + toR x.+1
  -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
toR 1 = 1 + toR 0 symmetry;apply plus_0_r.
  -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x: nat
toR x.+2 = 1 + toR x.+1 reflexivity.
  Defined.

  Local Definition f_preserves_plus a a': toR (a + a') = toR a + toR a'.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
toR (a + a') = toR a + toR a'
  Proof.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
toR (a + a') = toR a + toR a'
  induction a as [|a IHa].natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a': nat
toR (0 + a') = toR 0 + toR a'
natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a + a') = toR a + toR a'
toR (a.+1 + a') = toR a.+1 + toR a'
  -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a': nat
toR (0 + a') = toR 0 + toR a' change (toR a' = 0 + toR a').natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a': nat
toR a' = 0 + toR a'
    apply symmetry,plus_0_l.
  -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a + a') = toR a + toR a'
toR (a.+1 + a') = toR a.+1 + toR a' change (toR (S (a + a')) = toR (S a) + toR a').natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a + a') = toR a + toR a'
toR (a + a').+1 = toR a.+1 + toR a'
    rewrite !f_S,IHa.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a + a') = toR a + toR a'
1 + (toR a + toR a') = 1 + toR a + toR a'
    apply associativity.
  Qed.

  Local Definition f_preserves_mult a a': toR (a * a') = toR a * toR a'.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
toR (a * a') = toR a * toR a'
  Proof.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
toR (a * a') = toR a * toR a'
  induction a as [|a IHa].natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a': nat
toR (0 * a') = toR 0 * toR a'
natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a * a') = toR a * toR a'
toR (a.+1 * a') = toR a.+1 * toR a'
  -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a': nat
toR (0 * a') = toR 0 * toR a' change (0 = 0 * toR a').natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a': nat
0 = 0 * toR a'
    rewrite mult_0_l.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a': nat
0 = 0 reflexivity.
  -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a * a') = toR a * toR a'
toR (a.+1 * a') = toR a.+1 * toR a' rewrite f_S.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a * a') = toR a * toR a'
toR (a.+1 * a') = (1 + toR a) * toR a'
    change (toR (a' + a * a') = (1 + toR a) * toR a').natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a * a') = toR a * toR a'
toR (a' + a * a') = (1 + toR a) * toR a'
    rewrite f_preserves_plus, IHa.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a * a') = toR a * toR a'
toR a' + toR a * toR a' = (1 + toR a) * toR a'
    rewrite plus_mult_distr_r,mult_1_l.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': nat
IHa: toR (a * a') = toR a * toR a'
toR a' + toR a * toR a' = toR a' + toR a * toR a'
    reflexivity.
  Qed.

  Global Instance nat_to_sr_morphism
    : IsSemiRingPreserving (naturals_to_semiring nat R).natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiRingPreserving toR
  Proof.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiRingPreserving toR
    split; split.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiGroupPreserving toR
natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsUnitPreserving toR
natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiGroupPreserving toR
natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsUnitPreserving toR
    -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiGroupPreserving toR rapply f_preserves_plus.
    -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsUnitPreserving toR reflexivity.
    -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiGroupPreserving toR rapply f_preserves_mult.
    -natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsUnitPreserving toR reflexivity.
  Defined.

  Lemma toR_unique (h : nat -> R) `{!IsSemiRingPreserving h} x :
    naturals_to_semiring nat R x = h x.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
x: nat
toR x = h x
  Proof.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
x: nat
toR x = h x
  induction x as [|n E].natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
toR 0 = h 0
natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
E: toR n = h n
toR n.+1 = h n.+1
  +natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
toR 0 = h 0 change (0 = h 0).natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
0 = h 0
    apply symmetry,preserves_0.
  +natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
E: toR n = h n
toR n.+1 = h n.+1 rewrite f_S.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
E: toR n = h n
1 + toR n = h n.+1 change (1 + naturals_to_semiring nat R n = h (1+n)).natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
E: toR n = h n
1 + toR n = h (1 + n)
    rewrite (preserves_plus (f:=h)).natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
E: toR n = h n
1 + toR n = h 1 + h n
    rewrite E.natpaths:= paths: nat -> nat -> Type
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: nat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
E: toR n = h n
1 + h n = h 1 + h n apply ap10,ap,symmetry,preserves_1.
  Qed.
End for_another_semiring.

Lemma nat_naturals : Naturals@{N N N N N N N i} nat.natpaths:= paths: nat -> nat -> Type
Naturals nat
Proof.natpaths:= paths: nat -> nat -> Type
Naturals nat
split;try apply _.natpaths:= paths: nat -> nat -> Type
forall (B : Type) (Aplus0 : Plus B) (Amult0 : Mult B)
(Azero0 : Zero B) (Aone0 : One B) (H : IsSemiCRing B)
(h : nat -> B),
IsSemiRingPreserving h ->
forall x : nat, naturals_to_semiring nat B x = h x
intros;apply toR_unique, _.
Qed.
Global Existing Instance nat_naturals.

Global Instance nat_cut_minus: CutMinus@{N} nat := Nat.Core.sub.

Lemma plus_minus : forall a b, cut_minus (a + b) b =N= a.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a + b ∸ b =N= a
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a + b ∸ b =N= a
unfold cut_minus,nat_cut_minus.natpaths:= paths: nat -> nat -> Type
forall a b : nat, Core.sub (a + b) b =N= a
intros a b;revert a;induction b as [|b IH].natpaths:= paths: nat -> nat -> Type
forall a : nat, Core.sub (a + 0) 0 =N= a
natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
forall a : nat, Core.sub (a + b.+1) b.+1 =N= a
-natpaths:= paths: nat -> nat -> Type
forall a : nat, Core.sub (a + 0) 0 =N= a intros [|a];simpl;try split.natpaths:= paths: nat -> nat -> Type
a: nat
(nat_plus a 0).+1 =N= a.+1
  apply ap,add_0_r.
-natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
forall a : nat, Core.sub (a + b.+1) b.+1 =N= a intros [|a].natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
Core.sub (0 + b.+1) b.+1 =N= 0
natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
a: nat
Core.sub (a.+1 + b.+1) b.+1 =N= a.+1
  +natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
Core.sub (0 + b.+1) b.+1 =N= 0 simpl.natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
Core.sub b b =N= 0 pose proof (IH 0) as E.natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
E: Core.sub (0 + b) b =N= 0
Core.sub b b =N= 0
    rewrite add_0_l in E.natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
E: Core.sub b b =N= 0
Core.sub b b =N= 0 exact E.
  +natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
a: nat
Core.sub (a.+1 + b.+1) b.+1 =N= a.+1 simpl.natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
a: nat
Core.sub (nat_plus a b.+1) b =N= a.+1 change nat_plus with plus.natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, Core.sub (a + b) b =N= a
a: nat
Core.sub (a + b.+1) b =N= a.+1
    rewrite add_S_r,<-add_S_l;apply IH.
Qed.

Lemma le_plus_minus : forall n m : nat, n <= m -> m =N= (n + (cut_minus m  n)).natpaths:= paths: nat -> nat -> Type
forall n m : nat, n ≤ m -> m =N= n + (m ∸ n)
Proof.natpaths:= paths: nat -> nat -> Type
forall n m : nat, n ≤ m -> m =N= n + (m ∸ n)
intros n m E.natpaths:= paths: nat -> nat -> Type
n, m: nat
E: n ≤ m
m =N= n + (m ∸ n) apply le_exists in E.natpaths:= paths: nat -> nat -> Type
n, m: nat
E: {k : nat & m =N= k + n}
m =N= n + (m ∸ n)
destruct E as [k E];rewrite E.natpaths:= paths: nat -> nat -> Type
n, m, k: nat
E: m =N= k + n
k + n =N= n + (k + n ∸ n)
rewrite plus_minus.natpaths:= paths: nat -> nat -> Type
n, m, k: nat
E: m =N= k + n
k + n =N= n + k apply add_comm.
Qed.

Lemma minus_ge : forall a b, a <= b -> cut_minus a b =N= 0.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a ≤ b -> a ∸ b =N= 0
Proof.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a ≤ b -> a ∸ b =N= 0
unfold cut_minus,nat_cut_minus.natpaths:= paths: nat -> nat -> Type
forall a b : nat, a ≤ b -> Core.sub a b =N= 0
intros a b;revert a;induction b as [|b IH];intros [|a];simpl.natpaths:= paths: nat -> nat -> Type
0 ≤ 0 -> 0 =N= 0
natpaths:= paths: nat -> nat -> Type
a: nat
a.+1 ≤ 0 -> a.+1 =N= 0
natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, a ≤ b -> Core.sub a b =N= 0
0 ≤ b.+1 -> 0 =N= 0
natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, a ≤ b -> Core.sub a b =N= 0
a: nat
a.+1 ≤ b.+1 -> Core.sub a b =N= 0
-natpaths:= paths: nat -> nat -> Type
0 ≤ 0 -> 0 =N= 0 split.
-natpaths:= paths: nat -> nat -> Type
a: nat
a.+1 ≤ 0 -> a.+1 =N= 0 intros E;destruct (not_lt_0 _ E).
-natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, a ≤ b -> Core.sub a b =N= 0
0 ≤ b.+1 -> 0 =N= 0 split.
-natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, a ≤ b -> Core.sub a b =N= 0
a: nat
a.+1 ≤ b.+1 -> Core.sub a b =N= 0 intros E.natpaths:= paths: nat -> nat -> Type
b: nat
IH: forall a : nat, a ≤ b -> Core.sub a b =N= 0
a: nat
E: a.+1 ≤ b.+1
Core.sub a b =N= 0 apply IH;apply le_S_S,E.
Qed.

Global Instance nat_cut_minus_spec : CutMinusSpec@{N N} nat nat_cut_minus.natpaths:= paths: nat -> nat -> Type
CutMinusSpec nat nat_cut_minus
Proof.natpaths:= paths: nat -> nat -> Type
CutMinusSpec nat nat_cut_minus
split.natpaths:= paths: nat -> nat -> Type
forall x y : nat, y ≤ x -> x ∸ y + y = x
natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≤ y -> x ∸ y = 0
-natpaths:= paths: nat -> nat -> Type
forall x y : nat, y ≤ x -> x ∸ y + y = x intros x y E.natpaths:= paths: nat -> nat -> Type
x, y: nat
E: y ≤ x
x ∸ y + y = x rewrite add_comm.natpaths:= paths: nat -> nat -> Type
x, y: nat
E: y ≤ x
y + (x ∸ y) = x
  symmetry.natpaths:= paths: nat -> nat -> Type
x, y: nat
E: y ≤ x
x = y + (x ∸ y)
  apply (le_plus_minus _ _ E).
-natpaths:= paths: nat -> nat -> Type
forall x y : nat, x ≤ y -> x ∸ y = 0 apply minus_ge.
Qed.

End nat_lift.