matita-arithmetics-nat.agda

open import Agda.Primitive
open import matita-basics-relations
open import matita-basics-logic
open import matita-basics-bool

data nat : Set (lzero) where
  O : nat
  S : (X---v : nat) -> nat

match-nat : (return-sort-v : Level) -> (return-type-v : (z-v : nat) -> Set return-sort-v) -> (case-O-v : return-type-v O) -> (case-S-v : (X---v : nat) -> return-type-v (S X---v)) -> (z-v : nat) -> return-type-v z-v
match-nat _ _ case0 caseS O = case0
match-nat _ _ case0 caseS (S x) = caseS x

nat-ind : (l5-v : Level) -> (Q--v : (X-x-365-v : nat) -> Set l5-v) -> (X-H-O-v : Q--v O) -> (X-H-S-v : (x-366-v : nat) -> (X-x-368-v : Q--v x-366-v) -> Q--v (S x-366-v)) -> (x-365-v : nat) -> Q--v x-365-v
nat-ind _ _ case0 caseS O = case0
nat-ind l P case0 caseS (S x) = caseS x (nat-ind l P case0 caseS x)

nat-rect-Type4 : (l5-v : Level) -> (Q--v : (X-x-369-v : nat) -> Set l5-v) -> (X-H-O-v : Q--v O) -> (X-H-S-v : (x-370-v : nat) -> (X-x-372-v : Q--v x-370-v) -> Q--v (S x-370-v)) -> (x-369-v : nat) -> Q--v x-369-v
nat-rect-Type4 _ _ case0 caseS O = case0
nat-rect-Type4 l P case0 caseS (S x) = caseS x (nat-ind l P case0 caseS x)

nat-rect-Type3 : (l5-v : Level) -> (Q--v : (X-x-369-v : nat) -> Set l5-v) -> (X-H-O-v : Q--v O) -> (X-H-S-v : (x-370-v : nat) -> (X-x-372-v : Q--v x-370-v) -> Q--v (S x-370-v)) -> (x-369-v : nat) -> Q--v x-369-v
nat-rect-Type3 _ _ case0 caseS O = case0
nat-rect-Type3 l P case0 caseS (S x) = caseS x (nat-ind l P case0 caseS x)

nat-rect-Type2 : (l5-v : Level) -> (Q--v : (X-x-369-v : nat) -> Set l5-v) -> (X-H-O-v : Q--v O) -> (X-H-S-v : (x-370-v : nat) -> (X-x-372-v : Q--v x-370-v) -> Q--v (S x-370-v)) -> (x-369-v : nat) -> Q--v x-369-v
nat-rect-Type2 _ _ case0 caseS O = case0
nat-rect-Type2 l P case0 caseS (S x) = caseS x (nat-ind l P case0 caseS x)

nat-rect-Type1 : (l5-v : Level) -> (Q--v : (X-x-369-v : nat) -> Set l5-v) -> (X-H-O-v : Q--v O) -> (X-H-S-v : (x-370-v : nat) -> (X-x-372-v : Q--v x-370-v) -> Q--v (S x-370-v)) -> (x-369-v : nat) -> Q--v x-369-v
nat-rect-Type1 _ _ case0 caseS O = case0
nat-rect-Type1 l P case0 caseS (S x) = caseS x (nat-ind l P case0 caseS x)

nat-rect-Type0 : (l5-v : Level) -> (Q--v : (X-x-369-v : nat) -> Set l5-v) -> (X-H-O-v : Q--v O) -> (X-H-S-v : (x-370-v : nat) -> (X-x-372-v : Q--v x-370-v) -> Q--v (S x-370-v)) -> (x-369-v : nat) -> Q--v x-369-v
nat-rect-Type0 _ _ case0 caseS O = case0
nat-rect-Type0 l P case0 caseS (S x) = caseS x (nat-ind l P case0 caseS x)




nat-inv-ind : (l18 : Level) -> (Hterm : nat) -> (P : (X-z653 : nat) -> Set l18) -> (X-H1 : (X-z654 : eq lzero nat Hterm O) -> P O) -> (X-H2 : (x-366 : nat) -> (X-x-368 : (X-z654 : eq lzero nat Hterm x-366) -> P x-366) -> (X-z654 : eq lzero nat Hterm (S x-366)) -> P (S x-366)) -> P Hterm
nat-inv-ind = λ (l18 : Level) -> λ (Hterm : nat) -> λ (P : (X-z653 : nat) -> Set l18) -> λ (H1 : (X-z654 : eq lzero nat Hterm O) -> P O) -> λ (H2 : (x-366 : nat) -> (X-x-368 : (X-z654 : eq lzero nat Hterm x-366) -> P x-366) -> (X-z654 : eq lzero nat Hterm (S x-366)) -> P (S x-366)) -> nat-ind l18 (λ (X-x-365 : nat) -> (X-z654 : eq lzero nat Hterm X-x-365) -> P X-x-365) H1 H2 Hterm (refl lzero nat Hterm)

nat-inv-rect-Type4 : (l18 : Level) -> (Hterm : nat) -> (P : (X-z659 : nat) -> Set l18) -> (X-H1 : (X-z660 : eq lzero nat Hterm O) -> P O) -> (X-H2 : (x-370 : nat) -> (X-x-372 : (X-z660 : eq lzero nat Hterm x-370) -> P x-370) -> (X-z660 : eq lzero nat Hterm (S x-370)) -> P (S x-370)) -> P Hterm
nat-inv-rect-Type4 = λ (l18 : Level) -> λ (Hterm : nat) -> λ (P : (X-z659 : nat) -> Set l18) -> λ (H1 : (X-z660 : eq lzero nat Hterm O) -> P O) -> λ (H2 : (x-370 : nat) -> (X-x-372 : (X-z660 : eq lzero nat Hterm x-370) -> P x-370) -> (X-z660 : eq lzero nat Hterm (S x-370)) -> P (S x-370)) -> nat-rect-Type4 l18 (λ (X-x-369 : nat) -> (X-z660 : eq lzero nat Hterm X-x-369) -> P X-x-369) H1 H2 Hterm (refl lzero nat Hterm)

nat-inv-rect-Type3 : (l18 : Level) -> (Hterm : nat) -> (P : (X-z665 : nat) -> Set l18) -> (X-H1 : (X-z666 : eq lzero nat Hterm O) -> P O) -> (X-H2 : (x-378 : nat) -> (X-x-380 : (X-z666 : eq lzero nat Hterm x-378) -> P x-378) -> (X-z666 : eq lzero nat Hterm (S x-378)) -> P (S x-378)) -> P Hterm
nat-inv-rect-Type3 = λ (l18 : Level) -> λ (Hterm : nat) -> λ (P : (X-z665 : nat) -> Set l18) -> λ (H1 : (X-z666 : eq lzero nat Hterm O) -> P O) -> λ (H2 : (x-378 : nat) -> (X-x-380 : (X-z666 : eq lzero nat Hterm x-378) -> P x-378) -> (X-z666 : eq lzero nat Hterm (S x-378)) -> P (S x-378)) -> nat-rect-Type3 l18 (λ (X-x-377 : nat) -> (X-z666 : eq lzero nat Hterm X-x-377) -> P X-x-377) H1 H2 Hterm (refl lzero nat Hterm)

nat-inv-rect-Type2 : (l18 : Level) -> (Hterm : nat) -> (P : (X-z671 : nat) -> Set l18) -> (X-H1 : (X-z672 : eq lzero nat Hterm O) -> P O) -> (X-H2 : (x-382 : nat) -> (X-x-384 : (X-z672 : eq lzero nat Hterm x-382) -> P x-382) -> (X-z672 : eq lzero nat Hterm (S x-382)) -> P (S x-382)) -> P Hterm
nat-inv-rect-Type2 = λ (l18 : Level) -> λ (Hterm : nat) -> λ (P : (X-z671 : nat) -> Set l18) -> λ (H1 : (X-z672 : eq lzero nat Hterm O) -> P O) -> λ (H2 : (x-382 : nat) -> (X-x-384 : (X-z672 : eq lzero nat Hterm x-382) -> P x-382) -> (X-z672 : eq lzero nat Hterm (S x-382)) -> P (S x-382)) -> nat-rect-Type2 l18 (λ (X-x-381 : nat) -> (X-z672 : eq lzero nat Hterm X-x-381) -> P X-x-381) H1 H2 Hterm (refl lzero nat Hterm)

nat-inv-rect-Type1 : (l18 : Level) -> (Hterm : nat) -> (P : (X-z677 : nat) -> Set l18) -> (X-H1 : (X-z678 : eq lzero nat Hterm O) -> P O) -> (X-H2 : (x-386 : nat) -> (X-x-388 : (X-z678 : eq lzero nat Hterm x-386) -> P x-386) -> (X-z678 : eq lzero nat Hterm (S x-386)) -> P (S x-386)) -> P Hterm
nat-inv-rect-Type1 = λ (l18 : Level) -> λ (Hterm : nat) -> λ (P : (X-z677 : nat) -> Set l18) -> λ (H1 : (X-z678 : eq lzero nat Hterm O) -> P O) -> λ (H2 : (x-386 : nat) -> (X-x-388 : (X-z678 : eq lzero nat Hterm x-386) -> P x-386) -> (X-z678 : eq lzero nat Hterm (S x-386)) -> P (S x-386)) -> nat-rect-Type1 l18 (λ (X-x-385 : nat) -> (X-z678 : eq lzero nat Hterm X-x-385) -> P X-x-385) H1 H2 Hterm (refl lzero nat Hterm)

nat-inv-rect-Type0 : (l18 : Level) -> (Hterm : nat) -> (P : (X-z683 : nat) -> Set l18) -> (X-H1 : (X-z684 : eq lzero nat Hterm O) -> P O) -> (X-H2 : (x-390 : nat) -> (X-x-392 : (X-z684 : eq lzero nat Hterm x-390) -> P x-390) -> (X-z684 : eq lzero nat Hterm (S x-390)) -> P (S x-390)) -> P Hterm
nat-inv-rect-Type0 = λ (l18 : Level) -> λ (Hterm : nat) -> λ (P : (X-z683 : nat) -> Set l18) -> λ (H1 : (X-z684 : eq lzero nat Hterm O) -> P O) -> λ (H2 : (x-390 : nat) -> (X-x-392 : (X-z684 : eq lzero nat Hterm x-390) -> P x-390) -> (X-z684 : eq lzero nat Hterm (S x-390)) -> P (S x-390)) -> nat-rect-Type0 l18 (λ (X-x-389 : nat) -> (X-z684 : eq lzero nat Hterm X-x-389) -> P X-x-389) H1 H2 Hterm (refl lzero nat Hterm)

nat-discr : (l118 : Level) -> (x : nat) -> (y : nat) -> (X-e : eq lzero nat x y) -> match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-- : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) (match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-- : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) ((P : Set l118) -> (X-z23 : P) -> P) (λ (u0 : nat) -> (P : Set l118) -> P) y) (λ (t0 : nat) -> match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-- : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) ((P : Set l118) -> P) (λ (u0 : nat) -> (P : Set l118) -> (X-z24 : (X-e0 : eq lzero nat (R0 lzero nat t0) u0) -> P) -> P) y) x
nat-discr = λ (l118 : Level) -> λ (x : nat) -> λ (y : nat) -> λ (Deq : eq lzero nat x y) -> eq-rect-Type2 lzero ((lsuc lzero) ⊔ (lsuc l118)) nat x (λ (x-13 : nat) -> λ (X-x-14 : eq lzero nat x x-13) -> match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-- : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) (match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-- : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) ((P : Set l118) -> (X-z23 : P) -> P) (λ (u0 : nat) -> (P : Set l118) -> P) x-13) (λ (t0 : nat) -> match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-- : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) ((P : Set l118) -> P) (λ (u0 : nat) -> (P : Set l118) -> (X-z24 : (X-e0 : eq lzero nat (R0 lzero nat t0) u0) -> P) -> P) x-13) x) (match-nat ((lsuc lzero) ⊔ (lsuc l118)) (λ (X-- : nat) -> match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-0 : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) (match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-0 : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) ((P : Set l118) -> (X-z23 : P) -> P) (λ (u0 : nat) -> (P : Set l118) -> P) X--) (λ (t0 : nat) -> match-nat ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l118))) (λ (X-0 : nat) -> Set ((lsuc lzero) ⊔ (lsuc l118))) ((P : Set l118) -> P) (λ (u0 : nat) -> (P : Set l118) -> (X-z24 : (X-e0 : eq lzero nat (R0 lzero nat t0) u0) -> P) -> P) X--) X--) (λ (P : Set l118) -> λ (DH : P) -> DH) (λ (a0 : nat) -> λ (P : Set l118) -> λ (DH : (X-e0 : eq lzero nat (R0 lzero nat a0) a0) -> P) -> DH (refl lzero nat (R0 lzero nat a0))) x) y Deq

pred : (X-n : nat) -> nat
pred = λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> nat) O (λ (p : nat) -> p) n

not-zero : (l7 : Level) -> (X-- : nat) -> Set l7
not-zero = λ (l7 : Level) -> λ (n : nat) -> match-nat ((lsuc lzero) ⊔ (lsuc l7)) (λ (X-- : nat) -> Set l7) (False l7) (λ (p : nat) -> True l7) n

data le (n : nat) : nat -> Set (lzero) where
  le-n' : le n n
  le-S' : (m : nat) -> le n m -> le n (S m)

le-n : (n-v : nat) -> le n-v n-v
le-n _ = le-n'
le-S : (n-v : nat) -> (m-v : nat) -> (X---v : le n-v m-v) -> le n-v (S m-v)
le-S _ = le-S'

match-le : (X-n-v : nat) -> (return-sort-v : Level) -> (return-type-v : (X---v : nat) -> (z-v : le X-n-v X---v) -> Set return-sort-v) -> (case-le-n-v : return-type-v X-n-v (le-n X-n-v)) -> (case-le-S-v : (m-v : nat) -> (X---v : le X-n-v m-v) -> return-type-v (S m-v) (le-S X-n-v m-v X---v)) -> (X---v : nat) -> (z-v : le X-n-v X---v) -> return-type-v X---v z-v
match-le _ _ _ casen caseS _ le-n' = casen
match-le n1 l P casen caseS (S n) (le-S' n p) = caseS n p

le-ind : (l7-v : Level) -> (X-n-v : nat) -> (Q--v : (x-417-v : nat) -> (X-x-418-v : le X-n-v x-417-v) -> Set l7-v) -> (X-H-le-n-v : Q--v X-n-v (le-n X-n-v)) -> (X-H-le-S-v : (m-v : nat) -> (x-419-v : le X-n-v m-v) -> (X-x-421-v : Q--v m-v x-419-v) -> Q--v (S m-v) (le-S X-n-v m-v x-419-v)) -> (x-417-v : nat) -> (x-418-v : le X-n-v x-417-v) -> Q--v x-417-v x-418-v
le-ind _ _ _ casen caseS _ le-n' = casen
le-ind l n1 P casen caseS (S n) (le-S' n p) = caseS n p (le-ind l n1 P casen caseS n p)


le-inv-ind : (l20 : Level) -> (x1 : nat) -> (x2 : nat) -> (X-Hterm : le x1 x2) -> (P : (X-z724 : nat) -> Set l20) -> (X-H1 : (X-z725 : eq lzero nat x2 x1) -> P x1) -> (X-H2 : (m : nat) -> (X-x-419 : le x1 m) -> (X-x-421 : (X-z725 : eq lzero nat x2 m) -> P m) -> (X-z725 : eq lzero nat x2 (S m)) -> P (S m)) -> P x2
le-inv-ind = λ (l20 : Level) -> λ (x1 : nat) -> λ (x2 : nat) -> λ (Hterm : le x1 x2) -> λ (P : (X-z724 : nat) -> Set l20) -> λ (H1 : (X-z725 : eq lzero nat x2 x1) -> P x1) -> λ (H2 : (m : nat) -> (X-x-419 : le x1 m) -> (X-x-421 : (X-z725 : eq lzero nat x2 m) -> P m) -> (X-z725 : eq lzero nat x2 (S m)) -> P (S m)) -> le-ind l20 x1 (λ (x-417 : nat) -> λ (X-x-418 : le x1 x-417) -> (X-z725 : eq lzero nat x2 x-417) -> P x-417) H1 H2 x2 Hterm (refl lzero nat x2)

lt : (X-- : nat) -> (X--1 : nat) -> Set (lzero)
lt = λ (n : nat) -> λ (m : nat) -> le (S n) m

ge : (X-- : nat) -> (X--1 : nat) -> Set (lzero)
ge = λ (n : nat) -> λ (m : nat) -> le m n

gt : (X-- : nat) -> (X--1 : nat) -> Set (lzero)
gt = λ (n : nat) -> λ (m : nat) -> lt m n

increasing : (X-f : (X-- : nat) -> nat) -> Set (lzero)
increasing = λ (f : (X-- : nat) -> nat) -> (n : nat) -> lt (f n) (f (S n))


plus : (X---v : nat) -> (X--1-v : nat) -> nat
plus O m = m
plus (S x) m = S (plus x m)

times : (X---v : nat) -> (X--1-v : nat) -> nat
times O x = O
times (S x) y = plus y (times x y)

minus : (X---v : nat) -> (X--1-v : nat) -> nat
minus O m = O
minus (S x) y = match-nat lzero (λ X---v → nat) (S x) (λ q → minus x q) y

nat-case : (l51 : Level) -> (n : nat) -> (P : (X-- : nat) -> Set l51) -> (X-- : (X-- : eq lzero nat n O) -> P O) -> (X--1 : (m : nat) -> (X--1 : eq lzero nat n (S m)) -> P (S m)) -> P n
nat-case = λ (l51 : Level) -> λ (n : nat) -> λ (P : (X-- : nat) -> Set l51) -> nat-ind l51 (λ (X-x-365 : nat) -> (X-- : (X-- : eq lzero nat X-x-365 O) -> P O) -> (X--1 : (m : nat) -> (X--1 : eq lzero nat X-x-365 (S m)) -> P (S m)) -> P X-x-365) (λ (auto : (X-- : eq lzero nat O O) -> P O) -> λ (auto' : (m : nat) -> (X-- : eq lzero nat O (S m)) -> P (S m)) -> auto (refl lzero nat O)) (λ (x-366 : nat) -> λ (X-x-368 : (X-- : (X-- : eq lzero nat x-366 O) -> P O) -> (X--1 : (m : nat) -> (X--1 : eq lzero nat x-366 (S m)) -> P (S m)) -> P x-366) -> λ (auto : (X-- : eq lzero nat (S x-366) O) -> P O) -> λ (auto' : (m : nat) -> (X-- : eq lzero nat (S x-366) (S m)) -> P (S m)) -> auto' x-366 (refl lzero nat (S x-366))) n

nat-elim2 : (l22 : Level) -> (R : (X-- : nat) -> (X--1 : nat) -> Set l22) -> (X-- : (n : nat) -> R O n) -> (X--1 : (n : nat) -> R (S n) O) -> (X--2 : (n : nat) -> (m : nat) -> (X--2 : R n m) -> R (S n) (S m)) -> (n : nat) -> (m : nat) -> R n m
nat-elim2 = λ (l22 : Level) -> λ (R : (X-- : nat) -> (X--1 : nat) -> Set l22) -> λ (ROn : (n : nat) -> R O n) -> λ (RSO : (n : nat) -> R (S n) O) -> λ (RSS : (n : nat) -> (m : nat) -> (X-- : R n m) -> R (S n) (S m)) -> λ (n : nat) -> nat-ind l22 (λ (X-x-365 : nat) -> (m : nat) -> R X-x-365 m) (λ (m : nat) -> ROn m) (λ (n0 : nat) -> λ (Rn0m : (m : nat) -> R n0 m) -> λ (m : nat) -> match-nat l22 (λ (X-- : nat) -> R (S n0) X--) (RSO n0) (λ (auto : nat) -> RSS n0 auto (Rn0m auto)) m) n

le-gen : (l4 : Level) -> (P : (X-- : nat) -> Set l4) -> (n : nat) -> (X-- : (i : nat) -> (X-- : le i n) -> P i) -> P n
le-gen = λ (l4 : Level) -> λ (P : (X-- : nat) -> Set l4) -> λ (n : nat) -> λ (auto : (i : nat) -> (X-- : le i n) -> P i) -> auto n (le-n n)

pred-Sn : (n : nat) -> eq lzero nat n (pred (S n))
pred-Sn = λ (n : nat) -> refl lzero nat n

injective-S : ||injective|| lzero lzero nat nat S
injective-S = λ (x : nat) -> λ (y : nat) -> λ (auto : eq lzero nat (S x) (S y)) -> rewrite-l lzero lzero nat y (λ (X-- : nat) -> eq lzero nat X-- y) (refl lzero nat y) x (rewrite-r lzero lzero nat (pred (S x)) (λ (X-- : nat) -> eq lzero nat y X--) (rewrite-r lzero lzero nat (S y) (λ (X-- : nat) -> eq lzero nat y (pred X--)) (pred-Sn y) (S x) auto) x (pred-Sn x))

S-pred : (n : nat) -> (X-- : lt O n) -> eq lzero nat (S (pred n)) n
S-pred = λ (n : nat) -> λ (posn : lt O n) -> match-le (S O) lzero (λ (X-- : nat) -> λ (X-0 : le (S O) X--) -> eq lzero nat (S (pred X--)) X--) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (S X--) (S O)) (refl lzero nat (S O)) (pred (S O)) (pred-Sn O)) (λ (m : nat) -> λ (auto : le (S O) m) -> rewrite-l lzero lzero nat m (λ (X-- : nat) -> eq lzero nat (S X--) (S m)) (refl lzero nat (S m)) (pred (S m)) (pred-Sn m)) n posn

plus-O-n : (n : nat) -> eq lzero nat n (plus O n)
plus-O-n = λ (n : nat) -> refl lzero nat n

plus-n-O : (n : nat) -> eq lzero nat n (plus n O)
plus-n-O = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat X-x-365 (plus X-x-365 O)) (refl lzero nat O) (λ (x-366 : nat) -> λ (X-x-368 : eq lzero nat x-366 (plus x-366 O)) -> rewrite-l lzero lzero nat x-366 (λ (X-- : nat) -> eq lzero nat (S x-366) (S X--)) (refl lzero nat (S x-366)) (plus x-366 O) X-x-368) n

plus-n-Sm : (n : nat) -> (m : nat) -> eq lzero nat (S (plus n m)) (plus n (S m))
plus-n-Sm = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (m : nat) -> eq lzero nat (S (plus X-x-365 m)) (plus X-x-365 (S m))) (λ (m : nat) -> refl lzero nat (S m)) (λ (x-366 : nat) -> λ (X-x-368 : (m : nat) -> eq lzero nat (S (plus x-366 m)) (plus x-366 (S m))) -> λ (m : nat) -> rewrite-r lzero lzero nat (plus x-366 (S m)) (λ (X-- : nat) -> eq lzero nat (S X--) (S (plus x-366 (S m)))) (rewrite-r lzero lzero nat (plus x-366 (S (S m))) (λ (X-- : nat) -> eq lzero nat X-- (S (plus x-366 (S m)))) (rewrite-r lzero lzero nat (plus x-366 (S (S m))) (λ (X-- : nat) -> eq lzero nat (plus x-366 (S (S m))) X--) (refl lzero nat (plus x-366 (S (S m)))) (S (plus x-366 (S m))) (X-x-368 (S m))) (S (plus x-366 (S m))) (X-x-368 (S m))) (S (plus x-366 m)) (X-x-368 m)) n

commutative-plus : commutative lzero nat plus
commutative-plus = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (y : nat) -> eq lzero nat (plus X-x-365 y) (plus y X-x-365)) (λ (y : nat) -> rewrite-l lzero lzero nat y (λ (X-- : nat) -> eq lzero nat y X--) (refl lzero nat y) (plus y O) (plus-n-O y)) (λ (x-366 : nat) -> λ (X-x-368 : (y : nat) -> eq lzero nat (plus x-366 y) (plus y x-366)) -> λ (y : nat) -> rewrite-r lzero lzero nat (plus x-366 (S y)) (λ (X-- : nat) -> eq lzero nat X-- (plus y (S x-366))) (rewrite-r lzero lzero nat (plus y (S x-366)) (λ (X-- : nat) -> eq lzero nat X-- (plus y (S x-366))) (refl lzero nat (plus y (S x-366))) (plus x-366 (S y)) (rewrite-l lzero lzero nat (S (plus x-366 y)) (λ (X-- : nat) -> eq lzero nat X-- (plus y (S x-366))) (rewrite-r lzero lzero nat (plus y x-366) (λ (X-- : nat) -> eq lzero nat (S X--) (plus y (S x-366))) (plus-n-Sm y x-366) (plus x-366 y) (X-x-368 y)) (plus x-366 (S y)) (plus-n-Sm x-366 y))) (S (plus x-366 y)) (plus-n-Sm x-366 y)) n

associative-plus : associative lzero nat plus
associative-plus = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (y : nat) -> (z : nat) -> eq lzero nat (plus (plus X-x-365 y) z) (plus X-x-365 (plus y z))) (λ (y : nat) -> λ (z : nat) -> refl lzero nat (plus y z)) (λ (x-366 : nat) -> λ (X-x-368 : (y : nat) -> (z : nat) -> eq lzero nat (plus (plus x-366 y) z) (plus x-366 (plus y z))) -> λ (y : nat) -> λ (z : nat) -> rewrite-r lzero lzero nat (plus x-366 (plus y z)) (λ (X-- : nat) -> eq lzero nat (S X--) (S (plus x-366 (plus y z)))) (refl lzero nat (S (plus x-366 (plus y z)))) (plus (plus x-366 y) z) (X-x-368 y z)) n

assoc-plus1 : (a : nat) -> (b : nat) -> (c : nat) -> eq lzero nat (plus c (plus b a)) (plus (plus b c) a)
assoc-plus1 = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> rewrite-r lzero lzero nat (plus a b) (λ (X-- : nat) -> eq lzero nat (plus c X--) (plus (plus b c) a)) (rewrite-r lzero lzero nat (plus a (plus b c)) (λ (X-- : nat) -> eq lzero nat (plus c (plus a b)) X--) (rewrite-r lzero lzero nat (plus a (plus b c)) (λ (X-- : nat) -> eq lzero nat X-- (plus a (plus b c))) (refl lzero nat (plus a (plus b c))) (plus c (plus a b)) (rewrite-l lzero lzero nat (plus (plus a b) c) (λ (X-- : nat) -> eq lzero nat (plus c (plus a b)) X--) (commutative-plus c (plus a b)) (plus a (plus b c)) (associative-plus a b c))) (plus (plus b c) a) (commutative-plus (plus b c) a)) (plus b a) (commutative-plus b a)

injective-plus-r : (n : nat) -> ||injective|| lzero lzero nat nat (λ (m : nat) -> plus n m)
injective-plus-r = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> ||injective|| lzero lzero nat nat (λ (m : nat) -> plus X-x-365 m)) (λ (x : nat) -> λ (y : nat) -> λ (auto : eq lzero nat x y) -> rewrite-l lzero lzero nat x (λ (X-- : nat) -> eq lzero nat x X--) (refl lzero nat x) y auto) (λ (x-366 : nat) -> λ (X-x-368 : (x : nat) -> (y : nat) -> (X-- : eq lzero nat (plus x-366 x) (plus x-366 y)) -> eq lzero nat x y) -> λ (x : nat) -> λ (y : nat) -> λ (auto : eq lzero nat (S (plus x-366 x)) (S (plus x-366 y))) -> X-x-368 x y (injective-S (plus x-366 x) (plus x-366 y) (rewrite-r lzero lzero nat (plus x-366 (S x)) (λ (X-- : nat) -> eq lzero nat X-- (S (plus x-366 y))) (rewrite-r lzero lzero nat (plus x-366 (S y)) (λ (X-- : nat) -> eq lzero nat (plus x-366 (S x)) X--) (rewrite-l lzero lzero nat (plus x-366 (S x)) (λ (X-- : nat) -> eq lzero nat (plus x-366 (S x)) X--) (refl lzero nat (plus x-366 (S x))) (plus x-366 (S y)) (rewrite-l lzero lzero nat (S (plus x-366 y)) (λ (X-- : nat) -> eq lzero nat (plus x-366 (S x)) X--) (rewrite-l lzero lzero nat (S (plus x-366 x)) (λ (X-- : nat) -> eq lzero nat X-- (S (plus x-366 y))) auto (plus x-366 (S x)) (plus-n-Sm x-366 x)) (plus x-366 (S y)) (plus-n-Sm x-366 y))) (S (plus x-366 y)) (plus-n-Sm x-366 y)) (S (plus x-366 x)) (plus-n-Sm x-366 x)))) n

injective-plus-l : (n : nat) -> ||injective|| lzero lzero nat nat (λ (m : nat) -> plus m n)
injective-plus-l = λ (n : nat) -> λ (x : nat) -> λ (y : nat) -> λ (auto : eq lzero nat (plus x n) (plus y n)) -> injective-plus-r n x y (rewrite-r lzero lzero nat (plus n y) (λ (X-- : nat) -> eq lzero nat X-- (plus n y)) (refl lzero nat (plus n y)) (plus n x) (rewrite-l lzero lzero nat (plus y n) (λ (X-- : nat) -> eq lzero nat (plus n x) X--) (rewrite-l lzero lzero nat (plus x n) (λ (X-- : nat) -> eq lzero nat X-- (plus y n)) auto (plus n x) (commutative-plus x n)) (plus n y) (commutative-plus y n)))

times-Sn-m : (n : nat) -> (m : nat) -> eq lzero nat (plus m (times n m)) (times (S n) m)
times-Sn-m = λ (n : nat) -> λ (m : nat) -> refl lzero nat (plus m (times n m))

times-O-n : (n : nat) -> eq lzero nat O (times O n)
times-O-n = λ (n : nat) -> refl lzero nat O

times-n-O : (n : nat) -> eq lzero nat O (times n O)
times-n-O = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat O (times X-x-365 O)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat O X--) (refl lzero nat O) (times O O) (times-O-n O)) (λ (x-366 : nat) -> λ (X-x-368 : eq lzero nat O (times x-366 O)) -> rewrite-l lzero lzero nat (plus O (times x-366 O)) (λ (X-- : nat) -> eq lzero nat O X--) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat O (plus O X--)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat O X--) (refl lzero nat O) (plus O O) (plus-O-n O)) (times x-366 O) X-x-368) (times (S x-366) O) (times-Sn-m x-366 O)) n

times-n-Sm : (n : nat) -> (m : nat) -> eq lzero nat (plus n (times n m)) (times n (S m))
times-n-Sm = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (m : nat) -> eq lzero nat (plus X-x-365 (times X-x-365 m)) (times X-x-365 (S m))) (λ (X-m : nat) -> refl lzero nat O) (λ (x-366 : nat) -> λ (X-x-368 : (m : nat) -> eq lzero nat (plus x-366 (times x-366 m)) (times x-366 (S m))) -> λ (m : nat) -> rewrite-r lzero lzero nat (plus x-366 (S (plus m (times x-366 m)))) (λ (X-- : nat) -> eq lzero nat X-- (S (plus m (times x-366 (S m))))) (rewrite-r lzero lzero nat (plus m (S (times x-366 m))) (λ (X-- : nat) -> eq lzero nat (plus x-366 X--) (S (plus m (times x-366 (S m))))) (rewrite-l lzero lzero nat (plus x-366 (times x-366 m)) (λ (X-- : nat) -> eq lzero nat (plus x-366 (plus m (S (times x-366 m)))) (S (plus m X--))) (rewrite-r lzero lzero nat (plus x-366 (plus m (times x-366 m))) (λ (X-- : nat) -> eq lzero nat (plus x-366 (plus m (S (times x-366 m)))) (S X--)) (rewrite-r lzero lzero nat (plus x-366 (S (plus m (times x-366 m)))) (λ (X-- : nat) -> eq lzero nat (plus x-366 (plus m (S (times x-366 m)))) X--) (rewrite-r lzero lzero nat (plus m (S (times x-366 m))) (λ (X-- : nat) -> eq lzero nat (plus x-366 (plus m (S (times x-366 m)))) (plus x-366 X--)) (refl lzero nat (plus x-366 (plus m (S (times x-366 m))))) (S (plus m (times x-366 m))) (plus-n-Sm m (times x-366 m))) (S (plus x-366 (plus m (times x-366 m)))) (plus-n-Sm x-366 (plus m (times x-366 m)))) (plus m (plus x-366 (times x-366 m))) (rewrite-l lzero lzero nat (plus (plus x-366 m) (times x-366 m)) (λ (X-- : nat) -> eq lzero nat (plus m (plus x-366 (times x-366 m))) X--) (assoc-plus1 (times x-366 m) x-366 m) (plus x-366 (plus m (times x-366 m))) (associative-plus x-366 m (times x-366 m)))) (times x-366 (S m)) (X-x-368 m)) (S (plus m (times x-366 m))) (plus-n-Sm m (times x-366 m))) (S (plus x-366 (plus m (times x-366 m)))) (plus-n-Sm x-366 (plus m (times x-366 m)))) n

commutative-times : commutative lzero nat times
commutative-times = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (y : nat) -> eq lzero nat (times X-x-365 y) (times y X-x-365)) (λ (y : nat) -> rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat O X--) (refl lzero nat O) (times y O) (times-n-O y)) (λ (x-366 : nat) -> λ (X-x-368 : (y : nat) -> eq lzero nat (times x-366 y) (times y x-366)) -> λ (y : nat) -> rewrite-l lzero lzero nat (plus y (times y x-366)) (λ (X-- : nat) -> eq lzero nat (plus y (times x-366 y)) X--) (rewrite-l lzero lzero nat (times x-366 y) (λ (X-- : nat) -> eq lzero nat (plus y (times x-366 y)) (plus y X--)) (refl lzero nat (plus y (times x-366 y))) (times y x-366) (X-x-368 y)) (times y (S x-366)) (times-n-Sm y x-366)) n

distributive-times-plus : distributive lzero nat times plus
distributive-times-plus = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (y : nat) -> (z : nat) -> eq lzero nat (times X-x-365 (plus y z)) (plus (times X-x-365 y) (times X-x-365 z))) (λ (X-y : nat) -> λ (X-z : nat) -> refl lzero nat O) (λ (x-366 : nat) -> λ (X-x-368 : (y : nat) -> (z : nat) -> eq lzero nat (times x-366 (plus y z)) (plus (times x-366 y) (times x-366 z))) -> λ (y : nat) -> λ (z : nat) -> rewrite-r lzero lzero nat (plus y (plus z (times x-366 (plus y z)))) (λ (X-- : nat) -> eq lzero nat X-- (plus (plus y (times x-366 y)) (plus z (times x-366 z)))) (rewrite-r lzero lzero nat (plus y (plus (times x-366 y) (plus z (times x-366 z)))) (λ (X-- : nat) -> eq lzero nat (plus y (plus z (times x-366 (plus y z)))) X--) (rewrite-r lzero lzero nat (plus z (plus (times x-366 y) (times x-366 z))) (λ (X-- : nat) -> eq lzero nat (plus y (plus z (times x-366 (plus y z)))) (plus y X--)) (rewrite-l lzero lzero nat (times x-366 (plus y z)) (λ (X-- : nat) -> eq lzero nat (plus y (plus z (times x-366 (plus y z)))) (plus y (plus z X--))) (refl lzero nat (plus y (plus z (times x-366 (plus y z))))) (plus (times x-366 y) (times x-366 z)) (X-x-368 y z)) (plus (times x-366 y) (plus z (times x-366 z))) (rewrite-l lzero lzero nat (plus (plus z (times x-366 y)) (times x-366 z)) (λ (X-- : nat) -> eq lzero nat (plus (times x-366 y) (plus z (times x-366 z))) X--) (assoc-plus1 (times x-366 z) z (times x-366 y)) (plus z (plus (times x-366 y) (times x-366 z))) (associative-plus z (times x-366 y) (times x-366 z)))) (plus (plus y (times x-366 y)) (plus z (times x-366 z))) (associative-plus y (times x-366 y) (plus z (times x-366 z)))) (plus (plus y z) (times x-366 (plus y z))) (associative-plus y z (times x-366 (plus y z)))) n

distributive-times-plus-r : (a : nat) -> (b : nat) -> (c : nat) -> eq lzero nat (times (plus b c) a) (plus (times b a) (times c a))
distributive-times-plus-r = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> rewrite-r lzero lzero nat (times a (plus b c)) (λ (X-- : nat) -> eq lzero nat X-- (plus (times b a) (times c a))) (rewrite-r lzero lzero nat (times a b) (λ (X-- : nat) -> eq lzero nat (times a (plus b c)) (plus X-- (times c a))) (rewrite-r lzero lzero nat (times a c) (λ (X-- : nat) -> eq lzero nat (times a (plus b c)) (plus (times a b) X--)) (rewrite-l lzero lzero nat (times a (plus b c)) (λ (X-- : nat) -> eq lzero nat (times a (plus b c)) X--) (refl lzero nat (times a (plus b c))) (plus (times a b) (times a c)) (distributive-times-plus a b c)) (times c a) (commutative-times c a)) (times b a) (commutative-times b a)) (times (plus b c) a) (commutative-times (plus b c) a)

associative-times : associative lzero nat times
associative-times = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (y : nat) -> (z : nat) -> eq lzero nat (times (times X-x-365 y) z) (times X-x-365 (times y z))) (λ (X-y : nat) -> λ (X-z : nat) -> refl lzero nat O) (λ (x-366 : nat) -> λ (X-x-368 : (y : nat) -> (z : nat) -> eq lzero nat (times (times x-366 y) z) (times x-366 (times y z))) -> λ (y : nat) -> λ (z : nat) -> rewrite-r lzero lzero nat (plus (times y z) (times x-366 (times y z))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times y z) (times x-366 (times y z)))) (refl lzero nat (plus (times y z) (times x-366 (times y z)))) (times (plus y (times x-366 y)) z) (rewrite-l lzero lzero nat (times (times x-366 y) z) (λ (X-- : nat) -> eq lzero nat (times (plus y (times x-366 y)) z) (plus (times y z) X--)) (distributive-times-plus-r z y (times x-366 y)) (times x-366 (times y z)) (X-x-368 y z))) n

times-times : (x : nat) -> (y : nat) -> (z : nat) -> eq lzero nat (times x (times y z)) (times y (times x z))
times-times = λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> rewrite-r lzero lzero nat (times y (times x z)) (λ (X-- : nat) -> eq lzero nat X-- (times y (times x z))) (refl lzero nat (times y (times x z))) (times x (times y z)) (rewrite-l lzero lzero nat (times (times x y) z) (λ (X-- : nat) -> eq lzero nat X-- (times y (times x z))) (rewrite-l lzero lzero nat (times y x) (λ (X-- : nat) -> eq lzero nat (times X-- z) (times y (times x z))) (associative-times y x z) (times x y) (commutative-times y x)) (times x (times y z)) (associative-times x y z))

times-n-1 : (n : nat) -> eq lzero nat n (times n (S O))
times-n-1 = λ (n : nat) -> rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat n (plus n X--)) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (plus n O) (plus-n-O n)) (times n O) (times-n-O n)) (times n (S O)) (times-n-Sm n O)

minus-S-S : (n : nat) -> (m : nat) -> eq lzero nat (minus (S n) (S m)) (minus n m)
minus-S-S = λ (n : nat) -> λ (m : nat) -> refl lzero nat (minus (S n) (S m))

minus-O-n : (n : nat) -> eq lzero nat O (minus O n)
minus-O-n = λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> eq lzero nat O (minus O X--)) (refl lzero nat O) (λ (auto : nat) -> refl lzero nat O) n

minus-n-O : (n : nat) -> eq lzero nat n (minus n O)
minus-n-O = λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> eq lzero nat X-- (minus X-- O)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat O X--) (refl lzero nat O) (minus O O) (minus-O-n O)) (λ (auto : nat) -> refl lzero nat (S auto)) n

minus-n-n : (n : nat) -> eq lzero nat O (minus n n)
minus-n-n = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat O (minus X-x-365 X-x-365)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat O X--) (refl lzero nat O) (minus O O) (minus-O-n O)) (λ (x-366 : nat) -> λ (X-x-368 : eq lzero nat O (minus x-366 x-366)) -> rewrite-r lzero lzero nat (minus x-366 x-366) (λ (X-- : nat) -> eq lzero nat O X--) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat O X--) (refl lzero nat O) (minus x-366 x-366) X-x-368) (minus (S x-366) (S x-366)) (minus-S-S x-366 x-366)) n

minus-Sn-n : (n : nat) -> eq lzero nat (S O) (minus (S n) n)
minus-Sn-n = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero nat (S O) (minus (S X-x-365) X-x-365)) (refl lzero nat (S O)) (λ (x-366 : nat) -> λ (X-x-368 : eq lzero nat (S O) (match-nat lzero (λ (X-- : nat) -> nat) (S x-366) (λ (q : nat) -> minus x-366 q) x-366)) -> rewrite-r lzero lzero nat (match-nat lzero (λ (X-- : nat) -> nat) (S x-366) (λ (q : nat) -> minus x-366 q) x-366) (λ (X-- : nat) -> eq lzero nat X-- (match-nat lzero (λ (X--1 : nat) -> nat) (S x-366) (λ (q : nat) -> minus x-366 q) x-366)) (refl lzero nat (match-nat lzero (λ (X-- : nat) -> nat) (S x-366) (λ (q : nat) -> minus x-366 q) x-366)) (S O) X-x-368) n

eq-minus-S-pred : (n : nat) -> (m : nat) -> eq lzero nat (minus n (S m)) (pred (minus n m))
eq-minus-S-pred = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> eq lzero nat (minus X-- (S X-0)) (pred (minus X-- X-0))) (λ (X-n : nat) -> refl lzero nat O) (λ (n : nat) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat X-- n) (refl lzero nat n) (minus n O) (minus-n-O n)) (λ (n : nat) -> λ (m : nat) -> λ (auto : eq lzero nat (minus n (S m)) (match-nat lzero (λ (X-- : nat) -> nat) O (λ (p : nat) -> p) (minus n m))) -> rewrite-r lzero lzero nat (match-nat lzero (λ (X-- : nat) -> nat) O (λ (p : nat) -> p) (minus n m)) (λ (X-- : nat) -> eq lzero nat X-- (match-nat lzero (λ (X-0 : nat) -> nat) O (λ (p : nat) -> p) (minus n m))) (refl lzero nat (match-nat lzero (λ (X-- : nat) -> nat) O (λ (p : nat) -> p) (minus n m))) (minus n (S m)) auto)

let-clause-73 : (x : nat) -> (y : nat) -> (z : nat) -> (x134 : nat) -> (x135 : nat) -> (x136 : nat) -> eq lzero nat (plus x134 (plus x135 x136)) (plus x135 (plus x134 x136))
let-clause-73 = λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> λ (x134 : nat) -> λ (x135 : nat) -> λ (x136 : nat) -> rewrite-l lzero lzero nat (plus (plus x135 x134) x136) (λ (X-- : nat) -> eq lzero nat (plus x134 (plus x135 x136)) X--) (assoc-plus1 x136 x135 x134) (plus x135 (plus x134 x136)) (associative-plus x135 x134 x136)

plus-plus-comm-23 : (x : nat) -> (y : nat) -> (z : nat) -> eq lzero nat (plus (plus x y) z) (plus (plus x z) y)
plus-plus-comm-23 = λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> rewrite-r lzero lzero nat (plus z (plus x y)) (λ (X-- : nat) -> eq lzero nat X-- (plus (plus x z) y)) (rewrite-r lzero lzero nat (plus x (plus z y)) (λ (X-- : nat) -> eq lzero nat X-- (plus (plus x z) y)) (rewrite-r lzero lzero nat (plus y z) (λ (X-- : nat) -> eq lzero nat (plus x X--) (plus (plus x z) y)) (rewrite-r lzero lzero nat (plus y (plus x z)) (λ (X-- : nat) -> eq lzero nat (plus x (plus y z)) X--) (rewrite-r lzero lzero nat (plus x (plus y z)) (λ (X-- : nat) -> eq lzero nat (plus x (plus y z)) X--) (refl lzero nat (plus x (plus y z))) (plus y (plus x z)) (let-clause-73 x y z y x z)) (plus (plus x z) y) (commutative-plus (plus x z) y)) (plus z y) (commutative-plus z y)) (plus z (plus x y)) (let-clause-73 x y z z x y)) (plus (plus x y) z) (commutative-plus (plus x y) z)

discr-plus-xy-minus-xz : (x : nat) -> (z : nat) -> (y : nat) -> (X-- : eq lzero nat (plus x y) (minus x z)) -> eq lzero nat y O
discr-plus-xy-minus-xz = λ (x : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (z : nat) -> (y : nat) -> (X-- : eq lzero nat (plus X-x-365 y) (minus X-x-365 z)) -> eq lzero nat y O) (λ (z : nat) -> λ (y : nat) -> λ (auto : eq lzero nat (plus O y) (minus O z)) -> rewrite-l lzero lzero nat y (λ (X-- : nat) -> eq lzero nat y X--) (refl lzero nat y) O (rewrite-r lzero lzero nat (minus O z) (λ (X-- : nat) -> eq lzero nat y X--) (rewrite-r lzero lzero nat (plus y O) (λ (X-- : nat) -> eq lzero nat X-- (minus O z)) (rewrite-l lzero lzero nat (plus O y) (λ (X-- : nat) -> eq lzero nat X-- (minus O z)) auto (plus y O) (commutative-plus O y)) y (plus-n-O y)) O (minus-O-n z))) (λ (x0 : nat) -> λ (IHx : (z : nat) -> (y : nat) -> (X-- : eq lzero nat (plus x0 y) (minus x0 z)) -> eq lzero nat y O) -> λ (X-clearme : nat) -> match-nat lzero (λ (X-- : nat) -> (y : nat) -> (X--1 : eq lzero nat (plus (S x0) y) (minus (S x0) X--)) -> eq lzero nat y O) (λ (y : nat) -> λ (H : eq lzero nat (S (plus x0 y)) (S x0)) -> IHx O y (eq-ind lzero lzero nat x0 (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat x0 x-1) -> eq lzero nat (plus x0 y) x-1) (injective-S (plus x0 y) x0 (rewrite-r lzero lzero nat (plus x0 (S y)) (λ (X-- : nat) -> eq lzero nat X-- (S x0)) (rewrite-r lzero lzero nat (S x0) (λ (X-- : nat) -> eq lzero nat X-- (S x0)) (refl lzero nat (S x0)) (plus x0 (S y)) (rewrite-l lzero lzero nat (S (plus x0 y)) (λ (X-- : nat) -> eq lzero nat X-- (S x0)) H (plus x0 (S y)) (plus-n-Sm x0 y))) (S (plus x0 y)) (plus-n-Sm x0 y))) (minus x0 O) (minus-n-O x0))) (λ (z : nat) -> λ (y : nat) -> eq-ind-r lzero lzero nat (plus x0 (S y)) (λ (x1 : nat) -> λ (X-- : eq lzero nat x1 (plus x0 (S y))) -> (X--1 : eq lzero nat x1 (minus x0 z)) -> eq lzero nat y O) (λ (H : eq lzero nat (plus x0 (S y)) (minus x0 z)) -> nat-discr lzero (S y) O (IHx z (S y) H) (eq lzero nat y O)) (S (plus x0 y)) (plus-n-Sm x0 y)) X-clearme) x

not-eq-S : (n : nat) -> (m : nat) -> (X-- : Not lzero (eq lzero nat n m)) -> Not lzero (eq lzero nat (S n) (S m))
not-eq-S = λ (n : nat) -> λ (m : nat) -> λ (auto : Not lzero (eq lzero nat n m)) -> not-to-not lzero (eq lzero nat (S n) (S m)) (eq lzero nat n m) (λ (auto' : eq lzero nat (S n) (S m)) -> rewrite-l lzero lzero nat m (λ (X-- : nat) -> eq lzero nat X-- m) (refl lzero nat m) n (rewrite-r lzero lzero nat (pred (S n)) (λ (X-- : nat) -> eq lzero nat m X--) (rewrite-r lzero lzero nat (S m) (λ (X-- : nat) -> eq lzero nat m (pred X--)) (pred-Sn m) (S n) auto') n (pred-Sn n))) auto

not-eq-O-S : (n : nat) -> Not lzero (eq lzero nat O (S n))
not-eq-O-S = λ (n : nat) -> nmk lzero (eq lzero nat O (S n)) (λ (eqOS : eq lzero nat O (S n)) -> eq-ind-r lzero lzero nat (S n) (λ (x : nat) -> λ (X-- : eq lzero nat x (S n)) -> not-zero lzero x) (I lzero) O eqOS)

not-eq-n-Sn : (n : nat) -> Not lzero (eq lzero nat n (S n))
not-eq-n-Sn = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> Not lzero (eq lzero nat X-x-365 (S X-x-365))) (not-eq-O-S O) (λ (x-366 : nat) -> λ (X-x-368 : Not lzero (eq lzero nat x-366 (S x-366))) -> not-eq-S x-366 (S x-366) X-x-368) n

lt-to-not-zero : (l6 : Level) -> (n : nat) -> (m : nat) -> (X-- : lt n m) -> not-zero l6 m
lt-to-not-zero = λ (l6 : Level) -> λ (n : nat) -> λ (m : nat) -> λ (Hlt : lt n m) -> le-ind l6 (S n) (λ (x-417 : nat) -> λ (X-x-418 : le (S n) x-417) -> not-zero l6 x-417) (I l6) (λ (m0 : nat) -> λ (X-x-419 : le (S n) m0) -> λ (X-x-421 : not-zero l6 m0) -> I l6) m Hlt

le-S-S : (n : nat) -> (m : nat) -> (X-- : le n m) -> le (S n) (S m)
le-S-S = λ (n : nat) -> λ (m : nat) -> λ (lenm : le n m) -> le-ind lzero n (λ (x-417 : nat) -> λ (X-x-418 : le n x-417) -> le (S n) (S x-417)) (le-n (S n)) (λ (m0 : nat) -> λ (X-x-419 : le n m0) -> λ (X-x-421 : le (S n) (S m0)) -> le-S (S n) (S m0) X-x-421) m lenm

le-O-n : (n : nat) -> le O n
le-O-n = λ (n : nat) -> nat-ind lzero (le O) (le-n O) (λ (x-366 : nat) -> λ (X-x-368 : le O x-366) -> le-S O x-366 X-x-368) n

le-n-Sn : (n : nat) -> le n (S n)
le-n-Sn = λ (n : nat) -> le-S n n (le-n n)

transitive-le : transitive lzero lzero nat le
transitive-le = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (leab : le a b) -> λ (lebc : le b c) -> le-ind lzero b (λ (x-417 : nat) -> λ (X-x-418 : le b x-417) -> le a x-417) leab (λ (m : nat) -> λ (X-x-419 : le b m) -> λ (X-x-421 : le a m) -> le-S a m X-x-421) c lebc

le-pred-n : (n : nat) -> le (pred n) n
le-pred-n = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> le (pred X-x-365) X-x-365) (le-n (pred O)) (λ (x-366 : nat) -> λ (X-x-368 : le (pred x-366) x-366) -> le-n-Sn (pred (S x-366))) n

monotonic-pred : monotonic lzero lzero nat le pred
monotonic-pred = λ (n : nat) -> λ (m : nat) -> λ (lenm : le n m) -> le-ind lzero n (λ (x-417 : nat) -> λ (X-x-418 : le n x-417) -> le (pred n) (pred x-417)) (le-n (pred n)) (λ (m0 : nat) -> λ (X-x-419 : le n m0) -> λ (X-x-421 : le (pred n) (pred m0)) -> transitive-le (pred n) n (pred (S m0)) (le-pred-n n) X-x-419) m lenm

le-S-S-to-le : (n : nat) -> (m : nat) -> (X-- : le (S n) (S m)) -> le n m
le-S-S-to-le = λ (n : nat) -> λ (m : nat) -> λ (auto : le (S n) (S m)) -> eq-coerc lzero (le (pred (S n)) (pred (S m))) (le n m) (monotonic-pred (S n) (S m) auto) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S m))) (le n m)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n X--) (le n m)) (refl (lsuc lzero) (Set (lzero)) (le n m)) (pred (S m)) (pred-Sn m)) (pred (S n)) (pred-Sn n))

monotonic-le-plus-r : (n : nat) -> monotonic lzero lzero nat le (λ (m : nat) -> plus n m)
monotonic-le-plus-r = λ (n : nat) -> λ (a : nat) -> λ (b : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (X-- : le a b) -> le (plus X-x-365 a) (plus X-x-365 b)) (λ (auto : le a b) -> auto) (λ (m : nat) -> λ (H : (X-- : le a b) -> le (plus m a) (plus m b)) -> λ (leab : le a b) -> le-S-S (plus m a) (plus m b) (H leab)) n

monotonic-le-plus-l : (m : nat) -> monotonic lzero lzero nat le (λ (n : nat) -> plus n m)
monotonic-le-plus-l = λ (m : nat) -> λ (x : nat) -> λ (y : nat) -> λ (auto : le x y) -> eq-coerc lzero (le (plus m x) (plus m y)) (le (plus x m) (plus y m)) (monotonic-le-plus-r m x y auto) (rewrite-r lzero (lsuc lzero) nat (plus m x) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus m x) (plus m y)) (le X-- (plus y m))) (rewrite-r lzero (lsuc lzero) nat (plus m y) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus m x) (plus m y)) (le (plus m x) X--)) (refl (lsuc lzero) (Set (lzero)) (le (plus m x) (plus m y))) (plus y m) (commutative-plus y m)) (plus x m) (commutative-plus x m))

le-plus : (n1 : nat) -> (n2 : nat) -> (m1 : nat) -> (m2 : nat) -> (X-- : le n1 n2) -> (X--1 : le m1 m2) -> le (plus n1 m1) (plus n2 m2)
le-plus = λ (n1 : nat) -> λ (n2 : nat) -> λ (m1 : nat) -> λ (m2 : nat) -> λ (len : le n1 n2) -> λ (lem : le m1 m2) -> transitive-le (plus n1 m1) (plus n1 m2) (plus n2 m2) (monotonic-le-plus-r n1 m1 m2 lem) (monotonic-le-plus-l m2 n1 n2 len)

le-plus-n : (n : nat) -> (m : nat) -> le m (plus n m)
le-plus-n = λ (n : nat) -> λ (m : nat) -> eq-coerc lzero (le (plus O m) (plus n m)) (le m (plus n m)) (monotonic-le-plus-l m O n (le-O-n n)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus n m)) (le m (plus n m))) (refl (lsuc lzero) (Set (lzero)) (le m (plus n m))) (plus O m) (plus-O-n m))

le-plus-a : (a : nat) -> (n : nat) -> (m : nat) -> (X-- : le n m) -> le n (plus a m)
le-plus-a = λ (a : nat) -> λ (n : nat) -> λ (m : nat) -> λ (auto : le n m) -> eq-coerc lzero (le (plus O n) (plus a m)) (le n (plus a m)) (le-plus O a n m (le-O-n a) auto) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus a m)) (le n (plus a m))) (refl (lsuc lzero) (Set (lzero)) (le n (plus a m))) (plus O n) (plus-O-n n))

le-plus-b : (b : nat) -> (n : nat) -> (m : nat) -> (X-- : le (plus n b) m) -> le n m
le-plus-b = λ (b : nat) -> λ (n : nat) -> λ (m : nat) -> λ (auto : le (plus n b) m) -> transitive-le n (plus n b) m (eq-coerc lzero (le n (plus b n)) (le n (plus n b)) (le-plus-n b n) (rewrite-r lzero (lsuc lzero) nat (plus b n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n (plus b n)) (le n X--)) (refl (lsuc lzero) (Set (lzero)) (le n (plus b n))) (plus n b) (commutative-plus n b))) auto

le-plus-n-r : (n : nat) -> (m : nat) -> le m (plus m n)
le-plus-n-r = λ (n : nat) -> λ (m : nat) -> eq-coerc lzero (le m (plus n m)) (le m (plus m n)) (le-plus-n n m) (rewrite-r lzero (lsuc lzero) nat (plus n m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m (plus n m)) (le m X--)) (refl (lsuc lzero) (Set (lzero)) (le m (plus n m))) (plus m n) (commutative-plus m n))

eq-plus-to-le : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : eq lzero nat n (plus m p)) -> le m n
eq-plus-to-le = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (auto : eq lzero nat n (plus m p)) -> eq-coerc lzero (le m (plus m p)) (le m n) (le-plus-n-r p m) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m X--) (le m n)) (refl (lsuc lzero) (Set (lzero)) (le m n)) (plus m p) auto)

le-plus-to-le : (a : nat) -> (n : nat) -> (m : nat) -> (X-- : le (plus a n) (plus a m)) -> le n m
le-plus-to-le = λ (a : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (n : nat) -> (m : nat) -> (X-- : le (plus X-x-365 n) (plus X-x-365 m)) -> le n m) (λ (n : nat) -> λ (m : nat) -> λ (auto : le n m) -> auto) (λ (x-366 : nat) -> λ (X-x-368 : (n : nat) -> (m : nat) -> (X-- : le (plus x-366 n) (plus x-366 m)) -> le n m) -> λ (n : nat) -> λ (m : nat) -> λ (auto : le (S (plus x-366 n)) (S (plus x-366 m))) -> eq-coerc lzero (le (pred (S n)) (pred (S m))) (le n m) (monotonic-pred (S n) (S m) (X-x-368 (S n) (S m) (eq-coerc lzero (le (S (plus x-366 n)) (S (plus x-366 m))) (le (plus x-366 (S n)) (plus x-366 (S m))) auto (rewrite-r lzero (lsuc lzero) nat (plus x-366 (S n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (S (plus x-366 m))) (le (plus x-366 (S n)) (plus x-366 (S m)))) (rewrite-r lzero (lsuc lzero) nat (plus x-366 (S m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus x-366 (S n)) X--) (le (plus x-366 (S n)) (plus x-366 (S m)))) (refl (lsuc lzero) (Set (lzero)) (le (plus x-366 (S n)) (plus x-366 (S m)))) (S (plus x-366 m)) (plus-n-Sm x-366 m)) (S (plus x-366 n)) (plus-n-Sm x-366 n))))) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S m))) (le n m)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n X--) (le n m)) (refl (lsuc lzero) (Set (lzero)) (le n m)) (pred (S m)) (pred-Sn m)) (pred (S n)) (pred-Sn n))) a

le-plus-to-le-r : (a : nat) -> (n : nat) -> (m : nat) -> (X-- : le (plus n a) (plus m a)) -> le n m
le-plus-to-le-r = λ (a : nat) -> λ (n : nat) -> λ (m : nat) -> λ (auto : le (plus n a) (plus m a)) -> le-plus-to-le a n m (eq-coerc lzero (le (plus n a) (plus m a)) (le (plus a n) (plus a m)) auto (rewrite-r lzero (lsuc lzero) nat (plus a n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus m a)) (le (plus a n) (plus a m))) (rewrite-r lzero (lsuc lzero) nat (plus a m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus a n) X--) (le (plus a n) (plus a m))) (refl (lsuc lzero) (Set (lzero)) (le (plus a n) (plus a m))) (plus m a) (commutative-plus m a)) (plus n a) (commutative-plus n a)))

monotonic-le-times-r : (n : nat) -> monotonic lzero lzero nat le (λ (m : nat) -> times n m)
monotonic-le-times-r = λ (n : nat) -> λ (x : nat) -> λ (y : nat) -> λ (lexy : le x y) -> nat-ind lzero (λ (X-x-365 : nat) -> le (times X-x-365 x) (times X-x-365 y)) (le-O-n O) (λ (a : nat) -> λ (lea : le (times a x) (times a y)) -> le-plus x y (times a x) (times a y) lexy lea) n

le-times : (n1 : nat) -> (n2 : nat) -> (m1 : nat) -> (m2 : nat) -> (X-- : le n1 n2) -> (X--1 : le m1 m2) -> le (times n1 m1) (times n2 m2)
le-times = λ (n1 : nat) -> λ (n2 : nat) -> λ (m1 : nat) -> λ (m2 : nat) -> λ (len : le n1 n2) -> λ (lem : le m1 m2) -> transitive-le (times n1 m1) (times n1 m2) (times n2 m2) (monotonic-le-times-r n1 m1 m2 lem) (eq-coerc lzero (le (times m2 n1) (times m2 n2)) (le (times n1 m2) (times n2 m2)) (monotonic-le-times-r m2 n1 n2 len) (rewrite-r lzero (lsuc lzero) nat (times n1 m2) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times m2 n2)) (le (times n1 m2) (times n2 m2))) (rewrite-r lzero (lsuc lzero) nat (times n2 m2) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n1 m2) X--) (le (times n1 m2) (times n2 m2))) (refl (lsuc lzero) (Set (lzero)) (le (times n1 m2) (times n2 m2))) (times m2 n2) (commutative-times m2 n2)) (times m2 n1) (commutative-times m2 n1)))

lt-times-n : (n : nat) -> (m : nat) -> (X-- : lt O n) -> le m (times n m)
lt-times-n = λ (n : nat) -> λ (m : nat) -> λ (H : lt O n) -> eq-coerc lzero (le (times m (S O)) (times m n)) (le m (times n m)) (monotonic-le-times-r m (S O) n H) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times m n)) (le m (times n m))) (rewrite-r lzero (lsuc lzero) nat (times n m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m X--) (le m (times n m))) (refl (lsuc lzero) (Set (lzero)) (le m (times n m))) (times m n) (commutative-times m n)) (times m (S O)) (times-n-1 m))

le-times-to-le : (a : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O a) -> (X--1 : le (times a n) (times a m)) -> le n m
le-times-to-le = λ (a : nat) -> nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> (X--1 : lt O a) -> (X--2 : le (times a X--) (times a X-0)) -> le X-- X-0) (λ (n : nat) -> λ (auto : le (S O) a) -> λ (auto' : le (times a O) (times a n)) -> le-O-n n) (λ (n : nat) -> λ (H1 : le (S O) a) -> λ (H2 : le (times a (S n)) (times a O)) -> transitive-le (S n) (times a (S n)) O (eq-coerc lzero (le (times (S n) (S O)) (times (S n) a)) (le (S n) (times a (S n))) (monotonic-le-times-r (S n) (S O) a H1) (rewrite-l lzero (lsuc lzero) nat (plus a (times a n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times (S n) (S O)) (times (S n) a)) (le (S n) X--)) (rewrite-r lzero (lsuc lzero) nat (times a (S n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times (S n) (S O)) X--) (le (S n) (plus a (times a n)))) (rewrite-l lzero (lsuc lzero) nat (S n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times a (S n))) (le (S n) (plus a (times a n)))) (rewrite-l lzero (lsuc lzero) nat (plus a (times a n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S n) X--) (le (S n) (plus a (times a n)))) (refl (lsuc lzero) (Set (lzero)) (le (S n) (plus a (times a n)))) (times a (S n)) (times-n-Sm a n)) (times (S n) (S O)) (times-n-1 (S n))) (times (S n) a) (commutative-times (S n) a)) (times a (S n)) (times-n-Sm a n))) (eq-coerc lzero (le (times a (S n)) (times a O)) (le (times a (S n)) O) H2 (rewrite-l lzero (lsuc lzero) nat (plus a (times a n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times a O)) (le (times a (S n)) O)) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus a (times a n)) X--) (le (times a (S n)) O)) (rewrite-l lzero (lsuc lzero) nat (plus a (times a n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus a (times a n)) O) (le X-- O)) (refl (lsuc lzero) (Set (lzero)) (le (plus a (times a n)) O)) (times a (S n)) (times-n-Sm a n)) (times a O) (times-n-O a)) (times a (S n)) (times-n-Sm a n)))) (λ (n : nat) -> λ (m : nat) -> λ (H : (X-- : le (S O) a) -> (X--1 : le (times a n) (times a m)) -> le n m) -> λ (lta : le (S O) a) -> λ (le-v : le (times a (S n)) (times a (S m))) -> le-S-S n m (H lta (le-plus-to-le a (times a n) (times a m) (eq-coerc lzero (le (times a (S n)) (times a (S m))) (le (plus a (times a n)) (plus a (times a m))) le-v (rewrite-l lzero (lsuc lzero) nat (plus a (times a n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times a (S m))) (le (plus a (times a n)) (plus a (times a m)))) (rewrite-l lzero (lsuc lzero) nat (plus a (times a m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus a (times a n)) X--) (le (plus a (times a n)) (plus a (times a m)))) (refl (lsuc lzero) (Set (lzero)) (le (plus a (times a n)) (plus a (times a m)))) (times a (S m)) (times-n-Sm a m)) (times a (S n)) (times-n-Sm a n))))))

le-plus-minus-m-m : (n : nat) -> (m : nat) -> le n (plus (minus n m) m)
le-plus-minus-m-m = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (m : nat) -> le X-x-365 (plus (minus X-x-365 m) m)) (λ (m : nat) -> le-plus-n-r m O) (λ (a : nat) -> λ (Hind : (m : nat) -> le a (plus (minus a m) m)) -> λ (m : nat) -> match-nat lzero (λ (X-- : nat) -> le (S a) (plus (minus (S a) X--) X--)) (le-plus-n-r O (S a)) (λ (n0 : nat) -> eq-coerc lzero (le (S a) (S (plus (minus a n0) n0))) (le (S a) (plus (minus a n0) (S n0))) (le-S-S a (plus (minus a n0) n0) (Hind n0)) (rewrite-r lzero (lsuc lzero) nat (plus (minus a n0) (S n0)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S a) X--) (le (S a) (plus (minus a n0) (S n0)))) (refl (lsuc lzero) (Set (lzero)) (le (S a) (plus (minus a n0) (S n0)))) (S (plus (minus a n0) n0)) (plus-n-Sm (minus a n0) n0))) m) n

le-plus-to-minus-r : (a : nat) -> (b : nat) -> (c : nat) -> (X-- : le (plus a b) c) -> le a (minus c b)
le-plus-to-minus-r = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (H : le (plus a b) c) -> le-plus-to-le-r b a (minus c b) (transitive-le (plus a b) c (plus (minus c b) b) H (le-plus-minus-m-m c b))

lt-to-le : (x : nat) -> (y : nat) -> (X-- : lt x y) -> le x y
lt-to-le = λ (x : nat) -> λ (y : nat) -> λ (auto : lt x y) -> le-plus-b (S O) x y (eq-coerc lzero (le (S x) y) (le (plus x (S O)) y) auto (rewrite-r lzero (lsuc lzero) nat (plus x (S O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- y) (le (plus x (S O)) y)) (refl (lsuc lzero) (Set (lzero)) (le (plus x (S O)) y)) (S x) (rewrite-r lzero lzero nat (plus x O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus x (S O))) (plus-n-Sm x O) x (plus-n-O x))))

inv-eq-minus-O : (x : nat) -> (y : nat) -> (X-- : eq lzero nat (minus x y) O) -> le x y
inv-eq-minus-O = λ (x : nat) -> λ (y : nat) -> λ (auto : eq lzero nat (minus x y) O) -> eq-coerc lzero (le x (plus (minus x y) y)) (le x y) (le-plus-minus-m-m x y) (rewrite-r lzero (lsuc lzero) nat (plus y (minus x y)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le x X--) (le x y)) (rewrite-r lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le x (plus y X--)) (le x y)) (rewrite-l lzero (lsuc lzero) nat y (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le x X--) (le x y)) (refl (lsuc lzero) (Set (lzero)) (le x y)) (plus y O) (plus-n-O y)) (minus x y) auto) (plus (minus x y) y) (commutative-plus (minus x y) y))

le-x-times-x : (x : nat) -> le x (times x x)
le-x-times-x = λ (x : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> le X-x-365 (times X-x-365 X-x-365)) (le-O-n (times O O)) (λ (x-366 : nat) -> λ (X-x-368 : le x-366 (times x-366 x-366)) -> le-plus-n-r (times x-366 (S x-366)) (S x-366)) x

transitive-lt : transitive lzero lzero nat lt
transitive-lt = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (ltab : lt a b) -> λ (ltbc : lt b c) -> le-ind lzero (S b) (λ (x-417 : nat) -> λ (X-x-418 : le (S b) x-417) -> lt a x-417) (le-S (S a) b ltab) (λ (m : nat) -> λ (X-x-419 : le (S b) m) -> λ (X-x-421 : lt a m) -> le-S (S a) m X-x-421) c ltbc

lt-to-le-to-lt : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt n m) -> (X--1 : le m p) -> lt n p
lt-to-le-to-lt = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (H : lt n m) -> λ (H1 : le m p) -> le-ind lzero m (λ (x-417 : nat) -> λ (X-x-418 : le m x-417) -> lt n x-417) H (λ (m0 : nat) -> λ (X-x-419 : le m m0) -> λ (X-x-421 : lt n m0) -> transitive-lt n m0 (S m0) X-x-421 (eq-coerc lzero (le (S m0) (plus O (S m0))) (le (S m0) (S m0)) (le-plus-n O (S m0)) (rewrite-l lzero (lsuc lzero) nat (S m0) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S m0) X--) (le (S m0) (S m0))) (refl (lsuc lzero) (Set (lzero)) (le (S m0) (S m0))) (plus O (S m0)) (plus-O-n (S m0))))) p H1

le-to-lt-to-lt : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : le n m) -> (X--1 : lt m p) -> lt n p
le-to-lt-to-lt = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (H : le n m) -> le-ind lzero n (λ (x-417 : nat) -> λ (X-x-418 : le n x-417) -> (X-- : lt x-417 p) -> lt n p) (λ (auto : lt n p) -> auto) (λ (m0 : nat) -> λ (X-x-419 : le n m0) -> λ (X-x-421 : (X-- : lt m0 p) -> lt n p) -> λ (auto : lt (S m0) p) -> X-x-421 (transitive-lt m0 (S m0) p (eq-coerc lzero (le (S m0) (plus O (S m0))) (le (S m0) (S m0)) (le-plus-n O (S m0)) (rewrite-l lzero (lsuc lzero) nat (S m0) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S m0) X--) (le (S m0) (S m0))) (refl (lsuc lzero) (Set (lzero)) (le (S m0) (S m0))) (plus O (S m0)) (plus-O-n (S m0)))) auto)) m H

lt-S-to-lt : (n : nat) -> (m : nat) -> (X-- : lt (S n) m) -> lt n m
lt-S-to-lt = λ (n : nat) -> λ (m : nat) -> λ (auto : lt (S n) m) -> transitive-lt n (S n) m (eq-coerc lzero (le (S n) (plus O (S n))) (le (S n) (S n)) (le-plus-n O (S n)) (rewrite-l lzero (lsuc lzero) nat (S n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S n) X--) (le (S n) (S n))) (refl (lsuc lzero) (Set (lzero)) (le (S n) (S n))) (plus O (S n)) (plus-O-n (S n)))) auto

ltn-to-ltO : (n : nat) -> (m : nat) -> (X-- : lt n m) -> lt O m
ltn-to-ltO = λ (n : nat) -> λ (m : nat) -> λ (auto : lt n m) -> lt-to-le-to-lt O (S n) m (eq-coerc lzero (le (S O) (plus n (S O))) (le (S O) (S n)) (le-plus-n n (S O)) (rewrite-l lzero (lsuc lzero) nat (S n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S O) X--) (le (S O) (S n))) (refl (lsuc lzero) (Set (lzero)) (le (S O) (S n))) (plus n (S O)) (rewrite-r lzero lzero nat (plus n O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus n (S O))) (plus-n-Sm n O) n (plus-n-O n)))) auto

lt-O-S : (n : nat) -> lt O (S n)
lt-O-S = λ (n : nat) -> ltn-to-ltO n (S n) (eq-coerc lzero (le (S n) (plus O (S n))) (le (S n) (S n)) (le-plus-n O (S n)) (rewrite-l lzero (lsuc lzero) nat (S n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S n) X--) (le (S n) (S n))) (refl (lsuc lzero) (Set (lzero)) (le (S n) (S n))) (plus O (S n)) (plus-O-n (S n))))

monotonic-lt-plus-r : (n : nat) -> monotonic lzero lzero nat lt (λ (m : nat) -> plus n m)
monotonic-lt-plus-r = λ (n : nat) -> λ (x : nat) -> λ (y : nat) -> λ (auto : lt x y) -> eq-coerc lzero (le (plus n (S x)) (plus n y)) (le (S (plus n x)) (plus n y)) (monotonic-le-plus-r n (S x) y auto) (rewrite-r lzero (lsuc lzero) nat (plus n (S x)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus n (S x)) (plus n y)) (le X-- (plus n y))) (refl (lsuc lzero) (Set (lzero)) (le (plus n (S x)) (plus n y))) (S (plus n x)) (plus-n-Sm n x))

monotonic-lt-plus-l : (n : nat) -> monotonic lzero lzero nat lt (λ (m : nat) -> plus m n)
monotonic-lt-plus-l = λ (n : nat) -> λ (x : nat) -> λ (y : nat) -> λ (auto : lt x y) -> eq-coerc lzero (le (plus n (S x)) (plus n y)) (le (S (plus x n)) (plus y n)) (monotonic-le-plus-r n (S x) y auto) (rewrite-r lzero (lsuc lzero) nat (plus n x) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus n (S x)) (plus n y)) (le (S X--) (plus y n))) (rewrite-r lzero (lsuc lzero) nat (plus n (S x)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus n (S x)) (plus n y)) (le X-- (plus y n))) (rewrite-r lzero (lsuc lzero) nat (plus n y) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus n (S x)) (plus n y)) (le (plus n (S x)) X--)) (refl (lsuc lzero) (Set (lzero)) (le (plus n (S x)) (plus n y))) (plus y n) (commutative-plus y n)) (S (plus n x)) (plus-n-Sm n x)) (plus x n) (commutative-plus x n))

lt-plus : (n : nat) -> (m : nat) -> (p : nat) -> (q : nat) -> (X-- : lt n m) -> (X--1 : lt p q) -> lt (plus n p) (plus m q)
lt-plus = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (q : nat) -> λ (ltnm : lt n m) -> λ (ltpq : lt p q) -> transitive-lt (plus n p) (plus n q) (plus m q) (eq-coerc lzero (le (plus n (S p)) (plus n q)) (le (S (plus n p)) (plus n q)) (monotonic-le-plus-r n (S p) q ltpq) (rewrite-r lzero (lsuc lzero) nat (plus n (S p)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus n (S p)) (plus n q)) (le X-- (plus n q))) (refl (lsuc lzero) (Set (lzero)) (le (plus n (S p)) (plus n q))) (S (plus n p)) (plus-n-Sm n p))) (monotonic-lt-plus-l q n m ltnm)

lt-plus-to-lt-l : (n : nat) -> (p : nat) -> (q : nat) -> (X-- : lt (plus p n) (plus q n)) -> lt p q
lt-plus-to-lt-l = λ (n : nat) -> λ (p : nat) -> λ (q : nat) -> λ (auto : lt (plus p n) (plus q n)) -> le-plus-to-le n (S p) q (eq-coerc lzero (le (S (plus p n)) (plus q n)) (le (plus n (S p)) (plus n q)) auto (rewrite-r lzero (lsuc lzero) nat (plus n p) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S X--) (plus q n)) (le (plus n (S p)) (plus n q))) (rewrite-r lzero (lsuc lzero) nat (plus n (S p)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus q n)) (le (plus n (S p)) (plus n q))) (rewrite-r lzero (lsuc lzero) nat (plus n q) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus n (S p)) X--) (le (plus n (S p)) (plus n q))) (refl (lsuc lzero) (Set (lzero)) (le (plus n (S p)) (plus n q))) (plus q n) (commutative-plus q n)) (S (plus n p)) (plus-n-Sm n p)) (plus p n) (commutative-plus p n)))

lt-plus-to-lt-r : (n : nat) -> (p : nat) -> (q : nat) -> (X-- : lt (plus n p) (plus n q)) -> lt p q
lt-plus-to-lt-r = λ (n : nat) -> λ (p : nat) -> λ (q : nat) -> λ (auto : lt (plus n p) (plus n q)) -> lt-plus-to-lt-l n p q (eq-coerc lzero (lt (plus n p) (plus n q)) (lt (plus p n) (plus q n)) auto (rewrite-r lzero (lsuc lzero) nat (plus p n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus n q)) (lt (plus p n) (plus q n))) (rewrite-r lzero (lsuc lzero) nat (plus q n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus p n) X--) (lt (plus p n) (plus q n))) (refl (lsuc lzero) (Set (lzero)) (lt (plus p n) (plus q n))) (plus n q) (commutative-plus n q)) (plus n p) (commutative-plus n p)))

increasing-to-monotonic : (f : (X-- : nat) -> nat) -> (X-- : increasing f) -> monotonic lzero lzero nat lt f
increasing-to-monotonic = λ (f : (X-- : nat) -> nat) -> λ (incr : increasing f) -> λ (n : nat) -> λ (m : nat) -> λ (ltnm : lt n m) -> le-ind lzero (S n) (λ (x-417 : nat) -> λ (X-x-418 : le (S n) x-417) -> lt (f n) (f x-417)) (incr n) (λ (m0 : nat) -> λ (X-x-419 : le (S n) m0) -> λ (X-x-421 : lt (f n) (f m0)) -> transitive-lt (f n) (f m0) (f (S m0)) X-x-421 (incr m0)) m ltnm

monotonic-lt-times-r : (c : nat) -> (X-- : lt O c) -> monotonic lzero lzero nat lt (λ (t : nat) -> times c t)
monotonic-lt-times-r = λ (c : nat) -> λ (posc : lt O c) -> λ (n : nat) -> λ (m : nat) -> λ (ltnm : lt n m) -> le-ind lzero (S n) (λ (x-417 : nat) -> λ (X-x-418 : le (S n) x-417) -> lt (times c n) (times c x-417)) (eq-coerc lzero (le (S (plus O (times c n))) (plus c (times c n))) (le (S (times c n)) (times c (S n))) (monotonic-lt-plus-l (times c n) O c posc) (rewrite-r lzero (lsuc lzero) nat (plus O (S (times c n))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus c (times c n))) (le (S (times c n)) (times c (S n)))) (rewrite-l lzero (lsuc lzero) nat (plus c (times c n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus O (S (times c n))) (plus c (times c n))) (le (S (times c n)) X--)) (rewrite-l lzero (lsuc lzero) nat (S (times c n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus c (times c n))) (le (S (times c n)) (plus c (times c n)))) (refl (lsuc lzero) (Set (lzero)) (le (S (times c n)) (plus c (times c n)))) (plus O (S (times c n))) (plus-O-n (S (times c n)))) (times c (S n)) (times-n-Sm c n)) (S (plus O (times c n))) (plus-n-Sm O (times c n)))) (λ (a : nat) -> λ (X-- : le (S n) a) -> λ (lt1 : le (S (times c n)) (times c a)) -> transitive-le (S (times c n)) (times c a) (times c (S a)) lt1 (eq-coerc lzero (le (times c a) (plus (times c a) c)) (le (times c a) (times c (S a))) (le-plus-n-r c (times c a)) (rewrite-l lzero (lsuc lzero) nat (plus c (times c a)) (λ (X--1 : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times c a) (plus (times c a) c)) (le (times c a) X--1)) (rewrite-r lzero (lsuc lzero) nat (plus c (times c a)) (λ (X--1 : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times c a) X--1) (le (times c a) (plus c (times c a)))) (refl (lsuc lzero) (Set (lzero)) (le (times c a) (plus c (times c a)))) (plus (times c a) c) (commutative-plus (times c a) c)) (times c (S a)) (times-n-Sm c a)))) m ltnm

monotonic-lt-times-l : (c : nat) -> (X-- : lt O c) -> monotonic lzero lzero nat lt (λ (t : nat) -> times t c)
monotonic-lt-times-l = λ (c : nat) -> λ (auto : lt O c) -> λ (x : nat) -> λ (y : nat) -> λ (auto' : lt x y) -> eq-coerc lzero (le (S (times c x)) (times c y)) (le (S (times x c)) (times y c)) (monotonic-lt-times-r c auto x y auto') (rewrite-r lzero (lsuc lzero) nat (times c x) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (times c x)) (times c y)) (le (S X--) (times y c))) (rewrite-r lzero (lsuc lzero) nat (times c y) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S (times c x)) (times c y)) (le (S (times c x)) X--)) (refl (lsuc lzero) (Set (lzero)) (le (S (times c x)) (times c y))) (times y c) (commutative-times y c)) (times x c) (commutative-times x c))

lt-to-le-to-lt-times : (n : nat) -> (m : nat) -> (p : nat) -> (q : nat) -> (X-- : lt n m) -> (X--1 : le p q) -> (X--2 : lt O q) -> lt (times n p) (times m q)
lt-to-le-to-lt-times = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (q : nat) -> λ (ltnm : lt n m) -> λ (lepq : le p q) -> λ (posq : lt O q) -> le-to-lt-to-lt (times n p) (times n q) (times m q) (monotonic-le-times-r n p q lepq) (monotonic-lt-times-l q posq n m ltnm)

lt-times : (n : nat) -> (m : nat) -> (p : nat) -> (q : nat) -> (X-- : lt n m) -> (X--1 : lt p q) -> lt (times n p) (times m q)
lt-times = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (q : nat) -> λ (ltnm : lt n m) -> λ (ltpq : lt p q) -> lt-to-le-to-lt-times n m p q ltnm (lt-to-le p q ltpq) (ltn-to-ltO p q ltpq)

lt-plus-to-minus-r : (a : nat) -> (b : nat) -> (c : nat) -> (X-- : lt (plus a b) c) -> lt a (minus c b)
lt-plus-to-minus-r = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (H : lt (plus a b) c) -> le-plus-to-minus-r (S a) b c H

lt-plus-Sn-r : (a : nat) -> (x : nat) -> (n : nat) -> lt a (plus (plus a x) (S n))
lt-plus-Sn-r = λ (a : nat) -> λ (x : nat) -> λ (n : nat) -> eq-coerc lzero (le (S a) (S (plus (plus a x) n))) (le (S a) (plus (plus a x) (S n))) (le-S-S a (plus (plus a x) n) (eq-coerc lzero (le a (plus a (plus x n))) (le a (plus (plus a x) n)) (le-plus-n-r (plus x n) a) (rewrite-r lzero (lsuc lzero) nat (plus n (plus a x)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le a (plus a (plus x n))) (le a X--)) (rewrite-r lzero (lsuc lzero) nat (plus a (plus n x)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le a (plus a (plus x n))) (le a X--)) (rewrite-r lzero (lsuc lzero) nat (plus x n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le a (plus a (plus x n))) (le a (plus a X--))) (refl (lsuc lzero) (Set (lzero)) (le a (plus a (plus x n)))) (plus n x) (commutative-plus n x)) (plus n (plus a x)) (rewrite-l lzero lzero nat (plus (plus a n) x) (λ (X-- : nat) -> eq lzero nat (plus n (plus a x)) X--) (assoc-plus1 x a n) (plus a (plus n x)) (associative-plus a n x))) (plus (plus a x) n) (commutative-plus (plus a x) n)))) (rewrite-r lzero (lsuc lzero) nat (plus a (plus x (S n))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S a) (S (plus (plus a x) n))) (le (S a) X--)) (rewrite-r lzero (lsuc lzero) nat (plus (plus a x) (S n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S a) X--) (le (S a) (plus a (plus x (S n))))) (rewrite-r lzero (lsuc lzero) nat (plus a (plus x (S n))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S a) X--) (le (S a) (plus a (plus x (S n))))) (refl (lsuc lzero) (Set (lzero)) (le (S a) (plus a (plus x (S n))))) (plus (plus a x) (S n)) (associative-plus a x (S n))) (S (plus (plus a x) n)) (plus-n-Sm (plus a x) n)) (plus (plus a x) (S n)) (associative-plus a x (S n)))

let-clause-16 : (n : nat) -> (m : nat) -> (auto : lt (S n) (S m)) -> (x32 : nat) -> eq lzero nat (S x32) (plus x32 (S O))
let-clause-16 = λ (n : nat) -> λ (m : nat) -> λ (auto : lt (S n) (S m)) -> λ (x32 : nat) -> rewrite-r lzero lzero nat (plus x32 O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus x32 (S O))) (plus-n-Sm x32 O) x32 (plus-n-O x32)

lt-S-S-to-lt : (n : nat) -> (m : nat) -> (X-- : lt (S n) (S m)) -> lt n m
lt-S-S-to-lt = λ (n : nat) -> λ (m : nat) -> λ (auto : lt (S n) (S m)) -> lt-plus-to-lt-l (S O) n m (eq-coerc lzero (lt (S n) (S m)) (lt (plus n (S O)) (plus m (S O))) auto (rewrite-r lzero (lsuc lzero) nat (plus n (S O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (S m)) (lt (plus n (S O)) (plus m (S O)))) (rewrite-r lzero (lsuc lzero) nat (plus m (S O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus n (S O)) X--) (lt (plus n (S O)) (plus m (S O)))) (refl (lsuc lzero) (Set (lzero)) (lt (plus n (S O)) (plus m (S O)))) (S m) (let-clause-16 n m auto m)) (S n) (let-clause-16 n m auto n)))

not-le-Sn-O : (n : nat) -> Not lzero (le (S n) O)
not-le-Sn-O = λ (n : nat) -> nmk lzero (le (S n) O) (λ (Hlen0 : le (S n) O) -> lt-to-not-zero lzero n O Hlen0)

not-le-to-not-le-S-S : (n : nat) -> (m : nat) -> (X-- : Not lzero (le n m)) -> Not lzero (le (S n) (S m))
not-le-to-not-le-S-S = λ (n : nat) -> λ (m : nat) -> λ (auto : Not lzero (le n m)) -> not-to-not lzero (le (S n) (S m)) (le n m) (λ (auto' : le (S n) (S m)) -> eq-coerc lzero (le (pred (S n)) (pred (S m))) (le n m) (monotonic-pred (S n) (S m) auto') (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S m))) (le n m)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n X--) (le n m)) (refl (lsuc lzero) (Set (lzero)) (le n m)) (pred (S m)) (pred-Sn m)) (pred (S n)) (pred-Sn n))) auto

not-le-S-S-to-not-le : (n : nat) -> (m : nat) -> (X-- : Not lzero (le (S n) (S m))) -> Not lzero (le n m)
not-le-S-S-to-not-le = λ (n : nat) -> λ (m : nat) -> λ (auto : Not lzero (le (S n) (S m))) -> not-to-not lzero (le n m) (le (S n) (S m)) (λ (auto' : le n m) -> le-S-S n m auto') auto

not-le-Sn-n : (n : nat) -> Not lzero (le (S n) n)
not-le-Sn-n = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> Not lzero (le (S X-x-365) X-x-365)) (not-le-Sn-O O) (λ (x-366 : nat) -> λ (X-x-368 : Not lzero (le (S x-366) x-366)) -> not-le-to-not-le-S-S (S x-366) x-366 X-x-368) n

lt-to-not-le : (n : nat) -> (m : nat) -> (X-- : lt n m) -> Not lzero (le m n)
lt-to-not-le = λ (n : nat) -> λ (m : nat) -> λ (Hltnm : lt n m) -> le-ind lzero (S n) (λ (x-417 : nat) -> λ (X-x-418 : le (S n) x-417) -> Not lzero (le x-417 n)) (not-le-Sn-n n) (λ (m0 : nat) -> λ (X-x-419 : le (S n) m0) -> λ (X-x-421 : Not lzero (le m0 n)) -> not-to-not lzero (le (S m0) n) (le m0 n) (λ (auto : le (S m0) n) -> lt-to-le m0 n auto) X-x-421) m Hltnm

not-le-to-lt : (n : nat) -> (m : nat) -> (X-- : Not lzero (le n m)) -> lt m n
not-le-to-lt = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> (X--1 : Not lzero (le X-- X-0)) -> lt X-0 X--) (λ (n : nat) -> λ (abs : Not lzero (le O n)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt n O) (absurd lzero (le O n) (eq-coerc lzero (le O (plus n O)) (le O n) (le-plus-n n O) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le O X--) (le O n)) (refl (lsuc lzero) (Set (lzero)) (le O n)) (plus n O) (plus-n-O n))) abs)) (λ (n : nat) -> λ (auto : Not lzero (le (S n) O)) -> lt-O-S n) (λ (n : nat) -> λ (m : nat) -> λ (Hind : (X-- : Not lzero (le n m)) -> lt m n) -> λ (HnotleSS : Not lzero (le (S n) (S m))) -> le-S-S (S m) n (Hind (not-le-S-S-to-not-le n m HnotleSS)))

not-lt-to-le : (n : nat) -> (m : nat) -> (X-- : Not lzero (lt n m)) -> le m n
not-lt-to-le = λ (n : nat) -> λ (m : nat) -> λ (H : Not lzero (lt n m)) -> le-S-S-to-le m n (not-le-to-lt (S n) m (not-to-not lzero (le (S n) m) (lt n m) (λ (auto : le (S n) m) -> auto) H))

le-to-not-lt : (n : nat) -> (m : nat) -> (X-- : le n m) -> Not lzero (lt m n)
le-to-not-lt = λ (n : nat) -> λ (m : nat) -> λ (H : le n m) -> lt-to-not-le n (S m) (le-to-lt-to-lt n m (S m) H (eq-coerc lzero (le (S m) (plus O (S m))) (le (S m) (S m)) (le-plus-n O (S m)) (rewrite-l lzero (lsuc lzero) nat (S m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S m) X--) (le (S m) (S m))) (refl (lsuc lzero) (Set (lzero)) (le (S m) (S m))) (plus O (S m)) (plus-O-n (S m)))))

decidable-eq-nat : (n : nat) -> (m : nat) -> decidable lzero (eq lzero nat n m)
decidable-eq-nat = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> decidable lzero (eq lzero nat X-- X-0)) (λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> decidable lzero (eq lzero nat O X--)) (or-introl lzero lzero (eq lzero nat O O) (Not lzero (eq lzero nat O O)) (refl lzero nat O)) (λ (auto : nat) -> or-intror lzero lzero (eq lzero nat O (S auto)) (Not lzero (eq lzero nat O (S auto))) (not-eq-O-S auto)) n) (λ (n : nat) -> or-intror lzero lzero (eq lzero nat (S n) O) (Not lzero (eq lzero nat (S n) O)) (sym-not-eq lzero nat O (S n) (not-eq-O-S n))) (λ (n : nat) -> λ (m : nat) -> λ (Hind : decidable lzero (eq lzero nat n m)) -> match-Or lzero lzero (eq lzero nat n m) (Not lzero (eq lzero nat n m)) lzero (λ (X-- : Or lzero lzero (eq lzero nat n m) (Not lzero (eq lzero nat n m))) -> decidable lzero (eq lzero nat (S n) (S m))) (λ (auto : eq lzero nat n m) -> or-introl lzero lzero (eq lzero nat (S n) (S m)) (Not lzero (eq lzero nat (S n) (S m))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (S n) (S X--)) (refl lzero nat (S n)) m auto)) (λ (auto : Not lzero (eq lzero nat n m)) -> or-intror lzero lzero (eq lzero nat (S n) (S m)) (Not lzero (eq lzero nat (S n) (S m))) (not-eq-S n m auto)) Hind)

decidable-le : (n : nat) -> (m : nat) -> decidable lzero (le n m)
decidable-le = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> decidable lzero (le X-- X-0)) (λ (n : nat) -> or-introl lzero lzero (le O n) (Not lzero (le O n)) (le-O-n n)) (λ (n : nat) -> or-intror lzero lzero (le (S n) O) (Not lzero (le (S n) O)) (not-le-Sn-O n)) (λ (n : nat) -> λ (m : nat) -> λ (X-clearme : decidable lzero (le n m)) -> match-Or lzero lzero (le n m) (Not lzero (le n m)) lzero (λ (X-- : Or lzero lzero (le n m) (Not lzero (le n m))) -> decidable lzero (le (S n) (S m))) (λ (auto : le n m) -> or-introl lzero lzero (le (S n) (S m)) (Not lzero (le (S n) (S m))) (le-S-S n m auto)) (λ (auto : Not lzero (le n m)) -> or-intror lzero lzero (le (S n) (S m)) (Not lzero (le (S n) (S m))) (not-le-to-not-le-S-S n m auto)) X-clearme)

decidable-lt : (n : nat) -> (m : nat) -> decidable lzero (lt n m)
decidable-lt = λ (n : nat) -> λ (m : nat) -> decidable-le (S n) m

le-to-or-lt-eq : (n : nat) -> (m : nat) -> (X-- : le n m) -> Or lzero lzero (lt n m) (eq lzero nat n m)
le-to-or-lt-eq = λ (n : nat) -> λ (m : nat) -> λ (lenm : le n m) -> le-ind lzero n (λ (x-417 : nat) -> λ (X-x-418 : le n x-417) -> Or lzero lzero (lt n x-417) (eq lzero nat n x-417)) (RC-reflexive lzero lzero nat lt n) (λ (m0 : nat) -> λ (X-x-419 : le n m0) -> λ (X-x-421 : Or lzero lzero (lt n m0) (eq lzero nat n m0)) -> or-introl lzero lzero (lt n (S m0)) (eq lzero nat n (S m0)) (le-to-lt-to-lt n m0 (S m0) X-x-419 (eq-coerc lzero (le (S m0) (plus O (S m0))) (le (S m0) (S m0)) (le-plus-n O (S m0)) (rewrite-l lzero (lsuc lzero) nat (S m0) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S m0) X--) (le (S m0) (S m0))) (refl (lsuc lzero) (Set (lzero)) (le (S m0) (S m0))) (plus O (S m0)) (plus-O-n (S m0)))))) m lenm

eq-or-gt : (n : nat) -> Or lzero lzero (eq lzero nat O n) (lt O n)
eq-or-gt = λ (n : nat) -> Or-ind lzero lzero lzero (lt O n) (eq lzero nat O n) (λ (X-x-170 : Or lzero lzero (lt O n) (eq lzero nat O n)) -> Or lzero lzero (eq lzero nat O n) (lt O n)) (λ (X-x-171 : lt O n) -> or-intror lzero lzero (eq lzero nat O n) (lt O n) X-x-171) (λ (X-x-172 : eq lzero nat O n) -> or-introl lzero lzero (eq lzero nat O n) (lt O n) (rewrite-r lzero lzero nat n (λ (X-- : nat) -> eq lzero nat X-- n) (refl lzero nat n) O X-x-172)) (le-to-or-lt-eq O n (le-O-n n))

increasing-to-le2 : (f : (X-- : nat) -> nat) -> (X-- : increasing f) -> (m : nat) -> (X--1 : le (f O) m) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) m) (lt m (f (S i))))
increasing-to-le2 = λ (f : (X-- : nat) -> nat) -> λ (incr : increasing f) -> λ (m : nat) -> λ (lem : le (f O) m) -> le-ind lzero (f O) (λ (x-417 : nat) -> λ (X-x-418 : le (f O) x-417) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) x-417) (lt x-417 (f (S i))))) (ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) (f O)) (lt (f O) (f (S i)))) O (conj lzero lzero (le (f O) (f O)) (lt (f O) (f (S O))) (le-n (f O)) (incr O))) (λ (n : nat) -> λ (len : le (f O) n) -> λ (X-clearme : ex lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) n) (lt n (f (S i))))) -> match-ex lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) n) (lt n (f (S i)))) lzero (λ (X-- : ex lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) n) (lt n (f (S i))))) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) (S n)) (lt (S n) (f (S i))))) (λ (a : nat) -> λ (X-clearme0 : And lzero lzero (le (f a) n) (lt n (f (S a)))) -> match-And lzero lzero (le (f a) n) (lt n (f (S a))) lzero (λ (X-- : And lzero lzero (le (f a) n) (lt n (f (S a)))) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) (S n)) (lt (S n) (f (S i))))) (λ (len0 : le (f a) n) -> λ (ltnr : lt n (f (S a))) -> match-Or lzero lzero (lt (S n) (f (S a))) (eq lzero nat (S n) (f (S a))) lzero (λ (X-- : Or lzero lzero (lt (S n) (f (S a))) (eq lzero nat (S n) (f (S a)))) -> ex lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) (S n)) (lt (S n) (f (S i))))) (λ (H : lt (S n) (f (S a))) -> ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) (S n)) (lt (S n) (f (S i)))) a (conj lzero lzero (le (f a) (S n)) (lt (S n) (f (S a))) (le-S (f a) n len0) H)) (λ (H : eq lzero nat (S n) (f (S a))) -> ex-intro lzero lzero nat (λ (i : nat) -> And lzero lzero (le (f i) (S n)) (lt (S n) (f (S i)))) (S a) (conj lzero lzero (le (f (S a)) (S n)) (lt (S n) (f (S (S a)))) (eq-coerc lzero (le (S n) (S n)) (le (f (S a)) (S n)) (le-n (S n)) (rewrite-l lzero (lsuc lzero) nat (S n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S n) (S n)) (le X-- (S n))) (refl (lsuc lzero) (Set (lzero)) (le (S n) (S n))) (f (S a)) H)) (eq-coerc lzero (lt (f (S a)) (f (S (S a)))) (lt (S n) (f (S (S a)))) (incr (S a)) (rewrite-l lzero (lsuc lzero) nat (S n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (f (S (S a)))) (lt (S n) (f (S (S a))))) (refl (lsuc lzero) (Set (lzero)) (lt (S n) (f (S (S a))))) (f (S a)) H)))) (le-to-or-lt-eq (S n) (f (S a)) ltnr)) X-clearme0) X-clearme) m lem

le-inv-plus-l : (x : nat) -> (y : nat) -> (z : nat) -> (X-- : le (plus x y) z) -> And lzero lzero (le x (minus z y)) (le y z)
le-inv-plus-l = λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> λ (auto : le (plus x y) z) -> conj lzero lzero (le x (minus z y)) (le y z) (le-plus-to-minus-r x y z auto) (le-plus-b x y z (eq-coerc lzero (le (plus x y) z) (le (plus y x) z) auto (rewrite-r lzero (lsuc lzero) nat (plus y x) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- z) (le (plus y x) z)) (refl (lsuc lzero) (Set (lzero)) (le (plus y x) z)) (plus x y) (commutative-plus x y))))

lt-inv-plus-l : (x : nat) -> (y : nat) -> (z : nat) -> (X-- : lt (plus x y) z) -> And lzero lzero (lt x z) (lt y (minus z x))
lt-inv-plus-l = λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> λ (auto : lt (plus x y) z) -> conj lzero lzero (lt x z) (lt y (minus z x)) (lt-to-le-to-lt x (S (plus x y)) z (eq-coerc lzero (lt x (plus (plus x O) (S y))) (lt x (S (plus x y))) (lt-plus-Sn-r x O y) (rewrite-r lzero (lsuc lzero) nat (plus x (plus O (S y))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt x X--) (lt x (S (plus x y)))) (rewrite-r lzero (lsuc lzero) nat (plus x (S y)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt x (plus x (plus O (S y)))) (lt x X--)) (rewrite-l lzero (lsuc lzero) nat (S y) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt x (plus x X--)) (lt x (plus x (S y)))) (refl (lsuc lzero) (Set (lzero)) (lt x (plus x (S y)))) (plus O (S y)) (plus-O-n (S y))) (S (plus x y)) (plus-n-Sm x y)) (plus (plus x O) (S y)) (associative-plus x O (S y)))) auto) (lt-plus-to-minus-r y x z (eq-coerc lzero (lt (plus x y) z) (lt (plus y x) z) auto (rewrite-r lzero (lsuc lzero) nat (plus x y) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus x y) z) (lt X-- z)) (refl (lsuc lzero) (Set (lzero)) (lt (plus x y) z)) (plus y x) (commutative-plus y x))))

lt-or-ge : (m : nat) -> (n : nat) -> Or lzero lzero (lt m n) (le n m)
lt-or-ge = λ (m : nat) -> λ (n : nat) -> Or-ind lzero lzero lzero (lt m n) (Not lzero (lt m n)) (λ (X-x-170 : Or lzero lzero (lt m n) (Not lzero (lt m n))) -> Or lzero lzero (lt m n) (le n m)) (λ (X-x-171 : lt m n) -> or-introl lzero lzero (lt m n) (le n m) X-x-171) (λ (X-x-172 : Not lzero (lt m n)) -> or-intror lzero lzero (lt m n) (le n m) (not-lt-to-le m n X-x-172)) (decidable-lt m n)

le-or-ge : (m : nat) -> (n : nat) -> Or lzero lzero (le m n) (le n m)
le-or-ge = λ (m : nat) -> λ (n : nat) -> Or-ind lzero lzero lzero (le m n) (Not lzero (le m n)) (λ (X-x-170 : Or lzero lzero (le m n) (Not lzero (le m n))) -> Or lzero lzero (le m n) (le n m)) (λ (X-x-171 : le m n) -> or-introl lzero lzero (le m n) (le n m) X-x-171) (λ (X-x-172 : Not lzero (le m n)) -> or-intror lzero lzero (le m n) (le n m) (lt-to-le n m (not-le-to-lt m n X-x-172))) (decidable-le m n)

le-inv-S1 : (x : nat) -> (y : nat) -> (X-- : le (S x) y) -> ex2 lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat y (S z))
le-inv-S1 = λ (x : nat) -> λ (y : nat) -> λ (H : le (S x) y) -> le-ind lzero (S x) (λ (x-417 : nat) -> λ (X-x-418 : le (S x) x-417) -> ex2 lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat x-417 (S z))) (ex2-intro lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat (S x) (S z)) x (eq-coerc lzero (le x (plus O x)) (le x x) (le-plus-n O x) (rewrite-l lzero (lsuc lzero) nat x (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le x X--) (le x x)) (refl (lsuc lzero) (Set (lzero)) (le x x)) (plus O x) (plus-O-n x))) (refl lzero nat (S x))) (λ (y0 : nat) -> λ (X-- : le (S x) y0) -> λ (X-clearme : ex2 lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat y0 (S z))) -> match-ex2 lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat y0 (S z)) lzero (λ (X-0 : ex2 lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat y0 (S z))) -> ex2 lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat (S y0) (S z))) (λ (n : nat) -> λ (Hxn : le x n) -> λ (H0 : eq lzero nat y0 (S n)) -> eq-ind-r lzero lzero nat (S n) (λ (x0 : nat) -> λ (X-0 : eq lzero nat x0 (S n)) -> ex2 lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat (S x0) (S z))) (ex2-intro lzero lzero lzero nat (λ (z : nat) -> le x z) (λ (z : nat) -> eq lzero nat (S (S n)) (S z)) (S n) (le-S x n Hxn) (refl lzero nat (S (S n)))) y0 H0) X-clearme) y H

nat-ind-plus : (l20 : Level) -> (R : predicate lzero l20 nat) -> (X-- : R O) -> (X--1 : (n : nat) -> (X--1 : R n) -> R (plus n (S O))) -> (n : nat) -> R n
nat-ind-plus = λ (l20 : Level) -> λ (R : predicate lzero l20 nat) -> λ (auto : R O) -> λ (auto' : (n : nat) -> (X-- : R n) -> R (plus n (S O))) -> λ (n : nat) -> nat-ind l20 R auto (λ (x-366 : nat) -> λ (X-x-368 : R x-366) -> eq-coerc l20 (R (plus x-366 (S O))) (R (S x-366)) (auto' x-366 X-x-368) (rewrite-l lzero ((lsuc lzero) ⊔ (lsuc l20)) nat (S x-366) (λ (X-- : nat) -> eq ((lsuc lzero) ⊔ (lsuc l20)) (Set l20) (R X--) (R (S x-366))) (refl ((lsuc lzero) ⊔ (lsuc l20)) (Set l20) (R (S x-366))) (plus x-366 (S O)) (rewrite-r lzero lzero nat (plus x-366 O) (λ (X-- : nat) -> eq lzero nat (S X--) (plus x-366 (S O))) (plus-n-Sm x-366 O) x-366 (plus-n-O x-366)))) n

lt-O-n-elim : (l13 : Level) -> (n : nat) -> (X-- : lt O n) -> (P : (X--1 : nat) -> Set l13) -> (X--1 : (m : nat) -> P (S m)) -> P n
lt-O-n-elim = λ (l13 : Level) -> λ (n : nat) -> nat-ind ((lsuc lzero) ⊔ (lsuc l13)) (λ (X-x-365 : nat) -> (X-- : lt O X-x-365) -> (P : (X--1 : nat) -> Set l13) -> (X--1 : (m : nat) -> P (S m)) -> P X-x-365) (λ (abs : lt O O) -> False-ind lzero ((lsuc lzero) ⊔ (lsuc l13)) (λ (X-x-66 : False lzero) -> (P : (X-- : nat) -> Set l13) -> (X-- : (m : nat) -> P (S m)) -> P O) (absurd lzero (le (S O) O) abs (not-le-Sn-O O))) (λ (x-366 : nat) -> λ (X-x-368 : (X-- : lt O x-366) -> (P : (X--1 : nat) -> Set l13) -> (X--1 : (m : nat) -> P (S m)) -> P x-366) -> λ (auto : lt O (S x-366)) -> λ (P : (X-- : nat) -> Set l13) -> λ (auto' : (m : nat) -> P (S m)) -> auto' x-366) n

le-n-O-elim : (l9 : Level) -> (n : nat) -> (X-- : le n O) -> (P : (X--1 : nat) -> Set l9) -> (X--1 : P O) -> P n
le-n-O-elim = λ (l9 : Level) -> λ (n : nat) -> match-nat ((lsuc lzero) ⊔ (lsuc l9)) (λ (X-- : nat) -> (X--1 : le X-- O) -> (P : (X--2 : nat) -> Set l9) -> (X--2 : P O) -> P X--) (λ (auto : le O O) -> λ (P : (X-- : nat) -> Set l9) -> λ (auto' : P O) -> auto') (λ (a : nat) -> λ (abs : le (S a) O) -> False-ind lzero ((lsuc lzero) ⊔ (lsuc l9)) (λ (X-x-66 : False lzero) -> (P : (X-- : nat) -> Set l9) -> (X-- : P O) -> P (S a)) (absurd lzero (le (S a) O) abs (not-le-Sn-O a))) n

le-n-Sm-elim : (l39 : Level) -> (n : nat) -> (m : nat) -> (X-- : le n (S m)) -> (P : Set l39) -> (X--1 : (X--1 : le (S n) (S m)) -> P) -> (X--2 : (X--2 : eq lzero nat n (S m)) -> P) -> P
le-n-Sm-elim = λ (l39 : Level) -> λ (n : nat) -> λ (m : nat) -> λ (Hle : le n (S m)) -> λ (P : Set l39) -> le-ind l39 n (λ (x-417 : nat) -> λ (X-x-418 : le n x-417) -> (X-- : (X-- : le (S n) x-417) -> P) -> (X--1 : (X--1 : eq lzero nat n x-417) -> P) -> P) (λ (auto : (X-- : le (S n) n) -> P) -> λ (auto' : (X-- : eq lzero nat n n) -> P) -> auto' (refl lzero nat n)) (λ (m0 : nat) -> λ (X-x-419 : le n m0) -> λ (X-x-421 : (X-- : (X-- : le (S n) m0) -> P) -> (X--1 : (X--1 : eq lzero nat n m0) -> P) -> P) -> λ (auto : (X-- : le (S n) (S m0)) -> P) -> λ (auto' : (X-- : eq lzero nat n (S m0)) -> P) -> auto (le-S-S n m0 X-x-419)) (S m) Hle

nat-elim1 : (l31 : Level) -> (n : nat) -> (P : (X-- : nat) -> Set l31) -> (X-- : (m : nat) -> (X-- : (p : nat) -> (X-- : lt p m) -> P p) -> P m) -> P n
nat-elim1 = λ (l31 : Level) -> λ (n : nat) -> λ (P : (X-- : nat) -> Set l31) -> λ (H : (m : nat) -> (X-- : (p : nat) -> (X-- : lt p m) -> P p) -> P m) -> nat-ind l31 (λ (X-x-365 : nat) -> (q : nat) -> (X-- : le q X-x-365) -> P q) (λ (q : nat) -> λ (HleO : le q O) -> le-n-O-elim l31 q HleO P (H O (λ (p : nat) -> λ (ltpO : lt p O) -> False-ind lzero l31 (λ (X-x-66 : False lzero) -> P p) (absurd lzero (le (S p) O) ltpO (not-le-Sn-O p))))) (λ (p : nat) -> λ (Hind : (q : nat) -> (X-- : le q p) -> P q) -> λ (q : nat) -> λ (HleS : le q (S p)) -> H q (λ (a : nat) -> λ (lta : lt a q) -> Hind a (le-S-S-to-le a p (transitive-le (S a) q (S p) lta HleS)))) n n (le-n n)

f-ind-aux : (l42 l37 : Level) -> (A : Set l42) -> (f : (X-- : A) -> nat) -> (P : predicate l42 l37 A) -> (X-- : (n : nat) -> (X-- : (a : A) -> (X-- : lt (f a) n) -> P a) -> (a : A) -> (X--1 : eq lzero nat (f a) n) -> P a) -> (n : nat) -> (a : A) -> (X--1 : eq lzero nat (f a) n) -> P a
f-ind-aux = λ (l42 l37 : Level) -> λ (A : Set l42) -> λ (f : (X-- : A) -> nat) -> λ (P : predicate l42 l37 A) -> λ (H : (n : nat) -> (X-- : (a : A) -> (X-- : lt (f a) n) -> P a) -> (a : A) -> (X--1 : eq lzero nat (f a) n) -> P a) -> λ (n : nat) -> nat-elim1 (l42 ⊔ l37) n (λ (X-- : nat) -> (a : A) -> (X--1 : eq lzero nat (f a) X--) -> P a) (λ (n0 : nat) -> λ (auto : (p : nat) -> (X-- : lt p n0) -> (a : A) -> (X--1 : eq lzero nat (f a) p) -> P a) -> λ (a : A) -> λ (auto' : eq lzero nat (f a) n0) -> H n0 (λ (a0 : A) -> λ (auto'' : lt (f a0) n0) -> auto (f a0) auto'' a0 (refl lzero nat (f a0))) a (rewrite-r lzero lzero nat n0 (λ (X-- : nat) -> eq lzero nat X-- n0) (refl lzero nat n0) (f a) auto'))

f-ind : (l17 l12 : Level) -> (A : Set l17) -> (f : (X-- : A) -> nat) -> (P : predicate l17 l12 A) -> (X-- : (n : nat) -> (X-- : (a : A) -> (X-- : lt (f a) n) -> P a) -> (a : A) -> (X--1 : eq lzero nat (f a) n) -> P a) -> (a : A) -> P a
f-ind = λ (l17 l12 : Level) -> λ (A : Set l17) -> λ (f : (X-- : A) -> nat) -> λ (P : predicate l17 l12 A) -> λ (H : (n : nat) -> (X-- : (a : A) -> (X-- : lt (f a) n) -> P a) -> (a : A) -> (X--1 : eq lzero nat (f a) n) -> P a) -> λ (a : A) -> f-ind-aux l17 l12 A f P H (f a) a (refl lzero nat (f a))

f2-ind-aux : (l53 l52 l46 : Level) -> (A1 : Set l53) -> (A2 : Set l52) -> (f : (X-- : A1) -> (X--1 : A2) -> nat) -> (P : relation2 l53 l52 l46 A1 A2) -> (X-- : (n : nat) -> (X-- : (a1 : A1) -> (a2 : A2) -> (X-- : lt (f a1 a2) n) -> P a1 a2) -> (a1 : A1) -> (a2 : A2) -> (X--1 : eq lzero nat (f a1 a2) n) -> P a1 a2) -> (n : nat) -> (a1 : A1) -> (a2 : A2) -> (X--1 : eq lzero nat (f a1 a2) n) -> P a1 a2
f2-ind-aux = λ (l53 l52 l46 : Level) -> λ (A1 : Set l53) -> λ (A2 : Set l52) -> λ (f : (X-- : A1) -> (X--1 : A2) -> nat) -> λ (P : relation2 l53 l52 l46 A1 A2) -> λ (H : (n : nat) -> (X-- : (a1 : A1) -> (a2 : A2) -> (X-- : lt (f a1 a2) n) -> P a1 a2) -> (a1 : A1) -> (a2 : A2) -> (X--1 : eq lzero nat (f a1 a2) n) -> P a1 a2) -> λ (n : nat) -> nat-elim1 ((l53 ⊔ l52) ⊔ l46) n (λ (X-- : nat) -> (a1 : A1) -> (a2 : A2) -> (X--1 : eq lzero nat (f a1 a2) X--) -> P a1 a2) (λ (n0 : nat) -> λ (auto : (p : nat) -> (X-- : lt p n0) -> (a1 : A1) -> (a2 : A2) -> (X--1 : eq lzero nat (f a1 a2) p) -> P a1 a2) -> λ (a1 : A1) -> λ (a2 : A2) -> λ (auto' : eq lzero nat (f a1 a2) n0) -> H n0 (λ (a10 : A1) -> λ (a20 : A2) -> λ (auto'' : lt (f a10 a20) n0) -> auto (f a10 a20) auto'' a10 a20 (refl lzero nat (f a10 a20))) a1 a2 (rewrite-r lzero lzero nat n0 (λ (X-- : nat) -> eq lzero nat X-- n0) (refl lzero nat n0) (f a1 a2) auto'))

f2-ind : (l24 l23 l17 : Level) -> (A1 : Set l24) -> (A2 : Set l23) -> (f : (X-- : A1) -> (X--1 : A2) -> nat) -> (P : relation2 l24 l23 l17 A1 A2) -> (X-- : (n : nat) -> (X-- : (a1 : A1) -> (a2 : A2) -> (X-- : lt (f a1 a2) n) -> P a1 a2) -> (a1 : A1) -> (a2 : A2) -> (X--1 : eq lzero nat (f a1 a2) n) -> P a1 a2) -> (a1 : A1) -> (a2 : A2) -> P a1 a2
f2-ind = λ (l24 l23 l17 : Level) -> λ (A1 : Set l24) -> λ (A2 : Set l23) -> λ (f : (X-- : A1) -> (X--1 : A2) -> nat) -> λ (P : relation2 l24 l23 l17 A1 A2) -> λ (H : (n : nat) -> (X-- : (a1 : A1) -> (a2 : A2) -> (X-- : lt (f a1 a2) n) -> P a1 a2) -> (a1 : A1) -> (a2 : A2) -> (X--1 : eq lzero nat (f a1 a2) n) -> P a1 a2) -> λ (a1 : A1) -> λ (a2 : A2) -> f2-ind-aux l24 l23 l17 A1 A2 f P H (f a1 a2) a1 a2 (refl lzero nat (f a1 a2))

f3-ind-aux : (l64 l63 l62 l55 : Level) -> (A1 : Set l64) -> (A2 : Set l63) -> (A3 : Set l62) -> (f : (X-- : A1) -> (X--1 : A2) -> (X--2 : A3) -> nat) -> (P : relation3 l64 l63 l62 l55 A1 A2 A3) -> (X-- : (n : nat) -> (X-- : (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X-- : lt (f a1 a2 a3) n) -> P a1 a2 a3) -> (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X--1 : eq lzero nat (f a1 a2 a3) n) -> P a1 a2 a3) -> (n : nat) -> (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X--1 : eq lzero nat (f a1 a2 a3) n) -> P a1 a2 a3
f3-ind-aux = λ (l64 l63 l62 l55 : Level) -> λ (A1 : Set l64) -> λ (A2 : Set l63) -> λ (A3 : Set l62) -> λ (f : (X-- : A1) -> (X--1 : A2) -> (X--2 : A3) -> nat) -> λ (P : relation3 l64 l63 l62 l55 A1 A2 A3) -> λ (H : (n : nat) -> (X-- : (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X-- : lt (f a1 a2 a3) n) -> P a1 a2 a3) -> (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X--1 : eq lzero nat (f a1 a2 a3) n) -> P a1 a2 a3) -> λ (n : nat) -> nat-elim1 (((l62 ⊔ l64) ⊔ l55) ⊔ l63) n (λ (X-- : nat) -> (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X--1 : eq lzero nat (f a1 a2 a3) X--) -> P a1 a2 a3) (λ (n0 : nat) -> λ (auto : (p : nat) -> (X-- : lt p n0) -> (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X--1 : eq lzero nat (f a1 a2 a3) p) -> P a1 a2 a3) -> λ (a1 : A1) -> λ (a2 : A2) -> λ (a3 : A3) -> λ (auto' : eq lzero nat (f a1 a2 a3) n0) -> H n0 (λ (a10 : A1) -> λ (a20 : A2) -> λ (a30 : A3) -> λ (auto'' : lt (f a10 a20 a30) n0) -> auto (f a10 a20 a30) auto'' a10 a20 a30 (refl lzero nat (f a10 a20 a30))) a1 a2 a3 (rewrite-r lzero lzero nat n0 (λ (X-- : nat) -> eq lzero nat X-- n0) (refl lzero nat n0) (f a1 a2 a3) auto'))

f3-ind : (l31 l30 l29 l22 : Level) -> (A1 : Set l31) -> (A2 : Set l30) -> (A3 : Set l29) -> (f : (X-- : A1) -> (X--1 : A2) -> (X--2 : A3) -> nat) -> (P : relation3 l31 l30 l29 l22 A1 A2 A3) -> (X-- : (n : nat) -> (X-- : (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X-- : lt (f a1 a2 a3) n) -> P a1 a2 a3) -> (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X--1 : eq lzero nat (f a1 a2 a3) n) -> P a1 a2 a3) -> (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> P a1 a2 a3
f3-ind = λ (l31 l30 l29 l22 : Level) -> λ (A1 : Set l31) -> λ (A2 : Set l30) -> λ (A3 : Set l29) -> λ (f : (X-- : A1) -> (X--1 : A2) -> (X--2 : A3) -> nat) -> λ (P : relation3 l31 l30 l29 l22 A1 A2 A3) -> λ (H : (n : nat) -> (X-- : (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X-- : lt (f a1 a2 a3) n) -> P a1 a2 a3) -> (a1 : A1) -> (a2 : A2) -> (a3 : A3) -> (X--1 : eq lzero nat (f a1 a2 a3) n) -> P a1 a2 a3) -> λ (a1 : A1) -> λ (a2 : A2) -> λ (a3 : A3) -> f3-ind-aux l31 l30 l29 l22 A1 A2 A3 f P H (f a1 a2 a3) a1 a2 a3 (refl lzero nat (f a1 a2 a3))

lt-to-not-eq : (n : nat) -> (m : nat) -> (X-- : lt n m) -> Not lzero (eq lzero nat n m)
lt-to-not-eq = λ (n : nat) -> λ (m : nat) -> λ (H : lt n m) -> not-to-not lzero (eq lzero nat n m) (False lzero) (λ (auto : eq lzero nat n m) -> absurd lzero (le (S n) n) (eq-coerc lzero (le (S n) m) (le (S n) n) H (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S n) X--) (le (S n) n)) (refl (lsuc lzero) (Set (lzero)) (le (S n) n)) m auto)) (not-le-Sn-n n)) (nmk lzero (False lzero) (λ (auto : False lzero) -> auto))

le-n-O-to-eq : (n : nat) -> (X-- : le n O) -> eq lzero nat O n
le-n-O-to-eq = λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : le X-- O) -> eq lzero nat O X--) (λ (auto : le O O) -> refl lzero nat O) (λ (a : nat) -> λ (abs : le (S a) O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat O (S a)) (absurd lzero (le (S a) O) abs (not-le-Sn-O a))) n

le-to-le-to-eq : (n : nat) -> (m : nat) -> (X-- : le n m) -> (X--1 : le m n) -> eq lzero nat n m
le-to-le-to-eq = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> (X--1 : le X-- X-0) -> (X--2 : le X-0 X--) -> eq lzero nat X-- X-0) (λ (n : nat) -> λ (auto : le O n) -> λ (auto' : le n O) -> sym-eq lzero nat n O (sym-eq lzero nat O n (eq-coerc lzero (eq lzero nat O n) (eq lzero nat O n) (le-n-O-to-eq n auto') (refl (lsuc lzero) (Set (lzero)) (eq lzero nat O n))))) (λ (n : nat) -> λ (auto : le (S n) O) -> λ (auto' : le O (S n)) -> sym-eq lzero nat O (S n) (le-n-O-to-eq (S n) auto)) (λ (n : nat) -> λ (m : nat) -> λ (auto : (X-- : le n m) -> (X--1 : le m n) -> eq lzero nat n m) -> λ (auto' : le (S n) (S m)) -> λ (auto'' : le (S m) (S n)) -> eq-f lzero lzero nat nat S n m (auto (eq-coerc lzero (le (pred (S n)) (pred (S m))) (le n m) (monotonic-pred (S n) (S m) auto') (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S m))) (le n m)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n X--) (le n m)) (refl (lsuc lzero) (Set (lzero)) (le n m)) (pred (S m)) (pred-Sn m)) (pred (S n)) (pred-Sn n))) (eq-coerc lzero (le (pred (S m)) (pred (S n))) (le m n) (monotonic-pred (S m) (S n) auto'') (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S n))) (le m n)) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le m X--) (le m n)) (refl (lsuc lzero) (Set (lzero)) (le m n)) (pred (S n)) (pred-Sn n)) (pred (S m)) (pred-Sn m)))))

increasing-to-injective : (f : (X-- : nat) -> nat) -> (X-- : increasing f) -> ||injective|| lzero lzero nat nat f
increasing-to-injective = λ (f : (X-- : nat) -> nat) -> λ (incr : increasing f) -> λ (n : nat) -> λ (m : nat) -> match-Or lzero lzero (le n m) (Not lzero (le n m)) lzero (λ (X-- : Or lzero lzero (le n m) (Not lzero (le n m))) -> (X--1 : eq lzero nat (f n) (f m)) -> eq lzero nat n m) (λ (lenm : le n m) -> match-Or lzero lzero (lt n m) (eq lzero nat n m) lzero (λ (X-- : Or lzero lzero (lt n m) (eq lzero nat n m)) -> (X--1 : eq lzero nat (f n) (f m)) -> eq lzero nat n m) (λ (lenm0 : lt n m) -> λ (eqf : eq lzero nat (f n) (f m)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat n m) (absurd lzero (eq lzero nat (f n) (f m)) eqf (lt-to-not-eq (f n) (f m) (increasing-to-monotonic f incr n m lenm0)))) (λ (auto : eq lzero nat n m) -> λ (auto' : eq lzero nat (f n) (f m)) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) m auto) (le-to-or-lt-eq n m lenm)) (λ (nlenm : Not lzero (le n m)) -> λ (eqf : eq lzero nat (f n) (f m)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat n m) (absurd lzero (eq lzero nat (f n) (f m)) eqf (sym-not-eq lzero nat (f m) (f n) (lt-to-not-eq (f m) (f n) (increasing-to-monotonic f incr m n (not-le-to-lt n m nlenm)))))) (decidable-le n m)

minus-Sn-m : (m : nat) -> (n : nat) -> (X-- : le m n) -> eq lzero nat (minus (S n) m) (S (minus n m))
minus-Sn-m = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> (X--1 : le X-- X-0) -> eq lzero nat (minus (S X-0) X--) (S (minus X-0 X--))) (λ (n : nat) -> λ (auto : le O n) -> rewrite-l lzero lzero nat (S n) (λ (X-- : nat) -> eq lzero nat X-- (S (minus n O))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (S n) (S X--)) (refl lzero nat (S n)) (minus n O) (minus-n-O n)) (minus (S n) O) (minus-n-O (S n))) (λ (n : nat) -> λ (abs : le (S n) O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat (minus (S O) (S n)) (S (minus O (S n)))) (absurd lzero (le (S n) O) abs (not-le-Sn-O n))) (λ (n : nat) -> λ (m : nat) -> λ (Hind : (X-- : le n m) -> eq lzero nat (minus (S m) n) (S (minus m n))) -> λ (c : le (S n) (S m)) -> eq-coerc lzero (eq lzero nat (minus (S m) n) (S (minus m n))) (eq lzero nat (minus (S (S m)) (S n)) (S (minus (S m) (S n)))) (Hind (eq-coerc lzero (le (pred (S n)) (pred (S m))) (le n m) (monotonic-pred (S n) (S m) c) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S m))) (le n m)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n X--) (le n m)) (refl (lsuc lzero) (Set (lzero)) (le n m)) (pred (S m)) (pred-Sn m)) (pred (S n)) (pred-Sn n)))) (rewrite-r lzero (lsuc lzero) nat (minus (S m) n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (minus (S m) n) (S (minus m n))) (eq lzero nat X-- (S (minus (S m) (S n))))) (rewrite-r lzero (lsuc lzero) nat (minus m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (minus (S m) n) (S (minus m n))) (eq lzero nat (minus (S m) n) (S X--))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (minus (S m) n) (S (minus m n)))) (minus (S m) (S n)) (minus-S-S m n)) (minus (S (S m)) (S n)) (minus-S-S (S m) n)))

plus-minus : (m : nat) -> (n : nat) -> (p : nat) -> (X-- : le m n) -> eq lzero nat (plus (minus n m) p) (minus (plus n p) m)
plus-minus = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> (p : nat) -> (X--1 : le X-- X-0) -> eq lzero nat (plus (minus X-0 X--) p) (minus (plus X-0 p) X--)) (λ (n : nat) -> λ (p : nat) -> λ (auto : le O n) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (plus X-- p) (minus (plus n p) O)) (rewrite-l lzero lzero nat (plus n p) (λ (X-- : nat) -> eq lzero nat (plus n p) X--) (refl lzero nat (plus n p)) (minus (plus n p) O) (minus-n-O (plus n p))) (minus n O) (minus-n-O n)) (λ (n : nat) -> λ (p : nat) -> λ (abs : le (S n) O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat (plus (minus O (S n)) p) (minus (plus O p) (S n))) (absurd lzero (le (S n) O) abs (not-le-Sn-O n))) (λ (n : nat) -> λ (m : nat) -> λ (auto : (p : nat) -> (X-- : le n m) -> eq lzero nat (plus (minus m n) p) (minus (plus m p) n)) -> λ (p : nat) -> λ (auto' : le (S n) (S m)) -> auto p (eq-coerc lzero (le (pred (S n)) (pred (S m))) (le n m) (monotonic-pred (S n) (S m) auto') (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S m))) (le n m)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n X--) (le n m)) (refl (lsuc lzero) (Set (lzero)) (le n m)) (pred (S m)) (pred-Sn m)) (pred (S n)) (pred-Sn n))))

minus-plus-m-m : (n : nat) -> (m : nat) -> eq lzero nat n (minus (plus n m) m)
minus-plus-m-m = λ (n : nat) -> λ (m : nat) -> eq-coerc lzero (eq lzero nat (plus (minus m m) n) (minus (plus m n) m)) (eq lzero nat n (minus (plus n m) m)) (plus-minus m m n (le-n m)) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus X-- n) (minus (plus m n) m)) (eq lzero nat n (minus (plus n m) m))) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat X-- (minus (plus m n) m)) (eq lzero nat n (minus (plus n m) m))) (rewrite-r lzero (lsuc lzero) nat (plus n m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat n (minus X-- m)) (eq lzero nat n (minus (plus n m) m))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat n (minus (plus n m) m))) (plus m n) (commutative-plus m n)) (plus O n) (plus-O-n n)) (minus m m) (minus-n-n m))

plus-minus-m-m : (n : nat) -> (m : nat) -> (X-- : le m n) -> eq lzero nat n (plus (minus n m) m)
plus-minus-m-m = λ (n : nat) -> λ (m : nat) -> λ (lemn : le m n) -> sym-eq lzero nat (plus (minus n m) m) n (eq-coerc lzero (eq lzero nat (plus (minus n m) m) (minus (plus n m) m)) (eq lzero nat (plus (minus n m) m) n) (plus-minus m n m lemn) (rewrite-r lzero (lsuc lzero) nat (plus m (minus n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (minus n m) m) (minus (plus n m) m)) (eq lzero nat X-- n)) (rewrite-r lzero (lsuc lzero) nat (plus m (minus n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat X-- (minus (plus n m) m)) (eq lzero nat (plus m (minus n m)) n)) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus m (minus n m)) X--) (eq lzero nat (plus m (minus n m)) n)) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (plus m (minus n m)) n)) (minus (plus n m) m) (minus-plus-m-m n m)) (plus (minus n m) m) (commutative-plus (minus n m) m)) (plus (minus n m) m) (commutative-plus (minus n m) m)))

minus-to-plus : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : le m n) -> (X--1 : eq lzero nat (minus n m) p) -> eq lzero nat n (plus m p)
minus-to-plus = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (lemn : le m n) -> λ (eqp : eq lzero nat (minus n m) p) -> eq-coerc lzero (eq lzero nat n (plus (minus n m) m)) (eq lzero nat n (plus m p)) (plus-minus-m-m n m lemn) (rewrite-r lzero (lsuc lzero) nat (plus m (minus n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat n X--) (eq lzero nat n (plus m p))) (rewrite-r lzero (lsuc lzero) nat p (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat n (plus m X--)) (eq lzero nat n (plus m p))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat n (plus m p))) (minus n m) eqp) (plus (minus n m) m) (commutative-plus (minus n m) m))

plus-to-minus : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : eq lzero nat n (plus m p)) -> eq lzero nat (minus n m) p
plus-to-minus = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (eqp : eq lzero nat n (plus m p)) -> sym-eq lzero nat p (minus n m) (eq-coerc lzero (eq lzero nat p (minus (plus p m) m)) (eq lzero nat p (minus n m)) (minus-plus-m-m p m) (rewrite-r lzero (lsuc lzero) nat (plus m p) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat p (minus X-- m)) (eq lzero nat p (minus n m))) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat p (minus X-- m)) (eq lzero nat p (minus n m))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat p (minus n m))) (plus m p) eqp) (plus p m) (commutative-plus p m)))

minus-pred-pred : (n : nat) -> (m : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> eq lzero nat (minus (pred n) (pred m)) (minus n m)
minus-pred-pred = λ (n : nat) -> λ (m : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> lt-O-n-elim lzero n posn (λ (X-- : nat) -> eq lzero nat (minus (pred X--) (pred m)) (minus X-- m)) (lt-O-n-elim lzero m posm (λ (X-- : nat) -> (m0 : nat) -> eq lzero nat (minus (pred (S m0)) (pred X--)) (minus (S m0) X--)) (λ (m0 : nat) -> λ (m00 : nat) -> rewrite-l lzero lzero nat m00 (λ (X-- : nat) -> eq lzero nat (minus X-- (pred (S m0))) (minus (S m00) (S m0))) (rewrite-l lzero lzero nat m0 (λ (X-- : nat) -> eq lzero nat (minus m00 X--) (minus (S m00) (S m0))) (rewrite-r lzero lzero nat (minus m00 m0) (λ (X-- : nat) -> eq lzero nat (minus m00 m0) X--) (refl lzero nat (minus m00 m0)) (minus (S m00) (S m0)) (minus-S-S m00 m0)) (pred (S m0)) (pred-Sn m0)) (pred (S m00)) (pred-Sn m00)))

plus-minus-associative : (x : nat) -> (y : nat) -> (z : nat) -> (X-- : le z y) -> eq lzero nat (plus x (minus y z)) (minus (plus x y) z)
plus-minus-associative = λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> λ (auto : le z y) -> eq-coerc lzero (eq lzero nat (plus (minus y z) x) (minus (plus y x) z)) (eq lzero nat (plus x (minus y z)) (minus (plus x y) z)) (plus-minus z y x auto) (rewrite-r lzero (lsuc lzero) nat (plus x (minus y z)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat X-- (minus (plus y x) z)) (eq lzero nat (plus x (minus y z)) (minus (plus x y) z))) (rewrite-r lzero (lsuc lzero) nat (plus x y) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus x (minus y z)) (minus X-- z)) (eq lzero nat (plus x (minus y z)) (minus (plus x y) z))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (plus x (minus y z)) (minus (plus x y) z))) (plus y x) (commutative-plus y x)) (plus (minus y z) x) (commutative-plus (minus y z) x))

le-n-fn : (f : (X-- : nat) -> nat) -> (X-- : increasing f) -> (n : nat) -> le n (f n)
le-n-fn = λ (f : (X-- : nat) -> nat) -> λ (incr : increasing f) -> λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> le X-x-365 (f X-x-365)) (le-O-n (f O)) (λ (x-366 : nat) -> λ (X-x-368 : le x-366 (f x-366)) -> le-to-lt-to-lt x-366 (f x-366) (f (S x-366)) X-x-368 (incr x-366)) n

monotonic-le-minus-l : (p : nat) -> (q : nat) -> (n : nat) -> (X-- : le q p) -> le (minus q n) (minus p n)
monotonic-le-minus-l = nat-elim2 lzero (λ (X-- : nat) -> λ (X-0 : nat) -> (n : nat) -> (X--1 : le X-0 X--) -> le (minus X-0 n) (minus X-- n)) (λ (p : nat) -> λ (q : nat) -> λ (lePO : le p O) -> le-n-O-elim lzero p lePO (λ (X-- : nat) -> le (minus X-- q) (minus O q)) (le-n (minus O q))) (λ (p : nat) -> λ (q : nat) -> λ (auto : le O (S p)) -> le-plus-minus-m-m (minus O q) (match-nat lzero (λ (X-- : nat) -> nat) (S p) (λ (q0 : nat) -> minus p q0) q)) (λ (p : nat) -> λ (q : nat) -> λ (Hind : (n0 : nat) -> (X-- : le q p) -> le (minus q n0) (minus p n0)) -> λ (n : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : le (S q) (S p)) -> le (minus (S q) X--) (minus (S p) X--)) (λ (auto : le (S q) (S p)) -> auto) (λ (a : nat) -> λ (leSS : le (S q) (S p)) -> Hind a (eq-coerc lzero (le (pred (S q)) (pred (S p))) (le q p) (monotonic-pred (S q) (S p) leSS) (rewrite-l lzero (lsuc lzero) nat q (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (pred (S p))) (le q p)) (rewrite-l lzero (lsuc lzero) nat p (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le q X--) (le q p)) (refl (lsuc lzero) (Set (lzero)) (le q p)) (pred (S p)) (pred-Sn p)) (pred (S q)) (pred-Sn q)))) n)

le-minus-to-plus : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : le (minus n m) p) -> le n (plus p m)
le-minus-to-plus = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (lep : le (minus n m) p) -> transitive-le n (plus (minus n m) m) (plus p m) (le-plus-minus-m-m n m) (monotonic-le-plus-l m (minus n m) p lep)

le-minus-to-plus-r : (a : nat) -> (b : nat) -> (c : nat) -> (X-- : le c b) -> (X--1 : le a (minus b c)) -> le (plus a c) b
le-minus-to-plus-r = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (Hlecb : le c b) -> λ (H : le a (minus b c)) -> eq-ind-r lzero lzero nat (plus (minus b c) c) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (minus b c) c)) -> le (plus a c) x) (monotonic-le-plus-l c a (minus b c) H) b (plus-minus-m-m b c Hlecb)

le-plus-to-minus : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : le n (plus p m)) -> le (minus n m) p
le-plus-to-minus = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (lep : le n (plus p m)) -> eq-coerc lzero (le (minus n m) (minus (plus p m) m)) (le (minus n m) p) (monotonic-le-minus-l (plus p m) n m lep) (rewrite-l lzero (lsuc lzero) nat p (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus n m) X--) (le (minus n m) p)) (refl (lsuc lzero) (Set (lzero)) (le (minus n m) p)) (minus (plus p m) m) (minus-plus-m-m p m))

monotonic-le-minus-r : (p : nat) -> (q : nat) -> (n : nat) -> (X-- : le q p) -> le (minus n p) (minus n q)
monotonic-le-minus-r = λ (p : nat) -> λ (q : nat) -> λ (n : nat) -> λ (lepq : le q p) -> le-plus-to-minus n p (minus n q) (transitive-le n (plus (minus n q) q) (plus (minus n q) p) (le-plus-minus-m-m n q) (monotonic-le-plus-r (minus n q) q p lepq))

increasing-to-le : (f : (X-- : nat) -> nat) -> (X-- : increasing f) -> (m : nat) -> ex lzero lzero nat (λ (i : nat) -> le m (f i))
increasing-to-le = λ (f : (X-- : nat) -> nat) -> λ (incr : increasing f) -> λ (m : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> ex lzero lzero nat (λ (i : nat) -> le X-x-365 (f i))) (ex-intro lzero lzero nat (λ (i : nat) -> le O (f i)) m (eq-coerc lzero (le O (plus (f m) O)) (le O (f m)) (le-plus-n (f m) O) (rewrite-l lzero (lsuc lzero) nat (f m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le O X--) (le O (f m))) (refl (lsuc lzero) (Set (lzero)) (le O (f m))) (plus (f m) O) (plus-n-O (f m))))) (λ (n : nat) -> λ (X-clearme : ex lzero lzero nat (λ (i : nat) -> le n (f i))) -> match-ex lzero lzero nat (λ (i : nat) -> le n (f i)) lzero (λ (X-- : ex lzero lzero nat (λ (i : nat) -> le n (f i))) -> ex lzero lzero nat (λ (i : nat) -> le (S n) (f i))) (λ (a : nat) -> λ (lenfa : le n (f a)) -> ex-intro lzero lzero nat (λ (i : nat) -> le (S n) (f i)) (S a) (le-to-lt-to-lt n (f a) (f (S a)) lenfa (incr a))) X-clearme) m

minus-le : (x : nat) -> (y : nat) -> le (minus x y) x
minus-le = λ (x : nat) -> λ (y : nat) -> eq-coerc lzero (le (minus x y) (minus (plus x y) y)) (le (minus x y) x) (monotonic-le-minus-l (plus x y) x y (le-plus-n-r y x)) (rewrite-l lzero (lsuc lzero) nat x (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus x y) X--) (le (minus x y) x)) (refl (lsuc lzero) (Set (lzero)) (le (minus x y) x)) (minus (plus x y) y) (minus-plus-m-m x y))

not-eq-to-le-to-lt : (n : nat) -> (m : nat) -> (X-- : Not lzero (eq lzero nat n m)) -> (X--1 : le n m) -> lt n m
not-eq-to-le-to-lt = λ (n : nat) -> λ (m : nat) -> λ (Hneq : Not lzero (eq lzero nat n m)) -> λ (Hle : le n m) -> match-Or lzero lzero (lt n m) (eq lzero nat n m) lzero (λ (X-- : Or lzero lzero (lt n m) (eq lzero nat n m)) -> lt n m) (λ (auto : lt n m) -> auto) (λ (Heq : eq lzero nat n m) -> not-le-to-lt m n (not-to-not lzero (le m n) (eq lzero nat n m) (λ (auto : le m n) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) m Heq) Hneq)) (le-to-or-lt-eq n m Hle)

lt-times-n-to-lt-l : (n : nat) -> (p : nat) -> (q : nat) -> (X-- : lt (times p n) (times q n)) -> lt p q
lt-times-n-to-lt-l = λ (n : nat) -> λ (p : nat) -> λ (q : nat) -> λ (Hlt : lt (times p n) (times q n)) -> Or-ind lzero lzero lzero (lt p q) (Not lzero (lt p q)) (λ (X-x-170 : Or lzero lzero (lt p q) (Not lzero (lt p q))) -> lt p q) (λ (X-x-171 : lt p q) -> X-x-171) (λ (nltpq : Not lzero (lt p q)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt p q) (absurd lzero (le (times q n) (times p n)) (eq-coerc lzero (le (times n q) (times n p)) (le (times q n) (times p n)) (monotonic-le-times-r n q p (not-lt-to-le p q nltpq)) (rewrite-r lzero (lsuc lzero) nat (times n q) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n q) (times n p)) (le X-- (times p n))) (rewrite-r lzero (lsuc lzero) nat (times n p) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times n q) (times n p)) (le (times n q) X--)) (refl (lsuc lzero) (Set (lzero)) (le (times n q) (times n p))) (times p n) (commutative-times p n)) (times q n) (commutative-times q n))) (lt-to-not-le (times p n) (times q n) Hlt))) (decidable-lt p q)

lt-times-n-to-lt-r : (n : nat) -> (p : nat) -> (q : nat) -> (X-- : lt (times n p) (times n q)) -> lt p q
lt-times-n-to-lt-r = λ (n : nat) -> λ (p : nat) -> λ (q : nat) -> λ (auto : lt (times n p) (times n q)) -> lt-times-n-to-lt-l n p q (eq-coerc lzero (lt (times n p) (times n q)) (lt (times p n) (times q n)) auto (rewrite-r lzero (lsuc lzero) nat (times p n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (times n q)) (lt (times p n) (times q n))) (rewrite-r lzero (lsuc lzero) nat (times q n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (times p n) X--) (lt (times p n) (times q n))) (refl (lsuc lzero) (Set (lzero)) (lt (times p n) (times q n))) (times n q) (commutative-times n q)) (times n p) (commutative-times n p)))

lt-minus-to-plus : (a : nat) -> (b : nat) -> (c : nat) -> (X-- : lt (minus a b) c) -> lt a (plus c b)
lt-minus-to-plus = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (H : lt (minus a b) c) -> not-le-to-lt (plus c b) a (not-to-not lzero (le (plus c b) a) (le c (minus a b)) (λ (auto : le (plus c b) a) -> le-plus-to-minus-r c b a auto) (lt-to-not-le (minus a b) c H))

lt-minus-to-plus-r : (a : nat) -> (b : nat) -> (c : nat) -> (X-- : lt a (minus b c)) -> lt (plus a c) b
lt-minus-to-plus-r = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (H : lt a (minus b c)) -> not-le-to-lt b (plus a c) (not-to-not lzero (le b (plus a c)) (le (minus b c) a) (le-plus-to-minus b c a) (lt-to-not-le a (minus b c) H))

lt-plus-to-minus : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : le m n) -> (X--1 : lt n (plus p m)) -> lt (minus n m) p
lt-plus-to-minus = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (lenm : le m n) -> λ (H : lt n (plus p m)) -> eq-ind lzero lzero nat (minus (S n) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (minus (S n) m) x-1) -> le x-1 p) (le-plus-to-minus (S n) m p H) (S (minus n m)) (minus-Sn-m m n lenm)

monotonic-lt-minus-l : (p : nat) -> (q : nat) -> (n : nat) -> (X-- : le n q) -> (X--1 : lt q p) -> lt (minus q n) (minus p n)
monotonic-lt-minus-l = λ (p : nat) -> λ (q : nat) -> λ (n : nat) -> λ (H1 : le n q) -> λ (H2 : lt q p) -> lt-plus-to-minus-r (minus q n) n p (eq-ind lzero lzero nat q (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat q x-1) -> lt x-1 p) H2 (plus (minus q n) n) (plus-minus-m-m q n H1))

discr-minus-x-xy : (x : nat) -> (y : nat) -> (X-- : eq lzero nat x (minus x y)) -> Or lzero lzero (eq lzero nat x O) (eq lzero nat y O)
discr-minus-x-xy = λ (X-clearme : nat) -> match-nat lzero (λ (X-- : nat) -> (y : nat) -> (X--1 : eq lzero nat X-- (minus X-- y)) -> Or lzero lzero (eq lzero nat X-- O) (eq lzero nat y O)) (λ (y : nat) -> λ (auto : eq lzero nat O (minus O y)) -> or-introl lzero lzero (eq lzero nat O O) (eq lzero nat y O) (refl lzero nat O)) (λ (x : nat) -> λ (X-clearme0 : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : eq lzero nat (S x) (minus (S x) X--)) -> Or lzero lzero (eq lzero nat (S x) O) (eq lzero nat X-- O)) (λ (auto : eq lzero nat (S x) (minus (S x) O)) -> RC-reflexive lzero lzero nat (λ (X-- : nat) -> λ (X-0 : nat) -> eq lzero nat (S x) O) O) (λ (y : nat) -> λ (H : eq lzero nat (S x) (minus x y)) -> eq-ind lzero lzero nat (S x) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S x) x-1) -> (X-- : le x-1 x) -> Or lzero lzero (eq lzero nat (S x) O) (eq lzero nat (S y) O)) (λ (H0 : le (S x) x) -> Not-ind lzero lzero (le (S x) x) (λ (X-x-79 : Not lzero (le (S x) x)) -> Or lzero lzero (eq lzero nat (S x) O) (eq lzero nat (S y) O)) (λ (H00 : (X-- : le (S x) x) -> False lzero) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> Or lzero lzero (eq lzero nat (S x) O) (eq lzero nat (S y) O)) (H00 H0)) (not-le-Sn-n x)) (minus x y) H (minus-le x y)) X-clearme0) X-clearme

plus-le-0 : (x : nat) -> (y : nat) -> (X-- : le (plus x y) O) -> And lzero lzero (eq lzero nat x O) (eq lzero nat y O)
plus-le-0 = λ (x : nat) -> λ (y : nat) -> λ (H : le (plus x y) O) -> And-ind lzero lzero lzero (le x (minus O y)) (le y O) (λ (X-x-118 : And lzero lzero (le x (minus O y)) (le y O)) -> And lzero lzero (eq lzero nat x O) (eq lzero nat y O)) (λ (H1 : le x (minus O y)) -> λ (H2 : le y O) -> conj lzero lzero (eq lzero nat x O) (eq lzero nat y O) (sym-eq lzero nat O x (eq-coerc lzero (eq lzero nat O x) (eq lzero nat O x) (le-n-O-to-eq x H1) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat O x)))) (sym-eq lzero nat O y (eq-coerc lzero (eq lzero nat O y) (eq lzero nat O y) (le-n-O-to-eq y H2) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat O y))))) (le-inv-plus-l x y O H)

eq-minus-O : (n : nat) -> (m : nat) -> (X-- : le n m) -> eq lzero nat (minus n m) O
eq-minus-O = λ (n : nat) -> λ (m : nat) -> λ (lenm : le n m) -> le-n-O-elim lzero (minus n m) (eq-coerc lzero (le (minus n m) (minus n n)) (le (minus n m) O) (monotonic-le-minus-r m n n lenm) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus n m) X--) (le (minus n m) O)) (refl (lsuc lzero) (Set (lzero)) (le (minus n m) O)) (minus n n) (minus-n-n n))) (λ (X-- : nat) -> eq lzero nat X-- O) (refl lzero nat O)

distributive-times-minus : distributive lzero nat times minus
distributive-times-minus = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> match-Or lzero lzero (lt b c) (Not lzero (lt b c)) lzero (λ (X-- : Or lzero lzero (lt b c) (Not lzero (lt b c))) -> eq lzero nat (times a (minus b c)) (minus (times a b) (times a c))) (λ (Hbc : lt b c) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (times a x) (minus (times a b) (times a c))) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (times a O) x) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat X-- O) (refl lzero nat O) (times a O) (times-n-O a)) (minus (times a b) (times a c)) (eq-minus-O (times a b) (times a c) (monotonic-le-times-r a b c (lt-to-le b c Hbc)))) (minus b c) (eq-minus-O b c (lt-to-le b c Hbc))) (λ (Hbc : Not lzero (lt b c)) -> sym-eq lzero nat (minus (times a b) (times a c)) (times a (minus b c)) (eq-coerc lzero (eq lzero nat (minus (times a b) (times a c)) (times a (minus b c))) (eq lzero nat (minus (times a b) (times a c)) (times a (minus b c))) (plus-to-minus (times a b) (times a c) (times a (minus b c)) (eq-ind lzero lzero nat (times a (plus c (minus b c))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times a (plus c (minus b c))) x-1) -> eq lzero nat (times a b) x-1) (eq-f lzero lzero nat nat (times a) b (plus c (minus b c)) (eq-coerc lzero (eq lzero nat b (plus (minus b c) c)) (eq lzero nat b (plus c (minus b c))) (plus-minus-m-m b c (not-lt-to-le b c Hbc)) (rewrite-r lzero (lsuc lzero) nat (plus c (minus b c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat b X--) (eq lzero nat b (plus c (minus b c)))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat b (plus c (minus b c)))) (plus (minus b c) c) (commutative-plus (minus b c) c)))) (plus (times a c) (times a (minus b c))) (distributive-times-plus a c (minus b c)))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (minus (times a b) (times a c)) (times a (minus b c)))))) (decidable-lt b c)

minus-plus : (n : nat) -> (m : nat) -> (p : nat) -> eq lzero nat (minus (minus n m) p) (minus n (plus m p))
minus-plus = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> match-Or lzero lzero (le (plus m p) n) (Not lzero (le (plus m p) n)) lzero (λ (X-- : Or lzero lzero (le (plus m p) n) (Not lzero (le (plus m p) n))) -> eq lzero nat (minus (minus n m) p) (minus n (plus m p))) (λ (Hlt : le (plus m p) n) -> plus-to-minus (minus n m) p (minus n (plus m p)) (plus-to-minus n m (plus p (minus n (plus m p))) (eq-ind lzero lzero nat (plus (plus m p) (minus n (plus m p))) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (plus m p) (minus n (plus m p))) x-1) -> eq lzero nat n x-1) (minus-to-plus n (plus m p) (minus n (plus m p)) Hlt (refl lzero nat (minus n (plus m p)))) (plus m (plus p (minus n (plus m p)))) (associative-plus m p (minus n (plus m p)))))) (λ (Hlt : Not lzero (le (plus m p) n)) -> eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat x (minus n (plus m p))) (sym-eq lzero nat (minus n (plus m p)) O (eq-coerc lzero (eq lzero nat (minus n (plus m p)) O) (eq lzero nat (minus n (plus m p)) O) (eq-minus-O n (plus m p) (transitive-le n (S n) (plus m p) (le-n-Sn n) (not-le-to-lt (plus m p) n Hlt))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (minus n (plus m p)) O)))) (minus (minus n m) p) (eq-minus-O (minus n m) p (eq-coerc lzero (le (minus n m) (minus (plus p m) m)) (le (minus n m) p) (monotonic-le-minus-l (plus p m) n m (eq-coerc lzero (le n (plus m p)) (le n (plus p m)) (transitive-le n (S n) (plus m p) (le-n-Sn n) (not-le-to-lt (plus m p) n Hlt)) (rewrite-r lzero (lsuc lzero) nat (plus m p) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n (plus m p)) (le n X--)) (refl (lsuc lzero) (Set (lzero)) (le n (plus m p))) (plus p m) (commutative-plus p m)))) (rewrite-l lzero (lsuc lzero) nat p (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus n m) X--) (le (minus n m) p)) (refl (lsuc lzero) (Set (lzero)) (le (minus n m) p)) (minus (plus p m) m) (minus-plus-m-m p m))))) (decidable-le (plus m p) n)

minus-minus : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : le p m) -> (X--1 : le m n) -> eq lzero nat (plus p (minus n m)) (minus n (minus m p))
minus-minus = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (lepm : le p m) -> λ (lemn : le m n) -> sym-eq lzero nat (minus n (minus m p)) (plus p (minus n m)) (plus-to-minus n (minus m p) (plus p (minus n m)) (eq-ind lzero lzero nat (plus (plus (minus m p) p) (minus n m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (plus (minus m p) p) (minus n m)) x-1) -> eq lzero nat n x-1) (eq-ind lzero lzero nat m (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat m x-1) -> eq lzero nat n (plus x-1 (minus n m))) (eq-ind lzero lzero nat (plus (minus n m) m) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (minus n m) m) x-1) -> eq lzero nat n x-1) (eq-ind lzero lzero nat n (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat n x-1) -> eq lzero nat n x-1) (refl lzero nat n) (plus (minus n m) m) (plus-minus-m-m n m lemn)) (plus m (minus n m)) (commutative-plus (minus n m) m)) (plus (minus m p) p) (plus-minus-m-m m p lepm)) (plus (minus m p) (plus p (minus n m))) (associative-plus (minus m p) p (minus n m))))

minus-minus-associative : (x : nat) -> (y : nat) -> (z : nat) -> (X-- : le z y) -> (X--1 : le y x) -> eq lzero nat (minus x (minus y z)) (plus (minus x y) z)
minus-minus-associative = λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> λ (auto : le z y) -> λ (auto' : le y x) -> sym-eq lzero nat (plus (minus x y) z) (minus x (minus y z)) (eq-coerc lzero (eq lzero nat (plus z (minus x y)) (minus x (minus y z))) (eq lzero nat (plus (minus x y) z) (minus x (minus y z))) (minus-minus x y z auto auto') (rewrite-r lzero (lsuc lzero) nat (plus z (minus x y)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus z (minus x y)) (minus x (minus y z))) (eq lzero nat X-- (minus x (minus y z)))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (plus z (minus x y)) (minus x (minus y z)))) (plus (minus x y) z) (commutative-plus (minus x y) z)))

minus-minus-comm : (a : nat) -> (b : nat) -> (c : nat) -> eq lzero nat (minus (minus a b) c) (minus (minus a c) b)
minus-minus-comm = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> le-to-le-to-eq (minus (minus a b) c) (minus (minus a c) b) (eq-coerc lzero (le (minus (minus a b) c) (minus (plus (minus (minus a c) b) c) c)) (le (minus (minus a b) c) (minus (minus a c) b)) (monotonic-le-minus-l (plus (minus (minus a c) b) c) (minus a b) c (eq-coerc lzero (le (minus a b) (plus (minus (minus a b) c) c)) (le (minus a b) (plus (minus (minus a c) b) c)) (le-plus-minus-m-m (minus a b) c) (rewrite-r lzero (lsuc lzero) nat (minus a (plus b c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a b) (plus X-- c)) (le (minus a b) (plus (minus (minus a c) b) c))) (rewrite-r lzero (lsuc lzero) nat (plus c (minus a (plus b c))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a b) X--) (le (minus a b) (plus (minus (minus a c) b) c))) (rewrite-r lzero (lsuc lzero) nat (plus c (minus (minus a c) b)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a b) (plus c (minus a (plus b c)))) (le (minus a b) X--)) (rewrite-l lzero (lsuc lzero) nat (minus (minus a c) b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a b) (plus c X--)) (le (minus a b) (plus c (minus (minus a c) b)))) (refl (lsuc lzero) (Set (lzero)) (le (minus a b) (plus c (minus (minus a c) b)))) (minus a (plus b c)) (rewrite-l lzero lzero nat (plus c b) (λ (X-- : nat) -> eq lzero nat (minus (minus a c) b) (minus a X--)) (minus-plus a c b) (plus b c) (commutative-plus c b))) (plus (minus (minus a c) b) c) (commutative-plus (minus (minus a c) b) c)) (plus (minus a (plus b c)) c) (commutative-plus (minus a (plus b c)) c)) (minus (minus a b) c) (minus-plus a b c)))) (rewrite-l lzero (lsuc lzero) nat (minus (minus a c) b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (minus a b) c) X--) (le (minus (minus a b) c) (minus (minus a c) b))) (refl (lsuc lzero) (Set (lzero)) (le (minus (minus a b) c) (minus (minus a c) b))) (minus (plus (minus (minus a c) b) c) c) (minus-plus-m-m (minus (minus a c) b) c))) (eq-coerc lzero (le (minus (minus a c) b) (minus (plus (minus (minus a b) c) b) b)) (le (minus (minus a c) b) (minus (minus a b) c)) (monotonic-le-minus-l (plus (minus (minus a b) c) b) (minus a c) b (eq-coerc lzero (le (minus a c) (plus (minus (minus a c) b) b)) (le (minus a c) (plus (minus (minus a b) c) b)) (le-plus-minus-m-m (minus a c) b) (rewrite-r lzero (lsuc lzero) nat (minus a (plus c b)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a c) (plus X-- b)) (le (minus a c) (plus (minus (minus a b) c) b))) (rewrite-r lzero (lsuc lzero) nat (plus b (minus a (plus c b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a c) X--) (le (minus a c) (plus (minus (minus a b) c) b))) (rewrite-r lzero (lsuc lzero) nat (plus b (minus (minus a b) c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a c) (plus b (minus a (plus c b)))) (le (minus a c) X--)) (rewrite-l lzero (lsuc lzero) nat (minus (minus a b) c) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus a c) (plus b X--)) (le (minus a c) (plus b (minus (minus a b) c)))) (refl (lsuc lzero) (Set (lzero)) (le (minus a c) (plus b (minus (minus a b) c)))) (minus a (plus c b)) (rewrite-l lzero lzero nat (plus b c) (λ (X-- : nat) -> eq lzero nat (minus (minus a b) c) (minus a X--)) (minus-plus a b c) (plus c b) (commutative-plus b c))) (plus (minus (minus a b) c) b) (commutative-plus (minus (minus a b) c) b)) (plus (minus a (plus c b)) b) (commutative-plus (minus a (plus c b)) b)) (minus (minus a c) b) (minus-plus a c b)))) (rewrite-l lzero (lsuc lzero) nat (minus (minus a b) c) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (minus (minus a c) b) X--) (le (minus (minus a c) b) (minus (minus a b) c))) (refl (lsuc lzero) (Set (lzero)) (le (minus (minus a c) b) (minus (minus a b) c))) (minus (plus (minus (minus a b) c) b) b) (minus-plus-m-m (minus (minus a b) c) b)))

minus-le-minus-minus-comm : (b : nat) -> (c : nat) -> (a : nat) -> (X-- : le c b) -> eq lzero nat (minus a (minus b c)) (minus (plus a c) b)
minus-le-minus-minus-comm = λ (b : nat) -> λ (c : nat) -> λ (a : nat) -> λ (H : le c b) -> eq-ind-r lzero lzero nat (plus (minus b c) c) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (minus b c) c)) -> eq lzero nat (minus a (minus b c)) (minus (plus a c) x)) (rewrite-r lzero lzero nat (plus c a) (λ (X-- : nat) -> eq lzero nat (minus a (minus b c)) (minus X-- (plus (minus b c) c))) (rewrite-r lzero lzero nat (plus c (minus b c)) (λ (X-- : nat) -> eq lzero nat (minus a (minus b c)) (minus (plus c a) X--)) (rewrite-l lzero lzero nat (minus (minus (plus c a) c) (minus b c)) (λ (X-- : nat) -> eq lzero nat (minus a (minus b c)) X--) (rewrite-r lzero lzero nat (minus (plus c a) c) (λ (X-- : nat) -> eq lzero nat (minus X-- (minus b c)) (minus (minus (plus c a) c) (minus b c))) (refl lzero nat (minus (minus (plus c a) c) (minus b c))) a (rewrite-l lzero lzero nat (plus a c) (λ (X-- : nat) -> eq lzero nat a (minus X-- c)) (minus-plus-m-m a c) (plus c a) (commutative-plus a c))) (minus (plus c a) (plus c (minus b c))) (minus-plus (plus c a) c (minus b c))) (plus (minus b c) c) (commutative-plus (minus b c) c)) (plus a c) (commutative-plus a c)) b (plus-minus-m-m b c H)

minus-minus-m-m : (m : nat) -> (n : nat) -> (X-- : le n m) -> eq lzero nat (minus m (minus m n)) n
minus-minus-m-m = λ (m : nat) -> λ (n : nat) -> λ (auto : le n m) -> eq-coerc lzero (eq lzero nat (minus m (minus m n)) (minus (plus m n) m)) (eq lzero nat (minus m (minus m n)) n) (minus-le-minus-minus-comm m n m auto) (rewrite-r lzero (lsuc lzero) nat (plus n m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (minus m (minus m n)) (minus X-- m)) (eq lzero nat (minus m (minus m n)) n)) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (minus m (minus m n)) X--) (eq lzero nat (minus m (minus m n)) n)) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (minus m (minus m n)) n)) (minus (plus n m) m) (minus-plus-m-m n m)) (plus m n) (commutative-plus m n))

minus-plus-plus-l : (x : nat) -> (y : nat) -> (h : nat) -> eq lzero nat (minus (plus x h) (plus y h)) (minus x y)
minus-plus-plus-l = λ (x : nat) -> λ (y : nat) -> λ (h : nat) -> rewrite-l lzero lzero nat (minus (minus (plus x h) y) h) (λ (X-- : nat) -> eq lzero nat X-- (minus x y)) (rewrite-r lzero lzero nat (minus x y) (λ (X-- : nat) -> eq lzero nat X-- (minus x y)) (refl lzero nat (minus x y)) (minus (minus (plus x h) y) h) (rewrite-r lzero lzero nat (minus (plus x h) h) (λ (X-- : nat) -> eq lzero nat (minus (minus (plus x h) y) h) (minus X-- y)) (minus-minus-comm (plus x h) y h) x (minus-plus-m-m x h))) (minus (plus x h) (plus y h)) (minus-plus (plus x h) y h)

plus-minus-plus-plus-l : (z : nat) -> (x : nat) -> (y : nat) -> (h : nat) -> eq lzero nat (minus (plus z (plus x h)) (plus y h)) (minus (plus z x) y)
plus-minus-plus-plus-l = λ (z : nat) -> λ (x : nat) -> λ (y : nat) -> λ (h : nat) -> rewrite-r lzero lzero nat (minus (plus z x) y) (λ (X-- : nat) -> eq lzero nat X-- (minus (plus z x) y)) (refl lzero nat (minus (plus z x) y)) (minus (plus z (plus x h)) (plus y h)) (rewrite-l lzero lzero nat (plus (plus z x) h) (λ (X-- : nat) -> eq lzero nat (minus X-- (plus y h)) (minus (plus z x) y)) (minus-plus-plus-l (plus z x) y h) (plus z (plus x h)) (associative-plus z x h))

minus-plus-minus-l : (x : nat) -> (y : nat) -> (z : nat) -> (X-- : le y z) -> eq lzero nat (minus (plus z x) (minus z y)) (plus x y)
minus-plus-minus-l = λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> λ (auto : le y z) -> eq-coerc lzero (eq lzero nat (minus (plus x z) (minus z y)) (plus (minus (plus x z) z) y)) (eq lzero nat (minus (plus z x) (minus z y)) (plus x y)) (minus-minus-associative (plus x z) z y auto (eq-coerc lzero (le z (plus z x)) (le z (plus x z)) (le-plus-n-r x z) (rewrite-r lzero (lsuc lzero) nat (plus x z) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le z X--) (le z (plus x z))) (refl (lsuc lzero) (Set (lzero)) (le z (plus x z))) (plus z x) (commutative-plus z x)))) (rewrite-r lzero (lsuc lzero) nat (plus x z) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (minus (plus x z) (minus z y)) (plus (minus (plus x z) z) y)) (eq lzero nat (minus X-- (minus z y)) (plus x y))) (rewrite-l lzero (lsuc lzero) nat x (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (minus (plus x z) (minus z y)) (plus X-- y)) (eq lzero nat (minus (plus x z) (minus z y)) (plus x y))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (minus (plus x z) (minus z y)) (plus x y))) (minus (plus x z) z) (minus-plus-m-m x z)) (plus z x) (commutative-plus z x))

le-fwd-plus-plus-ge : (m1 : nat) -> (m2 : nat) -> (X-- : le m2 m1) -> (n1 : nat) -> (n2 : nat) -> (X--1 : le (plus m1 n1) (plus m2 n2)) -> le n1 n2
le-fwd-plus-plus-ge = λ (m1 : nat) -> λ (m2 : nat) -> λ (H : le m2 m1) -> λ (n1 : nat) -> λ (n2 : nat) -> eq-ind-r lzero lzero nat (plus n1 m1) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus n1 m1)) -> (X--1 : le x (plus m2 n2)) -> le n1 n2) (λ (H0 : le (plus n1 m1) (plus m2 n2)) -> And-ind lzero lzero lzero (le n1 (minus (plus m2 n2) m1)) (le m1 (plus m2 n2)) (λ (X-x-118 : And lzero lzero (le n1 (minus (plus m2 n2) m1)) (le m1 (plus m2 n2))) -> le n1 n2) (eq-ind-r lzero lzero nat (plus n2 m2) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus n2 m2)) -> (X-x-120 : le n1 (minus x m1)) -> (X-x-119 : le m1 x) -> le n1 n2) (eq-ind lzero lzero nat (minus n2 (minus m1 m2)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (minus n2 (minus m1 m2)) x-1) -> (X-x-120 : le n1 x-1) -> (X-x-119 : le m1 (plus n2 m2)) -> le n1 n2) (λ (H1 : le n1 (minus n2 (minus m1 m2))) -> λ (X-- : le m1 (plus n2 m2)) -> transitive-le n1 (minus n2 (minus m1 m2)) n2 H1 (minus-le n2 (minus m1 m2))) (minus (plus n2 m2) m1) (minus-le-minus-minus-comm m1 m2 n2 H)) (plus m2 n2) (commutative-plus m2 n2)) (le-inv-plus-l n1 m1 (plus m2 n2) H0)) (plus m1 n1) (commutative-plus m1 n1)

eqb : (X---v : nat) -> (X--1-v : nat) -> matita-basics-bool.bool
eqb O y = match-nat lzero (λ (X--1-v : nat) -> matita-basics-bool.bool) matita-basics-bool.true (λ (q-v : nat) -> matita-basics-bool.false) y
eqb (S x) y = match-nat lzero (λ (X--1-v : nat) -> matita-basics-bool.bool) matita-basics-bool.false (λ (q-v : nat) -> eqb x q-v) y



eqb-elim : (l28 : Level) -> (n : nat) -> (m : nat) -> (P : (X-- : bool) -> Set l28) -> (X-- : (X-- : eq lzero nat n m) -> P true) -> (X--1 : (X--1 : Not lzero (eq lzero nat n m)) -> P false) -> P (eqb n m)
eqb-elim = λ (l28 : Level) -> nat-elim2 ((lsuc lzero) ⊔ (lsuc l28)) (λ (X-- : nat) -> λ (X-0 : nat) -> (P : (X--1 : bool) -> Set l28) -> (X--1 : (X--1 : eq lzero nat X-- X-0) -> P true) -> (X--2 : (X--2 : Not lzero (eq lzero nat X-- X-0)) -> P false) -> P (eqb X-- X-0)) (λ (n : nat) -> match-nat ((lsuc lzero) ⊔ (lsuc l28)) (λ (X-- : nat) -> (P : (X--1 : bool) -> Set l28) -> (X--1 : (X--1 : eq lzero nat O X--) -> P true) -> (X--2 : (X--2 : Not lzero (eq lzero nat O X--)) -> P false) -> P (eqb O X--)) (λ (P : (X-- : bool) -> Set l28) -> λ (auto : (X-- : eq lzero nat O O) -> P true) -> λ (auto' : (X-- : Not lzero (eq lzero nat O O)) -> P false) -> auto (refl lzero nat O)) (λ (auto : nat) -> λ (P : (X-- : bool) -> Set l28) -> λ (auto' : (X-- : eq lzero nat O (S auto)) -> P true) -> λ (auto'' : (X-- : Not lzero (eq lzero nat O (S auto))) -> P false) -> auto'' (not-eq-O-S auto)) n) (λ (n : nat) -> λ (P : (X-- : bool) -> Set l28) -> λ (auto : (X-- : eq lzero nat (S n) O) -> P true) -> λ (auto' : (X-- : Not lzero (eq lzero nat (S n) O)) -> P false) -> auto' (sym-not-eq lzero nat O (S n) (not-eq-O-S n))) (λ (n : nat) -> λ (m : nat) -> λ (auto : (P : (X-- : bool) -> Set l28) -> (X-- : (X-- : eq lzero nat n m) -> P true) -> (X--1 : (X--1 : Not lzero (eq lzero nat n m)) -> P false) -> P (eqb n m)) -> λ (P : (X-- : bool) -> Set l28) -> λ (auto' : (X-- : eq lzero nat (S n) (S m)) -> P true) -> λ (auto'' : (X-- : Not lzero (eq lzero nat (S n) (S m))) -> P false) -> auto P (λ (auto''' : eq lzero nat n m) -> auto' (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (S n) (S X--)) (refl lzero nat (S n)) m auto''')) (λ (auto''' : Not lzero (eq lzero nat n m)) -> auto'' (not-eq-S n m auto''')))

eqb-n-n : (n : nat) -> eq lzero bool (eqb n n) true
eqb-n-n = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> eq lzero bool (eqb X-x-365 X-x-365) true) (refl lzero bool true) (λ (x-366 : nat) -> λ (X-x-368 : eq lzero bool (eqb x-366 x-366) true) -> rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (eqb x-366 x-366) X-x-368) n

eqb-true-to-eq : (n : nat) -> (m : nat) -> (X-- : eq lzero bool (eqb n m) true) -> eq lzero nat n m
eqb-true-to-eq = λ (n : nat) -> λ (m : nat) -> eqb-elim lzero n m (λ (X-- : bool) -> (X--1 : eq lzero bool X-- true) -> eq lzero nat n m) (λ (auto : eq lzero nat n m) -> λ (auto' : eq lzero bool true true) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) m auto) (λ (X-- : Not lzero (eq lzero nat n m)) -> λ (abs : eq lzero bool false true) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat n m) (absurd lzero (eq lzero bool true false) (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool true X--1) (refl lzero bool true) false abs) not-eq-true-false))

eqb-false-to-not-eq : (n : nat) -> (m : nat) -> (X-- : eq lzero bool (eqb n m) false) -> Not lzero (eq lzero nat n m)
eqb-false-to-not-eq = λ (n : nat) -> λ (m : nat) -> eqb-elim lzero n m (λ (X-- : bool) -> (X--1 : eq lzero bool X-- false) -> Not lzero (eq lzero nat n m)) (λ (auto : eq lzero nat n m) -> λ (auto' : eq lzero bool true false) -> not-to-not lzero (eq lzero nat n m) (eq lzero bool true false) (λ (auto'' : eq lzero nat n m) -> rewrite-l lzero lzero bool true (λ (X-- : bool) -> eq lzero bool true X--) (refl lzero bool true) false auto') not-eq-true-false) (λ (auto : Not lzero (eq lzero nat n m)) -> λ (auto' : eq lzero bool false false) -> auto)

eq-to-eqb-true : (n : nat) -> (m : nat) -> (X-- : eq lzero nat n m) -> eq lzero bool (eqb n m) true
eq-to-eqb-true = λ (n : nat) -> λ (m : nat) -> λ (auto : eq lzero nat n m) -> rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero bool (eqb n X--) true) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (eqb n n) (eqb-n-n n)) m auto

not-eq-to-eqb-false : (n : nat) -> (m : nat) -> (X-- : Not lzero (eq lzero nat n m)) -> eq lzero bool (eqb n m) false
not-eq-to-eqb-false = λ (n : nat) -> λ (m : nat) -> λ (noteq : Not lzero (eq lzero nat n m)) -> eqb-elim lzero n m (λ (X-- : bool) -> eq lzero bool X-- false) (λ (Heq : eq lzero nat n m) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero bool true false) (absurd lzero (eq lzero nat n m) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) m Heq) noteq)) (λ (auto : Not lzero (eq lzero nat n m)) -> refl lzero bool false)

leb : (X---v : nat) -> (X--1-v : nat) -> matita-basics-bool.bool
leb O _ = matita-basics-bool.true
leb (S x) y = match-nat lzero (λ (X--1-v : nat) -> matita-basics-bool.bool) matita-basics-bool.false (λ (q-v : nat) -> leb x q-v) y



leb-elim : (l22 : Level) -> (n : nat) -> (m : nat) -> (P : (X-- : bool) -> Set l22) -> (X-- : (X-- : le n m) -> P true) -> (X--1 : (X--1 : Not lzero (le n m)) -> P false) -> P (leb n m)
leb-elim = λ (l22 : Level) -> nat-elim2 ((lsuc lzero) ⊔ (lsuc l22)) (λ (X-- : nat) -> λ (X-0 : nat) -> (P : (X--1 : bool) -> Set l22) -> (X--1 : (X--1 : le X-- X-0) -> P true) -> (X--2 : (X--2 : Not lzero (le X-- X-0)) -> P false) -> P (leb X-- X-0)) (λ (n : nat) -> λ (P : (X-- : bool) -> Set l22) -> λ (auto : (X-- : le O n) -> P true) -> λ (auto' : (X-- : Not lzero (le O n)) -> P false) -> auto (le-O-n n)) (λ (n : nat) -> λ (P : (X-- : bool) -> Set l22) -> λ (auto : (X-- : le (S n) O) -> P true) -> λ (auto' : (X-- : Not lzero (le (S n) O)) -> P false) -> auto' (not-le-Sn-O n)) (λ (n : nat) -> λ (m : nat) -> λ (Hind : (P : (X-- : bool) -> Set l22) -> (X-- : (X-- : le n m) -> P true) -> (X--1 : (X--1 : Not lzero (le n m)) -> P false) -> P (leb n m)) -> λ (P : (X-- : bool) -> Set l22) -> λ (Pt : (X-- : le (S n) (S m)) -> P true) -> λ (Pf : (X-- : Not lzero (le (S n) (S m))) -> P false) -> Hind P (λ (lenm : le n m) -> Pt (le-S-S n m lenm)) (λ (nlenm : Not lzero (le n m)) -> Pf (not-le-to-not-le-S-S n m nlenm)))

leb-true-to-le : (n : nat) -> (m : nat) -> (X-- : eq lzero bool (leb n m) true) -> le n m
leb-true-to-le = λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> (X--1 : eq lzero bool X-- true) -> le n m) (λ (auto : le n m) -> λ (auto' : eq lzero bool true true) -> auto) (λ (X-- : Not lzero (le n m)) -> λ (abs : eq lzero bool false true) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> le n m) (absurd lzero (eq lzero bool true false) (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool true X--1) (refl lzero bool true) false abs) not-eq-true-false))

leb-false-to-not-le : (n : nat) -> (m : nat) -> (X-- : eq lzero bool (leb n m) false) -> Not lzero (le n m)
leb-false-to-not-le = λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> (X--1 : eq lzero bool X-- false) -> Not lzero (le n m)) (λ (X-- : le n m) -> λ (abs : eq lzero bool true false) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> Not lzero (le n m)) (absurd lzero (eq lzero bool true false) (rewrite-l lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool true X--1) (refl lzero bool true) false abs) not-eq-true-false)) (λ (auto : Not lzero (le n m)) -> λ (auto' : eq lzero bool false false) -> auto)

le-to-leb-true : (n : nat) -> (m : nat) -> (X-- : le n m) -> eq lzero bool (leb n m) true
le-to-leb-true = λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> (X--1 : le n m) -> eq lzero bool X-- true) (λ (auto : le n m) -> λ (auto' : le n m) -> refl lzero bool true) (λ (H : Not lzero (le n m)) -> λ (H1 : le n m) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero bool false true) (absurd lzero (le n m) H1 H))

not-le-to-leb-false : (n : nat) -> (m : nat) -> (X-- : Not lzero (le n m)) -> eq lzero bool (leb n m) false
not-le-to-leb-false = λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> (X--1 : Not lzero (le n m)) -> eq lzero bool X-- false) (λ (H : le n m) -> λ (H1 : Not lzero (le n m)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero bool true false) (absurd lzero (le n m) H H1)) (λ (auto : Not lzero (le n m)) -> λ (auto' : Not lzero (le n m)) -> refl lzero bool false)

lt-to-leb-false : (n : nat) -> (m : nat) -> (X-- : lt m n) -> eq lzero bool (leb n m) false
lt-to-leb-false = λ (n : nat) -> λ (m : nat) -> λ (auto : lt m n) -> not-le-to-leb-false n m (lt-to-not-le m n auto)

min : (X-- : nat) -> (X--1 : nat) -> nat
min = λ (n : nat) -> λ (m : nat) -> match-bool lzero (λ (X-- : bool) -> nat) n m (leb n m)

max : (X-- : nat) -> (X--1 : nat) -> nat
max = λ (n : nat) -> λ (m : nat) -> match-bool lzero (λ (X-- : bool) -> nat) m n (leb n m)

commutative-min : commutative lzero nat min
commutative-min = λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> eq lzero nat (match-bool lzero (λ (X-0 : bool) -> nat) n m X--) (match-bool lzero (λ (X-0 : bool) -> nat) m n (leb m n))) (leb-elim lzero m n (λ (X-- : bool) -> (X--1 : le n m) -> eq lzero nat (match-bool lzero (λ (X-0 : bool) -> nat) n m true) (match-bool lzero (λ (X-0 : bool) -> nat) m n X--)) (λ (auto : le m n) -> λ (auto' : le n m) -> le-to-le-to-eq n m auto' auto) (λ (auto : Not lzero (le m n)) -> λ (auto' : le n m) -> refl lzero nat n)) (λ (notle : Not lzero (le n m)) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero nat (match-bool lzero (λ (X-0 : bool) -> nat) n m false) (match-bool lzero (λ (X-0 : bool) -> nat) m n x)) (refl lzero nat (match-bool lzero (λ (X-0 : bool) -> nat) n m false)) (leb m n) (le-to-leb-true m n (transitive-le m (S m) n (le-n-Sn m) (not-le-to-lt n m notle))))

le-minr : (i : nat) -> (n : nat) -> (m : nat) -> (X-- : le i (min n m)) -> le i m
le-minr = λ (i : nat) -> λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> (X--1 : le i (match-bool lzero (λ (X-0 : bool) -> nat) n m X--)) -> le i m) (λ (auto : le n m) -> λ (auto' : le i n) -> transitive-le i n m auto' auto) (λ (auto : Not lzero (le n m)) -> λ (auto' : le i m) -> auto')

le-minl : (i : nat) -> (n : nat) -> (m : nat) -> (X-- : le i (min n m)) -> le i n
le-minl = λ (i : nat) -> λ (n : nat) -> λ (m : nat) -> λ (auto : le i (min n m)) -> le-minr i m n (eq-coerc lzero (le i (min n m)) (le i (min m n)) auto (rewrite-r lzero (lsuc lzero) nat (min m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le i X--) (le i (min m n))) (refl (lsuc lzero) (Set (lzero)) (le i (min m n))) (min n m) (commutative-min n m)))

to-min : (i : nat) -> (n : nat) -> (m : nat) -> (X-- : le i n) -> (X--1 : le i m) -> le i (min n m)
to-min = λ (i : nat) -> λ (n : nat) -> λ (m : nat) -> λ (lein : le i n) -> λ (leim : le i m) -> match-bool lzero (λ (X-- : bool) -> le i (match-bool lzero (λ (X-0 : bool) -> nat) n m X--)) lein leim (leb n m)

commutative-max : commutative lzero nat max
commutative-max = λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> eq lzero nat (match-bool lzero (λ (X-0 : bool) -> nat) m n X--) (match-bool lzero (λ (X-0 : bool) -> nat) n m (leb m n))) (leb-elim lzero m n (λ (X-- : bool) -> (X--1 : le n m) -> eq lzero nat (match-bool lzero (λ (X-0 : bool) -> nat) m n true) (match-bool lzero (λ (X-0 : bool) -> nat) n m X--)) (λ (auto : le m n) -> λ (auto' : le n m) -> le-to-le-to-eq m n auto auto') (λ (auto : Not lzero (le m n)) -> λ (auto' : le n m) -> refl lzero nat m)) (λ (notle : Not lzero (le n m)) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero nat (match-bool lzero (λ (X-0 : bool) -> nat) m n false) (match-bool lzero (λ (X-0 : bool) -> nat) n m x)) (refl lzero nat (match-bool lzero (λ (X-0 : bool) -> nat) m n false)) (leb m n) (le-to-leb-true m n (transitive-le m (S m) n (le-n-Sn m) (not-le-to-lt n m notle))))

le-maxl : (i : nat) -> (n : nat) -> (m : nat) -> (X-- : le (max n m) i) -> le n i
le-maxl = λ (i : nat) -> λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> (X--1 : le (match-bool lzero (λ (X-0 : bool) -> nat) m n X--) i) -> le n i) (λ (auto : le n m) -> λ (auto' : le m i) -> transitive-le n m i auto auto') (λ (auto : Not lzero (le n m)) -> λ (auto' : le n i) -> auto')

le-maxr : (i : nat) -> (n : nat) -> (m : nat) -> (X-- : le (max n m) i) -> le m i
le-maxr = λ (i : nat) -> λ (n : nat) -> λ (m : nat) -> λ (auto : le (max n m) i) -> le-maxl i m n (eq-coerc lzero (le (max n m) i) (le (max m n) i) auto (rewrite-r lzero (lsuc lzero) nat (max m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- i) (le (max m n) i)) (refl (lsuc lzero) (Set (lzero)) (le (max m n) i)) (max n m) (commutative-max n m)))

to-max : (i : nat) -> (n : nat) -> (m : nat) -> (X-- : le n i) -> (X--1 : le m i) -> le (max n m) i
to-max = λ (i : nat) -> λ (n : nat) -> λ (m : nat) -> λ (leni : le n i) -> λ (lemi : le m i) -> match-bool lzero (λ (X-- : bool) -> le (match-bool lzero (λ (X-0 : bool) -> nat) m n X--) i) lemi leni (leb n m)