matita-arithmetics-div-and-mod.agda

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


mod-aux : nat -> nat -> nat -> nat
mod-aux O y z = y
mod-aux (S x) y z = matita-basics-bool.match-bool lzero (λ (X---v : matita-basics-bool.bool) -> nat) y (mod-aux x (minus y (S z)) z) (leb y z)

mod : (X-- : nat) -> (X--1 : nat) -> nat
mod = λ (n : nat) -> λ (m : nat) -> match-nat lzero (λ (X-- : nat) -> nat) n (λ (p : nat) -> mod-aux n n p) m


div-aux : nat -> nat -> nat -> nat
div-aux O y z = O
div-aux (S x) y z = matita-basics-bool.match-bool lzero (λ (X---v : matita-basics-bool.bool) -> nat) O (S (div-aux x (minus y (S z)) z)) (leb y z)


div : (X-- : nat) -> (X--1 : nat) -> nat
div = λ (n : nat) -> λ (m : nat) -> match-nat lzero (λ (X-- : nat) -> nat) (S n) (λ (p : nat) -> div-aux n n p) m

le-mod-aux-m-m : (p : nat) -> (n : nat) -> (m : nat) -> (X-- : le n p) -> le (mod-aux p n m) m
le-mod-aux-m-m = λ (p : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (n : nat) -> (m : nat) -> (X-- : le n X-x-365) -> le (mod-aux X-x-365 n m) m) (λ (n : nat) -> λ (m : nat) -> λ (lenO : le n O) -> le-n-O-elim lzero n lenO (λ (X-- : nat) -> le X-- m) (le-O-n m)) (λ (q : nat) -> λ (Hind : (n : nat) -> (m : nat) -> (X-- : le n q) -> le (mod-aux q n m) m) -> λ (n : nat) -> λ (m : nat) -> λ (len : le n (S q)) -> leb-elim lzero n m (λ (X-- : bool) -> le (match-bool lzero (λ (X-0 : bool) -> nat) n (mod-aux q (minus n (S m)) m) X--) m) (λ (auto : le n m) -> auto) (λ (notlenm : Not lzero (le n m)) -> Hind (minus n (S m)) m (le-plus-to-minus n (S m) q (transitive-le n (S q) (plus q (S m)) len (eq-coerc lzero (le (S q) (plus (S q) m)) (le (S q) (plus q (S m))) (le-plus-n-r m (S q)) (rewrite-l lzero (lsuc lzero) nat (plus m (S q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S q) X--) (le (S q) (plus q (S m)))) (rewrite-r lzero (lsuc lzero) nat (plus q (S m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S q) X--) (le (S q) (plus q (S m)))) (refl (lsuc lzero) (Set (lzero)) (le (S q) (plus q (S m)))) (plus m (S q)) (rewrite-l lzero lzero nat (S (plus m q)) (λ (X-- : nat) -> eq lzero nat X-- (plus q (S m))) (rewrite-l lzero lzero nat (plus q m) (λ (X-- : nat) -> eq lzero nat (S X--) (plus q (S m))) (plus-n-Sm q m) (plus m q) (commutative-plus q m)) (plus m (S q)) (plus-n-Sm m q))) (plus (S q) m) (commutative-plus m (S q)))))))) p

lt-mod-m-m : (n : nat) -> (m : nat) -> (X-- : lt O m) -> lt (mod n m) m
lt-mod-m-m = λ (n : nat) -> λ (m : nat) -> match-nat lzero (λ (X-- : nat) -> (X--1 : lt O X--) -> lt (mod n X--) X--) (λ (abs : lt O O) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt (mod n O) O) (absurd lzero (le (S O) O) abs (not-le-Sn-O O))) (λ (p : nat) -> λ (X-- : lt O (S p)) -> le-S-S (mod-aux n n p) p (le-mod-aux-m-m n n p (le-n n))) m

div-aux-mod-aux : (p : nat) -> (n : nat) -> (m : nat) -> eq lzero nat n (plus (times (div-aux p n m) (S m)) (mod-aux p n m))
div-aux-mod-aux = λ (p : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (n : nat) -> (m : nat) -> eq lzero nat n (plus (times (div-aux X-x-365 n m) (S m)) (mod-aux X-x-365 n m))) (λ (n : nat) -> λ (m : nat) -> refl lzero nat n) (λ (q : nat) -> λ (Hind : (n : nat) -> (m : nat) -> eq lzero nat n (plus (times (div-aux q n m) (S m)) (mod-aux q n m))) -> λ (n : nat) -> λ (m : nat) -> leb-elim lzero n m (λ (X-- : bool) -> eq lzero nat n (plus (times (match-bool lzero (λ (X-0 : bool) -> nat) O (S (div-aux q (minus n (S m)) m)) X--) (S m)) (match-bool lzero (λ (X-0 : bool) -> nat) n (mod-aux q (minus n (S m)) m) X--))) (λ (lenm : le n m) -> refl lzero nat n) (λ (lenm : Not lzero (le n m)) -> eq-ind-r lzero lzero nat (plus m (plus (times (div-aux q (minus n (S m)) m) (S m)) (mod-aux q (minus n (S m)) m))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m (plus (times (div-aux q (minus n (S m)) m) (S m)) (mod-aux q (minus n (S m)) m)))) -> eq lzero nat n (S x)) (eq-ind lzero lzero nat (minus n (S m)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (minus n (S m)) x-1) -> eq lzero nat n (S (plus m x-1))) (eq-coerc lzero (eq lzero nat n (plus (minus n (S m)) (S m))) (eq lzero nat n (S (plus m (minus n (S m))))) (plus-minus-m-m n (S m) (not-le-to-lt n m lenm)) (rewrite-r lzero (lsuc lzero) nat (pred (minus n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat n (plus X-- (S m))) (eq lzero nat n (S (plus m (minus n (S m)))))) (rewrite-r lzero (lsuc lzero) nat (pred (minus n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat n (plus (pred (minus n m)) (S m))) (eq lzero nat n (S (plus m X--)))) (rewrite-r lzero (lsuc lzero) nat (plus m (S (pred (minus n m)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat n (plus (pred (minus n m)) (S m))) (eq lzero nat n X--)) (rewrite-r lzero (lsuc lzero) nat (plus m (S (pred (minus n m)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat n X--) (eq lzero nat n (plus m (S (pred (minus n m)))))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat n (plus m (S (pred (minus n m)))))) (plus (pred (minus n m)) (S m)) (rewrite-l lzero lzero nat (S (plus (pred (minus n m)) m)) (λ (X-- : nat) -> eq lzero nat X-- (plus m (S (pred (minus n m))))) (rewrite-l lzero lzero nat (plus m (pred (minus n m))) (λ (X-- : nat) -> eq lzero nat (S X--) (plus m (S (pred (minus n m))))) (plus-n-Sm m (pred (minus n m))) (plus (pred (minus n m)) m) (commutative-plus m (pred (minus n m)))) (plus (pred (minus n m)) (S m)) (plus-n-Sm (pred (minus n m)) m))) (S (plus m (pred (minus n m)))) (plus-n-Sm m (pred (minus n m)))) (minus n (S m)) (eq-minus-S-pred n m)) (minus n (S m)) (eq-minus-S-pred n m))) (plus (times (div-aux q (minus n (S m)) m) (S m)) (mod-aux q (minus n (S m)) m)) (Hind (minus n (S m)) m)) (plus (plus m (times (div-aux q (minus n (S m)) m) (S m))) (mod-aux q (minus n (S m)) m)) (associative-plus m (times (div-aux q (minus n (S m)) m) (S m)) (mod-aux q (minus n (S m)) m)))) p

div-mod : (n : nat) -> (m : nat) -> eq lzero nat n (plus (times (div n m) m) (mod n m))
div-mod = λ (n : nat) -> λ (m : nat) -> match-nat lzero (λ (X-- : nat) -> eq lzero nat n (plus (times (div n X--) X--) (mod n X--))) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat n (plus X-- n)) (rewrite-r lzero lzero nat (plus n O) (λ (X-- : nat) -> eq lzero nat 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)) (plus O n) (commutative-plus O n)) (times n O) (times-n-O n)) (λ (auto : nat) -> rewrite-r lzero lzero nat (plus (times (div-aux n n auto) (S auto)) (mod-aux n n auto)) (λ (X-- : nat) -> eq lzero nat X-- (plus (times (div-aux n n auto) (S auto)) (mod-aux n n auto))) (refl lzero nat (plus (times (div-aux n n auto) (S auto)) (mod-aux n n auto))) n (div-aux-mod-aux n n auto)) m

eq-times-div-minus-mod : (a : nat) -> (b : nat) -> eq lzero nat (times (div a b) b) (minus a (mod a b))
eq-times-div-minus-mod = λ (a : nat) -> λ (b : nat) -> eq-coerc lzero (eq lzero nat (times b (div a b)) (minus (plus (times b (div a b)) (mod a b)) (mod a b))) (eq lzero nat (times (div a b) b) (minus a (mod a b))) (minus-plus-m-m (times b (div a b)) (mod a b)) (rewrite-r lzero (lsuc lzero) nat (plus (mod a b) (times b (div a b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (times b (div a b)) (minus X-- (mod a b))) (eq lzero nat (times (div a b) b) (minus a (mod a b)))) (rewrite-r lzero (lsuc lzero) nat (times b (div a b)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (times b (div a b)) (minus (plus (mod a b) (times b (div a b))) (mod a b))) (eq lzero nat X-- (minus a (mod a b)))) (rewrite-l lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (times b (div a b)) (minus X-- (mod a b))) (eq lzero nat (times b (div a b)) (minus a (mod a b)))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (times b (div a b)) (minus a (mod a b)))) (plus (mod a b) (times b (div a b))) (rewrite-l lzero lzero nat (plus (times b (div a b)) (mod a b)) (λ (X-- : nat) -> eq lzero nat a X--) (rewrite-l lzero lzero nat (times (div a b) b) (λ (X-- : nat) -> eq lzero nat a (plus X-- (mod a b))) (div-mod a b) (times b (div a b)) (commutative-times (div a b) b)) (plus (mod a b) (times b (div a b))) (commutative-plus (times b (div a b)) (mod a b)))) (times (div a b) b) (commutative-times (div a b) b)) (plus (times b (div a b)) (mod a b)) (commutative-plus (times b (div a b)) (mod a b)))

data div-mod-spec (n-v : nat) (m-v : nat) (q-v : nat)  (r-v : nat) : Set where
  div-mod-spec-intro' : (X---v : lt r-v m-v) -> (X--1-v : matita-basics-logic.eq lzero nat n-v (plus (times q-v m-v) r-v)) -> div-mod-spec n-v m-v q-v r-v

div-mod-spec-intro : (n-v : nat) -> (m-v : nat) -> (q-v : nat) -> (r-v : nat) -> (X---v : lt r-v m-v) -> (X--1-v : matita-basics-logic.eq lzero nat n-v (plus (times q-v m-v) r-v)) -> div-mod-spec n-v m-v q-v r-v
div-mod-spec-intro _ _ _ _ = div-mod-spec-intro'

match-div-mod-spec : (X-n-v : nat) -> (X-m-v : nat) -> (X-q-v : nat) -> (X-r-v : nat) -> (return-sort-v : Level) -> (return-type-v : (z-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Set return-sort-v) -> (case-div-mod-spec-intro-v : (X---v : lt X-r-v X-m-v) -> (X--1-v : matita-basics-logic.eq lzero nat X-n-v (plus (times X-q-v X-m-v) X-r-v)) -> return-type-v (div-mod-spec-intro X-n-v X-m-v X-q-v X-r-v X---v X--1-v)) -> (z-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> return-type-v z-v
match-div-mod-spec X-n-12-v X-m-11-v X-q-10-v X-r-9-v return-sort-v return-type-v case-div-mod-spec-intro-v (div-mod-spec-intro' X---v X--1-v) = case-div-mod-spec-intro-v X---v X--1-v

div-mod-spec-ind : (l2-v : Level) -> (X-n-v : nat) -> (X-m-v : nat) -> (X-q-v : nat) -> (X-r-v : nat) -> (Q--v : (X-x-809-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Set l2-v) -> (X-H-div-mod-spec-intro-v : (x-811-v : lt X-r-v X-m-v) -> (x-810-v : matita-basics-logic.eq lzero nat X-n-v (plus (times X-q-v X-m-v) X-r-v)) -> Q--v (div-mod-spec-intro X-n-v X-m-v X-q-v X-r-v x-811-v x-810-v)) -> (x-809-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Q--v x-809-v
div-mod-spec-ind X-n-12-v X-m-11-v X-q-10-v X-r-9-v return-sort-v return-type-v case-div-mod-spec-intro-v (div-mod-spec-intro' X---v X--1-v) = case-div-mod-spec-intro-v X---v X--1-v

div-mod-spec-rect-Type4 : (l2-v : Level) -> (X-n-v : nat) -> (X-m-v : nat) -> (X-q-v : nat) -> (X-r-v : nat) -> (Q--v : (X-x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Set l2-v) -> (X-H-div-mod-spec-intro-v : (x-815-v : lt X-r-v X-m-v) -> (x-814-v : matita-basics-logic.eq lzero nat X-n-v (plus (times X-q-v X-m-v) X-r-v)) -> Q--v (div-mod-spec-intro X-n-v X-m-v X-q-v X-r-v x-815-v x-814-v)) -> (x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Q--v x-813-v
div-mod-spec-rect-Type4 X-n-12-v X-m-11-v X-q-10-v X-r-9-v return-sort-v return-type-v case-div-mod-spec-intro-v (div-mod-spec-intro' X---v X--1-v) = case-div-mod-spec-intro-v X---v X--1-v

div-mod-spec-rect-Type3 : (l2-v : Level) -> (X-n-v : nat) -> (X-m-v : nat) -> (X-q-v : nat) -> (X-r-v : nat) -> (Q--v : (X-x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Set l2-v) -> (X-H-div-mod-spec-intro-v : (x-815-v : lt X-r-v X-m-v) -> (x-814-v : matita-basics-logic.eq lzero nat X-n-v (plus (times X-q-v X-m-v) X-r-v)) -> Q--v (div-mod-spec-intro X-n-v X-m-v X-q-v X-r-v x-815-v x-814-v)) -> (x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Q--v x-813-v
div-mod-spec-rect-Type3 X-n-12-v X-m-11-v X-q-10-v X-r-9-v return-sort-v return-type-v case-div-mod-spec-intro-v (div-mod-spec-intro' X---v X--1-v) = case-div-mod-spec-intro-v X---v X--1-v

div-mod-spec-rect-Type5 : (l2-v : Level) -> (X-n-v : nat) -> (X-m-v : nat) -> (X-q-v : nat) -> (X-r-v : nat) -> (Q--v : (X-x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Set l2-v) -> (X-H-div-mod-spec-intro-v : (x-815-v : lt X-r-v X-m-v) -> (x-814-v : matita-basics-logic.eq lzero nat X-n-v (plus (times X-q-v X-m-v) X-r-v)) -> Q--v (div-mod-spec-intro X-n-v X-m-v X-q-v X-r-v x-815-v x-814-v)) -> (x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Q--v x-813-v
div-mod-spec-rect-Type5 X-n-12-v X-m-11-v X-q-10-v X-r-9-v return-sort-v return-type-v case-div-mod-spec-intro-v (div-mod-spec-intro' X---v X--1-v) = case-div-mod-spec-intro-v X---v X--1-v

div-mod-spec-rect-Type2 : (l2-v : Level) -> (X-n-v : nat) -> (X-m-v : nat) -> (X-q-v : nat) -> (X-r-v : nat) -> (Q--v : (X-x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Set l2-v) -> (X-H-div-mod-spec-intro-v : (x-815-v : lt X-r-v X-m-v) -> (x-814-v : matita-basics-logic.eq lzero nat X-n-v (plus (times X-q-v X-m-v) X-r-v)) -> Q--v (div-mod-spec-intro X-n-v X-m-v X-q-v X-r-v x-815-v x-814-v)) -> (x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Q--v x-813-v
div-mod-spec-rect-Type2 X-n-12-v X-m-11-v X-q-10-v X-r-9-v return-sort-v return-type-v case-div-mod-spec-intro-v (div-mod-spec-intro' X---v X--1-v) = case-div-mod-spec-intro-v X---v X--1-v

div-mod-spec-rect-Type1 : (l2-v : Level) -> (X-n-v : nat) -> (X-m-v : nat) -> (X-q-v : nat) -> (X-r-v : nat) -> (Q--v : (X-x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Set l2-v) -> (X-H-div-mod-spec-intro-v : (x-815-v : lt X-r-v X-m-v) -> (x-814-v : matita-basics-logic.eq lzero nat X-n-v (plus (times X-q-v X-m-v) X-r-v)) -> Q--v (div-mod-spec-intro X-n-v X-m-v X-q-v X-r-v x-815-v x-814-v)) -> (x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Q--v x-813-v
div-mod-spec-rect-Type1 X-n-12-v X-m-11-v X-q-10-v X-r-9-v return-sort-v return-type-v case-div-mod-spec-intro-v (div-mod-spec-intro' X---v X--1-v) = case-div-mod-spec-intro-v X---v X--1-v

div-mod-spec-rect-Type0 : (l2-v : Level) -> (X-n-v : nat) -> (X-m-v : nat) -> (X-q-v : nat) -> (X-r-v : nat) -> (Q--v : (X-x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Set l2-v) -> (X-H-div-mod-spec-intro-v : (x-815-v : lt X-r-v X-m-v) -> (x-814-v : matita-basics-logic.eq lzero nat X-n-v (plus (times X-q-v X-m-v) X-r-v)) -> Q--v (div-mod-spec-intro X-n-v X-m-v X-q-v X-r-v x-815-v x-814-v)) -> (x-813-v : div-mod-spec X-n-v X-m-v X-q-v X-r-v) -> Q--v x-813-v
div-mod-spec-rect-Type0 X-n-12-v X-m-11-v X-q-10-v X-r-9-v return-sort-v return-type-v case-div-mod-spec-intro-v (div-mod-spec-intro' X---v X--1-v) = case-div-mod-spec-intro-v X---v X--1-v



div-mod-spec-inv-ind : (l14 : Level) -> (x1 : nat) -> (x2 : nat) -> (x3 : nat) -> (x4 : nat) -> (Hterm : div-mod-spec x1 x2 x3 x4) -> (P : (X-z1434 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> (X-H1 : (x-811 : lt x4 x2) -> (x-810 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1435 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-811 x-810)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-811 x-810)) -> P Hterm
div-mod-spec-inv-ind = λ (l14 : Level) -> λ (x1 : nat) -> λ (x2 : nat) -> λ (x3 : nat) -> λ (x4 : nat) -> λ (Hterm : div-mod-spec x1 x2 x3 x4) -> λ (P : (X-z1434 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> λ (H1 : (x-811 : lt x4 x2) -> (x-810 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1435 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-811 x-810)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-811 x-810)) -> div-mod-spec-ind l14 x1 x2 x3 x4 (λ (X-x-809 : div-mod-spec x1 x2 x3 x4) -> (X-z1435 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm X-x-809) -> P X-x-809) H1 Hterm (refl lzero (div-mod-spec x1 x2 x3 x4) Hterm)

div-mod-spec-inv-rect-Type4 : (l14 : Level) -> (x1 : nat) -> (x2 : nat) -> (x3 : nat) -> (x4 : nat) -> (Hterm : div-mod-spec x1 x2 x3 x4) -> (P : (X-z1440 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> (X-H1 : (x-815 : lt x4 x2) -> (x-814 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1441 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-815 x-814)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-815 x-814)) -> P Hterm
div-mod-spec-inv-rect-Type4 = λ (l14 : Level) -> λ (x1 : nat) -> λ (x2 : nat) -> λ (x3 : nat) -> λ (x4 : nat) -> λ (Hterm : div-mod-spec x1 x2 x3 x4) -> λ (P : (X-z1440 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> λ (H1 : (x-815 : lt x4 x2) -> (x-814 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1441 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-815 x-814)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-815 x-814)) -> div-mod-spec-rect-Type4 l14 x1 x2 x3 x4 (λ (X-x-813 : div-mod-spec x1 x2 x3 x4) -> (X-z1441 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm X-x-813) -> P X-x-813) H1 Hterm (refl lzero (div-mod-spec x1 x2 x3 x4) Hterm)

div-mod-spec-inv-rect-Type3 : (l14 : Level) -> (x1 : nat) -> (x2 : nat) -> (x3 : nat) -> (x4 : nat) -> (Hterm : div-mod-spec x1 x2 x3 x4) -> (P : (X-z1446 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> (X-H1 : (x-823 : lt x4 x2) -> (x-822 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1447 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-823 x-822)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-823 x-822)) -> P Hterm
div-mod-spec-inv-rect-Type3 = λ (l14 : Level) -> λ (x1 : nat) -> λ (x2 : nat) -> λ (x3 : nat) -> λ (x4 : nat) -> λ (Hterm : div-mod-spec x1 x2 x3 x4) -> λ (P : (X-z1446 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> λ (H1 : (x-823 : lt x4 x2) -> (x-822 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1447 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-823 x-822)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-823 x-822)) -> div-mod-spec-rect-Type3 l14 x1 x2 x3 x4 (λ (X-x-821 : div-mod-spec x1 x2 x3 x4) -> (X-z1447 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm X-x-821) -> P X-x-821) H1 Hterm (refl lzero (div-mod-spec x1 x2 x3 x4) Hterm)

div-mod-spec-inv-rect-Type2 : (l14 : Level) -> (x1 : nat) -> (x2 : nat) -> (x3 : nat) -> (x4 : nat) -> (Hterm : div-mod-spec x1 x2 x3 x4) -> (P : (X-z1452 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> (X-H1 : (x-827 : lt x4 x2) -> (x-826 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1453 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-827 x-826)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-827 x-826)) -> P Hterm
div-mod-spec-inv-rect-Type2 = λ (l14 : Level) -> λ (x1 : nat) -> λ (x2 : nat) -> λ (x3 : nat) -> λ (x4 : nat) -> λ (Hterm : div-mod-spec x1 x2 x3 x4) -> λ (P : (X-z1452 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> λ (H1 : (x-827 : lt x4 x2) -> (x-826 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1453 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-827 x-826)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-827 x-826)) -> div-mod-spec-rect-Type2 l14 x1 x2 x3 x4 (λ (X-x-825 : div-mod-spec x1 x2 x3 x4) -> (X-z1453 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm X-x-825) -> P X-x-825) H1 Hterm (refl lzero (div-mod-spec x1 x2 x3 x4) Hterm)

div-mod-spec-inv-rect-Type1 : (l14 : Level) -> (x1 : nat) -> (x2 : nat) -> (x3 : nat) -> (x4 : nat) -> (Hterm : div-mod-spec x1 x2 x3 x4) -> (P : (X-z1458 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> (X-H1 : (x-831 : lt x4 x2) -> (x-830 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1459 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-831 x-830)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-831 x-830)) -> P Hterm
div-mod-spec-inv-rect-Type1 = λ (l14 : Level) -> λ (x1 : nat) -> λ (x2 : nat) -> λ (x3 : nat) -> λ (x4 : nat) -> λ (Hterm : div-mod-spec x1 x2 x3 x4) -> λ (P : (X-z1458 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> λ (H1 : (x-831 : lt x4 x2) -> (x-830 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1459 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-831 x-830)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-831 x-830)) -> div-mod-spec-rect-Type1 l14 x1 x2 x3 x4 (λ (X-x-829 : div-mod-spec x1 x2 x3 x4) -> (X-z1459 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm X-x-829) -> P X-x-829) H1 Hterm (refl lzero (div-mod-spec x1 x2 x3 x4) Hterm)

div-mod-spec-inv-rect-Type0 : (l14 : Level) -> (x1 : nat) -> (x2 : nat) -> (x3 : nat) -> (x4 : nat) -> (Hterm : div-mod-spec x1 x2 x3 x4) -> (P : (X-z1464 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> (X-H1 : (x-835 : lt x4 x2) -> (x-834 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1465 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-835 x-834)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-835 x-834)) -> P Hterm
div-mod-spec-inv-rect-Type0 = λ (l14 : Level) -> λ (x1 : nat) -> λ (x2 : nat) -> λ (x3 : nat) -> λ (x4 : nat) -> λ (Hterm : div-mod-spec x1 x2 x3 x4) -> λ (P : (X-z1464 : div-mod-spec x1 x2 x3 x4) -> Set l14) -> λ (H1 : (x-835 : lt x4 x2) -> (x-834 : eq lzero nat x1 (plus (times x3 x2) x4)) -> (X-z1465 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm (div-mod-spec-intro x1 x2 x3 x4 x-835 x-834)) -> P (div-mod-spec-intro x1 x2 x3 x4 x-835 x-834)) -> div-mod-spec-rect-Type0 l14 x1 x2 x3 x4 (λ (X-x-833 : div-mod-spec x1 x2 x3 x4) -> (X-z1465 : eq lzero (div-mod-spec x1 x2 x3 x4) Hterm X-x-833) -> P X-x-833) H1 Hterm (refl lzero (div-mod-spec x1 x2 x3 x4) Hterm)

div-mod-spec-discr : (l207 : Level) -> (a1 : nat) -> (a2 : nat) -> (a3 : nat) -> (a4 : nat) -> (x : div-mod-spec a1 a2 a3 a4) -> (y : div-mod-spec a1 a2 a3 a4) -> (X-e : eq lzero (div-mod-spec a1 a2 a3 a4) x y) -> match-div-mod-spec a1 a2 a3 a4 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l207))) (λ (X-- : div-mod-spec a1 a2 a3 a4) -> Set ((lsuc lzero) ⊔ (lsuc l207))) (λ (t0 : lt a4 a2) -> λ (t1 : eq lzero nat a1 (plus (times a3 a2) a4)) -> match-div-mod-spec a1 a2 a3 a4 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l207))) (λ (X-- : div-mod-spec a1 a2 a3 a4) -> Set ((lsuc lzero) ⊔ (lsuc l207))) (λ (u0 : lt a4 a2) -> λ (u1 : eq lzero nat a1 (plus (times a3 a2) a4)) -> (P : Set l207) -> (X-z53 : (e0 : eq lzero (lt a4 a2) (R0 lzero (lt a4 a2) t0) u0) -> (X-e1 : eq lzero (eq lzero nat a1 (plus (times a3 a2) a4)) (R1 lzero lzero (lt a4 a2) t0 (λ (x-19 : lt a4 a2) -> λ (X-x-20 : eq lzero (lt a4 a2) t0 x-19) -> eq lzero nat a1 (plus (times a3 a2) a4)) t1 u0 e0) u1) -> P) -> P) y) x
div-mod-spec-discr = λ (l207 : Level) -> λ (a1 : nat) -> λ (a2 : nat) -> λ (a3 : nat) -> λ (a4 : nat) -> λ (x : div-mod-spec a1 a2 a3 a4) -> λ (y : div-mod-spec a1 a2 a3 a4) -> λ (Deq : eq lzero (div-mod-spec a1 a2 a3 a4) x y) -> eq-rect-Type2 lzero ((lsuc lzero) ⊔ (lsuc l207)) (div-mod-spec a1 a2 a3 a4) x (λ (x-13 : div-mod-spec a1 a2 a3 a4) -> λ (X-x-14 : eq lzero (div-mod-spec a1 a2 a3 a4) x x-13) -> match-div-mod-spec a1 a2 a3 a4 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l207))) (λ (X-- : div-mod-spec a1 a2 a3 a4) -> Set ((lsuc lzero) ⊔ (lsuc l207))) (λ (t0 : lt a4 a2) -> λ (t1 : eq lzero nat a1 (plus (times a3 a2) a4)) -> match-div-mod-spec a1 a2 a3 a4 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l207))) (λ (X-- : div-mod-spec a1 a2 a3 a4) -> Set ((lsuc lzero) ⊔ (lsuc l207))) (λ (u0 : lt a4 a2) -> λ (u1 : eq lzero nat a1 (plus (times a3 a2) a4)) -> (P : Set l207) -> (X-z53 : (e0 : eq lzero (lt a4 a2) (R0 lzero (lt a4 a2) t0) u0) -> (X-e1 : eq lzero (eq lzero nat a1 (plus (times a3 a2) a4)) (R1 lzero lzero (lt a4 a2) t0 (λ (x-19 : lt a4 a2) -> λ (X-x-20 : eq lzero (lt a4 a2) t0 x-19) -> eq lzero nat a1 (plus (times a3 a2) a4)) t1 u0 e0) u1) -> P) -> P) x-13) x) (match-div-mod-spec a1 a2 a3 a4 ((lsuc lzero) ⊔ (lsuc l207)) (λ (X-- : div-mod-spec a1 a2 a3 a4) -> match-div-mod-spec a1 a2 a3 a4 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l207))) (λ (X-0 : div-mod-spec a1 a2 a3 a4) -> Set ((lsuc lzero) ⊔ (lsuc l207))) (λ (t0 : lt a4 a2) -> λ (t1 : eq lzero nat a1 (plus (times a3 a2) a4)) -> match-div-mod-spec a1 a2 a3 a4 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l207))) (λ (X-0 : div-mod-spec a1 a2 a3 a4) -> Set ((lsuc lzero) ⊔ (lsuc l207))) (λ (u0 : lt a4 a2) -> λ (u1 : eq lzero nat a1 (plus (times a3 a2) a4)) -> (P : Set l207) -> (X-z53 : (e0 : eq lzero (lt a4 a2) (R0 lzero (lt a4 a2) t0) u0) -> (X-e1 : eq lzero (eq lzero nat a1 (plus (times a3 a2) a4)) (R1 lzero lzero (lt a4 a2) t0 (λ (x-19 : lt a4 a2) -> λ (X-x-20 : eq lzero (lt a4 a2) t0 x-19) -> eq lzero nat a1 (plus (times a3 a2) a4)) t1 u0 e0) u1) -> P) -> P) X--) X--) (λ (a0 : lt a4 a2) -> λ (a10 : eq lzero nat a1 (plus (times a3 a2) a4)) -> λ (P : Set l207) -> λ (DH : (e0 : eq lzero (lt a4 a2) (R0 lzero (lt a4 a2) a0) a0) -> (X-e1 : eq lzero (eq lzero nat a1 (plus (times a3 a2) a4)) (R1 lzero lzero (lt a4 a2) a0 (λ (x-19 : lt a4 a2) -> λ (X-x-20 : eq lzero (lt a4 a2) a0 x-19) -> eq lzero nat a1 (plus (times a3 a2) a4)) a10 a0 e0) a10) -> P) -> DH (refl lzero (lt a4 a2) (R0 lzero (lt a4 a2) a0)) (refl lzero (eq lzero nat a1 (plus (times a3 a2) a4)) (R1 lzero lzero (lt a4 a2) a0 (λ (x-19 : lt a4 a2) -> λ (X-x-20 : eq lzero (lt a4 a2) a0 x-19) -> eq lzero nat a1 (plus (times a3 a2) a4)) a10 a0 (refl lzero (lt a4 a2) (R0 lzero (lt a4 a2) a0))))) x) y Deq

div-mod-spec-to-not-eq-O : (n : nat) -> (m : nat) -> (q : nat) -> (r : nat) -> (X-- : div-mod-spec n m q r) -> Not lzero (eq lzero nat m O)
div-mod-spec-to-not-eq-O = λ (n : nat) -> λ (m : nat) -> λ (q : nat) -> λ (r : nat) -> λ (X-clearme : div-mod-spec n m q r) -> match-div-mod-spec n m q r lzero (λ (X-- : div-mod-spec n m q r) -> Not lzero (eq lzero nat m O)) (λ (auto : lt r m) -> λ (auto' : eq lzero nat n (plus (times q m) r)) -> not-to-not lzero (eq lzero nat m O) (le (S n) O) (λ (auto'' : eq lzero nat m O) -> eq-coerc lzero (le (S r) m) (le (S n) O) auto (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S X--) m) (le (S n) O)) (rewrite-l lzero (lsuc lzero) nat m (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (S n) m) (le (S n) X--)) (refl (lsuc lzero) (Set (lzero)) (le (S n) m)) O auto'') r (rewrite-r lzero lzero nat (plus m r) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-r lzero lzero nat (times m q) (λ (X-- : nat) -> eq lzero nat n (plus X-- r)) (rewrite-l lzero lzero nat (times q m) (λ (X-- : nat) -> eq lzero nat n (plus X-- r)) auto' (times m q) (commutative-times q m)) m (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero nat m (times X-- q)) (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero nat X-- (times O q)) (times-O-n q) m auto'') m auto'')) r (rewrite-r lzero lzero nat O (λ (X-- : nat) -> eq lzero nat r (plus X-- r)) (plus-O-n r) m auto'')))) (not-le-Sn-O n)) X-clearme

div-mod-spec-div-mod : (n : nat) -> (m : nat) -> (X-- : lt O m) -> div-mod-spec n m (div n m) (mod n m)
div-mod-spec-div-mod = λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> div-mod-spec-intro n m (div n m) (mod n m) (lt-mod-m-m n m posm) (rewrite-r lzero lzero nat (times m (div n m)) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n m))) (rewrite-r lzero lzero nat (plus (mod n m) (times m (div n m))) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (plus (mod n m) (times m (div n m))) (rewrite-l lzero lzero nat (plus (times m (div n m)) (mod n m)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n m) m) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n m))) (div-mod n m) (times m (div n m)) (commutative-times (div n m) m)) (plus (mod n m) (times m (div n m))) (commutative-plus (times m (div n m)) (mod n m)))) (plus (times m (div n m)) (mod n m)) (commutative-plus (times m (div n m)) (mod n m))) (times (div n m) m) (commutative-times (div n m) m))

let-clause-1078 : (a : nat) -> (b : nat) -> (q : nat) -> (r : nat) -> (q1 : nat) -> (r1 : nat) -> (X-clearme : div-mod-spec a b q r) -> (ltrb : lt r b) -> (spec : eq lzero nat a (plus (times q b) r)) -> (X-clearme0 : div-mod-spec a b q1 r1) -> (ltr1b : lt r1 b) -> (spec1 : eq lzero nat a (plus (times q1 b) r1)) -> (leqq1 : le q q1) -> (ltqq1 : lt q q1) -> eq lzero nat a (plus r (times b q))
let-clause-1078 = λ (a : nat) -> λ (b : nat) -> λ (q : nat) -> λ (r : nat) -> λ (q1 : nat) -> λ (r1 : nat) -> λ (X-clearme : div-mod-spec a b q r) -> λ (ltrb : lt r b) -> λ (spec : eq lzero nat a (plus (times q b) r)) -> λ (X-clearme0 : div-mod-spec a b q1 r1) -> λ (ltr1b : lt r1 b) -> λ (spec1 : eq lzero nat a (plus (times q1 b) r1)) -> λ (leqq1 : le q q1) -> λ (ltqq1 : lt q q1) -> rewrite-l lzero lzero nat (plus (times b q) r) (λ (X-- : nat) -> eq lzero nat a X--) (rewrite-l lzero lzero nat (times q b) (λ (X-- : nat) -> eq lzero nat a (plus X-- r)) spec (times b q) (commutative-times q b)) (plus r (times b q)) (commutative-plus (times b q) r)

let-clause-1062 : (a : nat) -> (b : nat) -> (q : nat) -> (r : nat) -> (q1 : nat) -> (r1 : nat) -> (X-clearme : div-mod-spec a b q r) -> (ltrb : lt r b) -> (spec : eq lzero nat a (plus (times q b) r)) -> (X-clearme0 : div-mod-spec a b q1 r1) -> (ltr1b : lt r1 b) -> (spec1 : eq lzero nat a (plus (times q1 b) r1)) -> (leqq1 : Not lzero (le q q1)) -> eq lzero nat a (plus r1 (times b q1))
let-clause-1062 = λ (a : nat) -> λ (b : nat) -> λ (q : nat) -> λ (r : nat) -> λ (q1 : nat) -> λ (r1 : nat) -> λ (X-clearme : div-mod-spec a b q r) -> λ (ltrb : lt r b) -> λ (spec : eq lzero nat a (plus (times q b) r)) -> λ (X-clearme0 : div-mod-spec a b q1 r1) -> λ (ltr1b : lt r1 b) -> λ (spec1 : eq lzero nat a (plus (times q1 b) r1)) -> λ (leqq1 : Not lzero (le q q1)) -> rewrite-l lzero lzero nat (plus (times b q1) r1) (λ (X-- : nat) -> eq lzero nat a X--) (rewrite-l lzero lzero nat (times q1 b) (λ (X-- : nat) -> eq lzero nat a (plus X-- r1)) spec1 (times b q1) (commutative-times q1 b)) (plus r1 (times b q1)) (commutative-plus (times b q1) r1)

div-mod-spec-to-eq : (a : nat) -> (b : nat) -> (q : nat) -> (r : nat) -> (q1 : nat) -> (r1 : nat) -> (X-- : div-mod-spec a b q r) -> (X--1 : div-mod-spec a b q1 r1) -> eq lzero nat q q1
div-mod-spec-to-eq = λ (a : nat) -> λ (b : nat) -> λ (q : nat) -> λ (r : nat) -> λ (q1 : nat) -> λ (r1 : nat) -> λ (X-clearme : div-mod-spec a b q r) -> match-div-mod-spec a b q r lzero (λ (X-- : div-mod-spec a b q r) -> (X--1 : div-mod-spec a b q1 r1) -> eq lzero nat q q1) (λ (ltrb : lt r b) -> λ (spec : eq lzero nat a (plus (times q b) r)) -> λ (X-clearme0 : div-mod-spec a b q1 r1) -> match-div-mod-spec a b q1 r1 lzero (λ (X-- : div-mod-spec a b q1 r1) -> eq lzero nat q q1) (λ (ltr1b : lt r1 b) -> λ (spec1 : eq lzero nat a (plus (times q1 b) r1)) -> leb-elim lzero q q1 (λ (X-- : bool) -> eq lzero nat q q1) (λ (leqq1 : le q q1) -> Or-ind lzero lzero lzero (lt q q1) (eq lzero nat q q1) (λ (X-x-170 : Or lzero lzero (lt q q1) (eq lzero nat q q1)) -> eq lzero nat q q1) (λ (ltqq1 : lt q q1) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat q q1) (absurd lzero (le (S a) a) (lt-to-le-to-lt a (times (S q) b) a (eq-ind-r lzero lzero nat (plus (times q b) r) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times q b) r)) -> lt x (times (S q) b)) (eq-coerc lzero (lt (plus (times q b) r) (plus (times q b) b)) (lt (plus (times q b) r) (times (S q) b)) (monotonic-lt-plus-r (times q b) r b ltrb) (rewrite-r lzero (lsuc lzero) nat (times b q) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus X-- r) (plus X-- b)) (lt (plus X-- r) (times (S q) b))) (rewrite-r lzero (lsuc lzero) nat (plus r (times b q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (times b q) r) (plus (times b q) b)) (lt X-- (times (S q) b))) (rewrite-l lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (times b q) r) (plus (times b q) b)) (lt X-- (times (S q) b))) (rewrite-r lzero (lsuc lzero) nat (times b (S q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (times b q) r) (plus (times b q) b)) (lt a X--)) (rewrite-l lzero (lsuc lzero) nat (plus b (times b q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (times b q) r) (plus (times b q) b)) (lt a X--)) (rewrite-r lzero (lsuc lzero) nat (plus r (times b q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (times b q) b)) (lt a (plus b (times b q)))) (rewrite-l lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (times b q) b)) (lt a (plus b (times b q)))) (rewrite-r lzero (lsuc lzero) nat (plus b (times b q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt a X--) (lt a (plus b (times b q)))) (refl (lsuc lzero) (Set (lzero)) (lt a (plus b (times b q)))) (plus (times b q) b) (commutative-plus (times b q) b)) (plus r (times b q)) (let-clause-1078 a b q r q1 r1 X-clearme ltrb spec X-clearme0 ltr1b spec1 leqq1 ltqq1)) (plus (times b q) r) (commutative-plus (times b q) r)) (times b (S q)) (times-n-Sm b q)) (times (S q) b) (commutative-times (S q) b)) (plus r (times b q)) (let-clause-1078 a b q r q1 r1 X-clearme ltrb spec X-clearme0 ltr1b spec1 leqq1 ltqq1)) (plus (times b q) r) (commutative-plus (times b q) r)) (times q b) (commutative-times q b))) a spec) (transitive-le (times (S q) b) (times q1 b) a (eq-coerc lzero (le (times b (S q)) (times b q1)) (le (times (S q) b) (times q1 b)) (monotonic-le-times-r b (S q) q1 ltqq1) (rewrite-r lzero (lsuc lzero) nat (times b (S q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (S q)) (times b q1)) (le X-- (times q1 b))) (rewrite-l lzero (lsuc lzero) nat (plus b (times b q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (S q)) (times b q1)) (le X-- (times q1 b))) (rewrite-r lzero (lsuc lzero) nat (times b q1) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (S q)) (times b q1)) (le (plus b (times b q)) X--)) (rewrite-l lzero (lsuc lzero) nat (plus b (times b q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times b q1)) (le (plus b (times b q)) (times b q1))) (refl (lsuc lzero) (Set (lzero)) (le (plus b (times b q)) (times b q1))) (times b (S q)) (times-n-Sm b q)) (times q1 b) (commutative-times q1 b)) (times b (S q)) (times-n-Sm b q)) (times (S q) b) (commutative-times (S q) b))) (eq-coerc lzero (le (times q1 b) (plus (times q1 b) r1)) (le (times q1 b) a) (le-plus-n-r r1 (times q1 b)) (rewrite-r lzero (lsuc lzero) nat (times b q1) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus X-- r1)) (le X-- a)) (rewrite-r lzero (lsuc lzero) nat (plus r1 (times b q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b q1) X--) (le (times b q1) a)) (rewrite-l lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b q1) X--) (le (times b q1) a)) (refl (lsuc lzero) (Set (lzero)) (le (times b q1) a)) (plus r1 (times b q1)) (rewrite-l lzero lzero nat (plus (times b q1) r1) (λ (X-- : nat) -> eq lzero nat a X--) (rewrite-l lzero lzero nat (times q1 b) (λ (X-- : nat) -> eq lzero nat a (plus X-- r1)) spec1 (times b q1) (commutative-times q1 b)) (plus r1 (times b q1)) (commutative-plus (times b q1) r1))) (plus (times b q1) r1) (commutative-plus (times b q1) r1)) (times q1 b) (commutative-times q1 b))))) (not-le-Sn-n a))) (λ (X-x-172 : eq lzero nat q q1) -> rewrite-l lzero lzero nat q (λ (X-- : nat) -> eq lzero nat q X--) (refl lzero nat q) q1 X-x-172) (le-to-or-lt-eq q q1 leqq1)) (λ (leqq1 : Not lzero (le q q1)) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat q q1) (absurd lzero (le (S a) a) (lt-to-le-to-lt a (times (S q1) b) a (eq-ind-r lzero lzero nat (plus (times q1 b) r1) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times q1 b) r1)) -> lt x (times (S q1) b)) (eq-coerc lzero (lt (plus (times q1 b) r1) (plus (times q1 b) b)) (lt (plus (times q1 b) r1) (times (S q1) b)) (monotonic-lt-plus-r (times q1 b) r1 b ltr1b) (rewrite-r lzero (lsuc lzero) nat (times b q1) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus X-- r1) (plus X-- b)) (lt (plus X-- r1) (times (S q1) b))) (rewrite-r lzero (lsuc lzero) nat (plus r1 (times b q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (times b q1) r1) (plus (times b q1) b)) (lt X-- (times (S q1) b))) (rewrite-l lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (times b q1) r1) (plus (times b q1) b)) (lt X-- (times (S q1) b))) (rewrite-r lzero (lsuc lzero) nat (times b (S q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (times b q1) r1) (plus (times b q1) b)) (lt a X--)) (rewrite-l lzero (lsuc lzero) nat (plus b (times b q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (times b q1) r1) (plus (times b q1) b)) (lt a X--)) (rewrite-r lzero (lsuc lzero) nat (plus r1 (times b q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (times b q1) b)) (lt a (plus b (times b q1)))) (rewrite-l lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (times b q1) b)) (lt a (plus b (times b q1)))) (rewrite-r lzero (lsuc lzero) nat (plus b (times b q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt a X--) (lt a (plus b (times b q1)))) (refl (lsuc lzero) (Set (lzero)) (lt a (plus b (times b q1)))) (plus (times b q1) b) (commutative-plus (times b q1) b)) (plus r1 (times b q1)) (let-clause-1062 a b q r q1 r1 X-clearme ltrb spec X-clearme0 ltr1b spec1 leqq1)) (plus (times b q1) r1) (commutative-plus (times b q1) r1)) (times b (S q1)) (times-n-Sm b q1)) (times (S q1) b) (commutative-times (S q1) b)) (plus r1 (times b q1)) (let-clause-1062 a b q r q1 r1 X-clearme ltrb spec X-clearme0 ltr1b spec1 leqq1)) (plus (times b q1) r1) (commutative-plus (times b q1) r1)) (times q1 b) (commutative-times q1 b))) a spec1) (transitive-le (times (S q1) b) (times q b) a (eq-coerc lzero (le (times b (S q1)) (times b q)) (le (times (S q1) b) (times q b)) (monotonic-le-times-r b (S q1) q (not-le-to-lt q q1 leqq1)) (rewrite-r lzero (lsuc lzero) nat (times b (S q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (S q1)) (times b q)) (le X-- (times q b))) (rewrite-l lzero (lsuc lzero) nat (plus b (times b q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (S q1)) (times b q)) (le X-- (times q b))) (rewrite-r lzero (lsuc lzero) nat (times b q) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b (S q1)) (times b q)) (le (plus b (times b q1)) X--)) (rewrite-l lzero (lsuc lzero) nat (plus b (times b q1)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times b q)) (le (plus b (times b q1)) (times b q))) (refl (lsuc lzero) (Set (lzero)) (le (plus b (times b q1)) (times b q))) (times b (S q1)) (times-n-Sm b q1)) (times q b) (commutative-times q b)) (times b (S q1)) (times-n-Sm b q1)) (times (S q1) b) (commutative-times (S q1) b))) (eq-coerc lzero (le (times q b) (plus (times q b) r)) (le (times q b) a) (le-plus-n-r r (times q b)) (rewrite-r lzero (lsuc lzero) nat (times b q) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus X-- r)) (le X-- a)) (rewrite-r lzero (lsuc lzero) nat (plus r (times b q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b q) X--) (le (times b q) a)) (rewrite-l lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b q) X--) (le (times b q) a)) (refl (lsuc lzero) (Set (lzero)) (le (times b q) a)) (plus r (times b q)) (rewrite-l lzero lzero nat (plus (times b q) r) (λ (X-- : nat) -> eq lzero nat a X--) (rewrite-l lzero lzero nat (times q b) (λ (X-- : nat) -> eq lzero nat a (plus X-- r)) spec (times b q) (commutative-times q b)) (plus r (times b q)) (commutative-plus (times b q) r))) (plus (times b q) r) (commutative-plus (times b q) r)) (times q b) (commutative-times q b))))) (not-le-Sn-n a)))) X-clearme0) X-clearme

div-mod-spec-to-eq2 : (a : nat) -> (b : nat) -> (q : nat) -> (r : nat) -> (q1 : nat) -> (r1 : nat) -> (X-- : div-mod-spec a b q r) -> (X--1 : div-mod-spec a b q1 r1) -> eq lzero nat r r1
div-mod-spec-to-eq2 = λ (a : nat) -> λ (b : nat) -> λ (q : nat) -> λ (r : nat) -> λ (q1 : nat) -> λ (r1 : nat) -> λ (spec : div-mod-spec a b q r) -> λ (spec1 : div-mod-spec a b q1 r1) -> div-mod-spec-ind lzero a b q r (λ (X-x-809 : div-mod-spec a b q r) -> eq lzero nat r r1) (λ (X-- : lt r b) -> λ (eqa : eq lzero nat a (plus (times q b) r)) -> div-mod-spec-ind lzero a b q1 r1 (λ (X-x-809 : div-mod-spec a b q1 r1) -> eq lzero nat r r1) (λ (X-0 : lt r1 b) -> λ (eqa1 : eq lzero nat a (plus (times q1 b) r1)) -> injective-plus-r (times q b) r r1 (rewrite-r lzero lzero nat (times b q) (λ (X--1 : nat) -> eq lzero nat (plus X--1 r) (plus (times q b) r1)) (rewrite-r lzero lzero nat (plus r (times b q)) (λ (X--1 : nat) -> eq lzero nat X--1 (plus (times q b) r1)) (rewrite-l lzero lzero nat a (λ (X--1 : nat) -> eq lzero nat X--1 (plus (times q b) r1)) (rewrite-r lzero lzero nat (times b q) (λ (X--1 : nat) -> eq lzero nat a (plus X--1 r1)) (rewrite-r lzero lzero nat (plus r1 (times b q)) (λ (X--1 : nat) -> eq lzero nat a X--1) (rewrite-l lzero lzero nat a (λ (X--1 : nat) -> eq lzero nat a X--1) (refl lzero nat a) (plus r1 (times b q)) (rewrite-r lzero lzero nat q1 (λ (X--1 : nat) -> eq lzero nat a (plus r1 (times b X--1))) (rewrite-l lzero lzero nat (plus (times b q1) r1) (λ (X--1 : nat) -> eq lzero nat a X--1) (rewrite-l lzero lzero nat (times q1 b) (λ (X--1 : nat) -> eq lzero nat a (plus X--1 r1)) eqa1 (times b q1) (commutative-times q1 b)) (plus r1 (times b q1)) (commutative-plus (times b q1) r1)) q (div-mod-spec-to-eq a b q r q1 r1 spec spec1))) (plus (times b q) r1) (commutative-plus (times b q) r1)) (times q b) (commutative-times q b)) (plus r (times b q)) (rewrite-l lzero lzero nat (plus (times b q) r) (λ (X--1 : nat) -> eq lzero nat a X--1) (rewrite-l lzero lzero nat (times q b) (λ (X--1 : nat) -> eq lzero nat a (plus X--1 r)) eqa (times b q) (commutative-times q b)) (plus r (times b q)) (commutative-plus (times b q) r))) (plus (times b q) r) (commutative-plus (times b q) r)) (times q b) (commutative-times q b))) spec1) spec

div-plus-times : (m : nat) -> (q : nat) -> (r : nat) -> (X-- : lt r m) -> eq lzero nat (div (plus (times q m) r) m) q
div-plus-times = λ (m : nat) -> λ (q : nat) -> λ (r : nat) -> λ (ltrm : lt r m) -> div-mod-spec-to-eq (plus (times q m) r) m (div (plus (times q m) r) m) (mod (plus (times q m) r) m) q r (div-mod-spec-div-mod (plus (times q m) r) m (ltn-to-ltO r m ltrm)) (div-mod-spec-intro (plus (times q m) r) m q r ltrm (rewrite-r lzero lzero nat (times m q) (λ (X-- : nat) -> eq lzero nat (plus X-- r) (plus (times q m) r)) (rewrite-r lzero lzero nat (plus r (times m q)) (λ (X-- : nat) -> eq lzero nat X-- (plus (times q m) r)) (rewrite-r lzero lzero nat (times m q) (λ (X-- : nat) -> eq lzero nat (plus r (times m q)) (plus X-- r)) (rewrite-r lzero lzero nat (plus (times m q) r) (λ (X-- : nat) -> eq lzero nat X-- (plus (times m q) r)) (refl lzero nat (plus (times m q) r)) (plus r (times m q)) (commutative-plus r (times m q))) (times q m) (commutative-times q m)) (plus (times m q) r) (commutative-plus (times m q) r)) (times q m) (commutative-times q m)))

mod-plus-times : (m : nat) -> (q : nat) -> (r : nat) -> (X-- : lt r m) -> eq lzero nat (mod (plus (times q m) r) m) r
mod-plus-times = λ (m : nat) -> λ (q : nat) -> λ (r : nat) -> λ (ltrm : lt r m) -> div-mod-spec-to-eq2 (plus (times q m) r) m (div (plus (times q m) r) m) (mod (plus (times q m) r) m) q r (div-mod-spec-div-mod (plus (times q m) r) m (ltn-to-ltO r m ltrm)) (div-mod-spec-intro (plus (times q m) r) m q r ltrm (rewrite-r lzero lzero nat (times m q) (λ (X-- : nat) -> eq lzero nat (plus X-- r) (plus (times q m) r)) (rewrite-r lzero lzero nat (plus r (times m q)) (λ (X-- : nat) -> eq lzero nat X-- (plus (times q m) r)) (rewrite-r lzero lzero nat (plus r (times q m)) (λ (X-- : nat) -> eq lzero nat (plus r (times m q)) X--) (rewrite-r lzero lzero nat (times q m) (λ (X-- : nat) -> eq lzero nat (plus r X--) (plus r (times q m))) (refl lzero nat (plus r (times q m))) (times m q) (commutative-times m q)) (plus (times q m) r) (commutative-plus (times q m) r)) (plus (times m q) r) (commutative-plus (times m q) r)) (times q m) (commutative-times q m)))

div-times : (a : nat) -> (b : nat) -> (X-- : lt O b) -> eq lzero nat (div (times a b) b) a
div-times = λ (a : nat) -> λ (b : nat) -> λ (posb : lt O b) -> div-mod-spec-to-eq (times a b) b (div (times a b) b) (mod (times a b) b) a O (div-mod-spec-div-mod (times a b) b posb) (div-mod-spec-intro (times a b) b a O posb (rewrite-r lzero lzero nat (plus O (times a b)) (λ (X-- : nat) -> eq lzero nat (times a b) X--) (rewrite-l lzero lzero nat (times a b) (λ (X-- : nat) -> eq lzero nat (times a b) X--) (refl lzero nat (times a b)) (plus O (times a b)) (plus-O-n (times a b))) (plus (times a b) O) (commutative-plus (times a b) O)))

div-n-n : (n : nat) -> (X-- : lt O n) -> eq lzero nat (div n n) (S O)
div-n-n = λ (n : nat) -> λ (auto : lt O n) -> eq-coerc lzero (eq lzero nat (div (plus (times (S O) n) O) n) (S O)) (eq lzero nat (div n n) (S O)) (div-plus-times n (S O) O auto) (rewrite-l lzero (lsuc lzero) nat (times (S O) n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (div X-- n) (S O)) (eq lzero nat (div n n) (S O))) (rewrite-r lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (div X-- n) (S O)) (eq lzero nat (div n n) (S O))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (div n n) (S O))) (times (S O) n) (rewrite-r lzero lzero nat (times n (S O)) (λ (X-- : nat) -> eq lzero nat (times (S O) n) X--) (commutative-times (S O) n) n (times-n-1 n))) (plus (times (S O) n) O) (plus-n-O (times (S O) n)))

eq-div-O : (n : nat) -> (m : nat) -> (X-- : lt n m) -> eq lzero nat (div n m) O
eq-div-O = λ (n : nat) -> λ (m : nat) -> λ (ltnm : lt n m) -> div-mod-spec-to-eq n m (div n m) (mod n m) O n (div-mod-spec-div-mod n m (ltn-to-ltO n m ltnm)) (div-mod-spec-intro n m O n ltnm (rewrite-r lzero lzero nat (times m O) (λ (X-- : nat) -> eq lzero nat n (plus X-- n)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat n (plus X-- n)) (rewrite-r lzero lzero nat (plus n O) (λ (X-- : nat) -> eq lzero nat 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)) (plus O n) (commutative-plus O n)) (times m O) (times-n-O m)) (times O m) (commutative-times O m)))

mod-n-n : (n : nat) -> (X-- : lt O n) -> eq lzero nat (mod n n) O
mod-n-n = λ (n : nat) -> λ (posn : lt O n) -> div-mod-spec-to-eq2 n n (div n n) (mod n n) (S O) O (div-mod-spec-div-mod n n posn) (div-mod-spec-intro n n (S O) O posn (rewrite-r lzero lzero nat (times n (S O)) (λ (X-- : nat) -> eq lzero nat n (plus X-- O)) (rewrite-l lzero lzero nat (plus n (times n O)) (λ (X-- : nat) -> eq lzero nat n (plus X-- O)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat n (plus (plus n X--) O)) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n (plus X-- O)) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (plus n O) (plus-n-O n)) (plus n O) (plus-n-O n)) (times n O) (times-n-O n)) (times n (S O)) (times-n-Sm n O)) (times (S O) n) (commutative-times (S O) n)))

mod-S : (n : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : lt (S (mod n m)) m) -> eq lzero nat (mod (S n) m) (S (mod n m))
mod-S = λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> λ (H : lt (S (mod n m)) m) -> div-mod-spec-to-eq2 (S n) m (div (S n) m) (mod (S n) m) (div n m) (S (mod n m)) (div-mod-spec-div-mod (S n) m posm) (div-mod-spec-intro (S n) m (div n m) (S (mod n m)) H (eq-coerc lzero (eq lzero nat (S n) (S (plus (times m (div n m)) (mod n m)))) (eq lzero nat (S n) (plus (times (div n m) m) (S (mod n m)))) (eq-f lzero lzero nat nat S n (plus (times m (div n m)) (mod n m)) (rewrite-r lzero lzero nat (plus (mod n m) (times m (div n m))) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (plus (mod n m) (times m (div n m))) (rewrite-l lzero lzero nat (plus (times m (div n m)) (mod n m)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n m) m) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n m))) (div-mod n m) (times m (div n m)) (commutative-times (div n m) m)) (plus (mod n m) (times m (div n m))) (commutative-plus (times m (div n m)) (mod n m)))) (plus (times m (div n m)) (mod n m)) (commutative-plus (times m (div n m)) (mod n m)))) (rewrite-r lzero (lsuc lzero) nat (times m (div n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (S n) (S (plus (times m (div n m)) (mod n m)))) (eq lzero nat (S n) (plus X-- (S (mod n m))))) (rewrite-r lzero (lsuc lzero) nat (plus (times m (div n m)) (S (mod n m))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (S n) X--) (eq lzero nat (S n) (plus (times m (div n m)) (S (mod n m))))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (S n) (plus (times m (div n m)) (S (mod n m))))) (S (plus (times m (div n m)) (mod n m))) (plus-n-Sm (times m (div n m)) (mod n m))) (times (div n m) m) (commutative-times (div n m) m))))

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

lt-to-eq-mod : (n : nat) -> (m : nat) -> (X-- : lt n m) -> eq lzero nat (mod n m) n
lt-to-eq-mod = λ (n : nat) -> λ (m : nat) -> λ (ltnm : lt n m) -> div-mod-spec-to-eq2 n m (div n m) (mod n m) O n (div-mod-spec-div-mod n m (ltn-to-ltO n m ltnm)) (div-mod-spec-intro n m O n ltnm (rewrite-r lzero lzero nat (times m O) (λ (X-- : nat) -> eq lzero nat n (plus X-- n)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat n (plus X-- n)) (rewrite-r lzero lzero nat (plus n O) (λ (X-- : nat) -> eq lzero nat 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)) (plus O n) (commutative-plus O n)) (times m O) (times-n-O m)) (times O m) (commutative-times O m)))

or-div-mod : (n : nat) -> (q : nat) -> (X-- : lt O q) -> Or lzero lzero (And lzero lzero (eq lzero nat (S (mod n q)) q) (eq lzero nat (S n) (times (S (div n q)) q))) (And lzero lzero (lt (S (mod n q)) q) (eq lzero nat (S n) (plus (times (div n q) q) (S (mod n q)))))
or-div-mod = λ (n : nat) -> λ (q : nat) -> λ (posq : lt O q) -> Or-ind lzero lzero lzero (lt (S (mod n q)) q) (eq lzero nat (S (mod n q)) q) (λ (X-x-170 : Or lzero lzero (lt (S (mod n q)) q) (eq lzero nat (S (mod n q)) q)) -> Or lzero lzero (And lzero lzero (eq lzero nat (S (mod n q)) q) (eq lzero nat (S n) (times (S (div n q)) q))) (And lzero lzero (lt (S (mod n q)) q) (eq lzero nat (S n) (plus (times (div n q) q) (S (mod n q)))))) (λ (H : lt (S (mod n q)) q) -> or-intror lzero lzero (And lzero lzero (eq lzero nat (S (mod n q)) q) (eq lzero nat (S n) (times (S (div n q)) q))) (And lzero lzero (lt (S (mod n q)) q) (eq lzero nat (S n) (plus (times (div n q) q) (S (mod n q))))) (conj lzero lzero (lt (S (mod n q)) q) (eq lzero nat (S n) (plus (times (div n q) q) (S (mod n q)))) H (eq-coerc lzero (eq lzero nat (S n) (S (plus (times q (div n q)) (mod n q)))) (eq lzero nat (S n) (plus (times (div n q) q) (S (mod n q)))) (eq-f lzero lzero nat nat S n (plus (times q (div n q)) (mod n q)) (rewrite-r lzero lzero nat (plus (mod n q) (times q (div n q))) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (plus (mod n q) (times q (div n q))) (rewrite-l lzero lzero nat (plus (times q (div n q)) (mod n q)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n q) q) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n q))) (div-mod n q) (times q (div n q)) (commutative-times (div n q) q)) (plus (mod n q) (times q (div n q))) (commutative-plus (times q (div n q)) (mod n q)))) (plus (times q (div n q)) (mod n q)) (commutative-plus (times q (div n q)) (mod n q)))) (rewrite-r lzero (lsuc lzero) nat (times q (div n q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (S n) (S (plus (times q (div n q)) (mod n q)))) (eq lzero nat (S n) (plus X-- (S (mod n q))))) (rewrite-r lzero (lsuc lzero) nat (plus (times q (div n q)) (S (mod n q))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (S n) X--) (eq lzero nat (S n) (plus (times q (div n q)) (S (mod n q))))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (S n) (plus (times q (div n q)) (S (mod n q))))) (S (plus (times q (div n q)) (mod n q))) (plus-n-Sm (times q (div n q)) (mod n q))) (times (div n q) q) (commutative-times (div n q) q))))) (λ (H : eq lzero nat (S (mod n q)) q) -> or-introl lzero lzero (And lzero lzero (eq lzero nat (S (mod n q)) q) (eq lzero nat (S n) (times (S (div n q)) q))) (And lzero lzero (lt (S (mod n q)) q) (eq lzero nat (S n) (plus (times (div n q) q) (S (mod n q))))) (conj lzero lzero (eq lzero nat (S (mod n q)) q) (eq lzero nat (S n) (times (S (div n q)) q)) (rewrite-r lzero lzero nat q (λ (X-- : nat) -> eq lzero nat X-- q) (refl lzero nat q) (S (mod n q)) H) (rewrite-r lzero lzero nat (times q (S (div n q))) (λ (X-- : nat) -> eq lzero nat (S n) X--) (rewrite-l lzero lzero nat (plus q (times q (div n q))) (λ (X-- : nat) -> eq lzero nat (S n) X--) (eq-ind lzero lzero nat (S (mod n q)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (mod n q)) x-1) -> eq lzero nat (S n) (plus x-1 (times q (div n q)))) (eq-f lzero lzero nat nat S n (plus (mod n q) (times q (div n q))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat n X--) (refl lzero nat n) (plus (mod n q) (times q (div n q))) (rewrite-l lzero lzero nat (plus (times q (div n q)) (mod n q)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n q) q) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n q))) (div-mod n q) (times q (div n q)) (commutative-times (div n q) q)) (plus (mod n q) (times q (div n q))) (commutative-plus (times q (div n q)) (mod n q))))) q H) (times q (S (div n q))) (times-n-Sm q (div n q))) (times (S (div n q)) q) (commutative-times (S (div n q)) q)))) (le-to-or-lt-eq (S (mod n q)) q (lt-mod-m-m n q posq))

injective-times-r : (n : nat) -> (X-- : lt O n) -> ||injective|| lzero lzero nat nat (λ (m : nat) -> times n m)
injective-times-r = λ (n : nat) -> λ (posn : lt O n) -> λ (a : nat) -> λ (b : nat) -> λ (eqn : eq lzero nat (times n a) (times n b)) -> eq-ind lzero lzero nat (div (times a n) n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (div (times a n) n) x-1) -> eq lzero nat x-1 b) (eq-ind lzero lzero nat (div (times b n) n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (div (times b n) n) x-1) -> eq lzero nat (div (times a n) n) x-1) (rewrite-r lzero lzero nat (times n a) (λ (X-- : nat) -> eq lzero nat (div X-- n) (div (times b n) n)) (rewrite-r lzero lzero nat (times n b) (λ (X-- : nat) -> eq lzero nat (div (times n a) n) (div X-- n)) (rewrite-l lzero lzero nat (times n a) (λ (X-- : nat) -> eq lzero nat (div (times n a) n) (div X-- n)) (refl lzero nat (div (times n a) n)) (times n b) eqn) (times b n) (commutative-times b n)) (times a n) (commutative-times a n)) b (div-times b n posn)) a (div-times a n posn)

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

lt-div-S : (n : nat) -> (m : nat) -> (X-- : lt O m) -> lt n (times (S (div n m)) m)
lt-div-S = λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> eq-ind-r lzero lzero nat (plus (times (div n m) m) (mod n m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div n m) m) (mod n m))) -> lt x (plus m (times (div n m) m))) (eq-ind-r lzero lzero nat (plus (mod n m) (times (div n m) m)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (mod n m) (times (div n m) m))) -> lt x (plus m (times (div n m) m))) (monotonic-lt-plus-l (times (div n m) m) (mod n m) m (lt-mod-m-m n m posm)) (plus (times (div n m) m) (mod n m)) (commutative-plus (times (div n m) m) (mod n m))) n (div-mod n m)

le-div : (n : nat) -> (m : nat) -> (X-- : lt O n) -> le (div m n) m
le-div = λ (n : nat) -> λ (m : nat) -> λ (posn : lt O n) -> eq-ind-r lzero lzero nat (plus (times (div m n) n) (mod m n)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div m n) n) (mod m n))) -> le (div m n) x) (transitive-le (div m n) (times (div m n) n) (plus (times (div m n) n) (mod m n)) (eq-coerc lzero (le (times (div m n) (S O)) (times (div m n) n)) (le (div m n) (times (div m n) n)) (monotonic-le-times-r (div m n) (S O) n posn) (rewrite-r lzero (lsuc lzero) nat (times n (div m n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times (div m n) (S O)) (times (div m n) n)) (le (div m n) X--)) (rewrite-l lzero (lsuc lzero) nat (div m n) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (times (div m n) n)) (le (div m n) (times n (div m n)))) (rewrite-r lzero (lsuc lzero) nat (times n (div m n)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (div m n) X--) (le (div m n) (times n (div m n)))) (refl (lsuc lzero) (Set (lzero)) (le (div m n) (times n (div m n)))) (times (div m n) n) (commutative-times (div m n) n)) (times (div m n) (S O)) (times-n-1 (div m n))) (times (div m n) n) (commutative-times (div m n) n))) (le-plus-n-r (mod m n) (times (div m n) n))) m (div-mod m n)

le-plus-mod : (m : nat) -> (n : nat) -> (q : nat) -> (X-- : lt O q) -> le (mod (plus m n) q) (plus (mod m q) (mod n q))
le-plus-mod = λ (m : nat) -> λ (n : nat) -> λ (q : nat) -> λ (posq : lt O q) -> Or-ind lzero lzero lzero (le q (plus (mod m q) (mod n q))) (Not lzero (le q (plus (mod m q) (mod n q)))) (λ (X-x-170 : Or lzero lzero (le q (plus (mod m q) (mod n q))) (Not lzero (le q (plus (mod m q) (mod n q))))) -> le (mod (plus m n) q) (plus (mod m q) (mod n q))) (λ (Hle : le q (plus (mod m q) (mod n q))) -> transitive-le (mod (plus m n) q) q (plus (mod m q) (mod n q)) (le-S-S-to-le (mod (plus m n) q) q (le-S (S (mod (plus m n) q)) q (lt-mod-m-m (plus m n) q posq))) Hle) (λ (Hle : Not lzero (le q (plus (mod m q) (mod n q)))) -> eq-coerc lzero (le (mod (plus m n) q) (plus (mod (plus m n) q) O)) (le (mod (plus m n) q) (plus (mod m q) (mod n q))) (le-plus-n-r O (mod (plus m n) q)) (rewrite-l lzero (lsuc lzero) nat (mod (plus m n) q) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (mod (plus m n) q) (plus (mod (plus m n) q) O)) (le (mod (plus m n) q) X--)) (rewrite-l lzero (lsuc lzero) nat (mod (plus m n) q) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (mod (plus m n) q) X--) (le (mod (plus m n) q) (mod (plus m n) q))) (refl (lsuc lzero) (Set (lzero)) (le (mod (plus m n) q) (mod (plus m n) q))) (plus (mod (plus m n) q) O) (plus-n-O (mod (plus m n) q))) (plus (mod m q) (mod n q)) (div-mod-spec-to-eq2 (plus m n) q (div (plus m n) q) (mod (plus m n) q) (plus (div m q) (div n q)) (plus (mod m q) (mod n q)) (div-mod-spec-div-mod (plus m n) q posq) (div-mod-spec-intro (plus m n) q (plus (div m q) (div n q)) (plus (mod m q) (mod n q)) (not-le-to-lt q (plus (mod m q) (mod n q)) Hle) (eq-ind-r lzero lzero nat (plus (times (div n q) q) (mod n q)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div n q) q) (mod n q))) -> eq lzero nat (plus m x) (plus (times (plus (div m q) (div n q)) q) (plus (mod m q) (mod n q)))) (eq-coerc lzero (eq lzero nat (plus (plus m (times (div n q) q)) (mod n q)) (plus (plus (times (plus (div m q) (div n q)) q) (mod m q)) (mod n q))) (eq lzero nat (plus m (plus (times (div n q) q) (mod n q))) (plus (times (plus (div m q) (div n q)) q) (plus (mod m q) (mod n q)))) (eq-f lzero lzero nat nat (λ (x : nat) -> plus x (mod n q)) (plus m (times (div n q) q)) (plus (times (plus (div m q) (div n q)) q) (mod m q)) (eq-ind-r lzero lzero nat (plus (times (div m q) q) (mod m q)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div m q) q) (mod m q))) -> eq lzero nat (plus x (times (div n q) q)) (plus (times (plus (div m q) (div n q)) q) (mod m q))) (eq-coerc lzero (eq lzero nat (plus (times q (plus (div m q) (div n q))) (mod m q)) (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat (plus (plus (times (div m q) q) (mod m q)) (times (div n q) q)) (plus (times (plus (div m q) (div n q)) q) (mod m q))) (eq-f lzero lzero nat nat (λ (x : nat) -> plus x (mod m q)) (times q (plus (div m q) (div n q))) (times q (plus (div m q) (div n q))) (refl lzero nat (times q (plus (div m q) (div n q))))) (rewrite-r lzero (lsuc lzero) nat (plus (times (div m q) q) (plus (mod m q) (times (div n q) q))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times q (plus (div m q) (div n q))) (mod m q)) (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat X-- (plus (times (plus (div m q) (div n q)) q) (mod m q)))) (rewrite-r lzero (lsuc lzero) nat (times q (div m q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times q (plus (div m q) (div n q))) (mod m q)) (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat (plus X-- (plus (mod m q) (times (div n q) q))) (plus (times (plus (div m q) (div n q)) q) (mod m q)))) (rewrite-r lzero (lsuc lzero) nat (times q (div n q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times q (plus (div m q) (div n q))) (mod m q)) (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat (plus (times q (div m q)) (plus (mod m q) X--)) (plus (times (plus (div m q) (div n q)) q) (mod m q)))) (rewrite-r lzero (lsuc lzero) nat (plus (mod m q) (plus (times q (div m q)) (times q (div n q)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times q (plus (div m q) (div n q))) (mod m q)) (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat X-- (plus (times (plus (div m q) (div n q)) q) (mod m q)))) (rewrite-l lzero (lsuc lzero) nat (times q (plus (div m q) (div n q))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times q (plus (div m q) (div n q))) (mod m q)) (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat (plus (mod m q) X--) (plus (times (plus (div m q) (div n q)) q) (mod m q)))) (rewrite-r lzero (lsuc lzero) nat (times q (plus (div m q) (div n q))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times q (plus (div m q) (div n q))) (mod m q)) (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat (plus (mod m q) (times q (plus (div m q) (div n q)))) (plus X-- (mod m q)))) (rewrite-r lzero (lsuc lzero) nat (plus (mod m q) (times q (plus (div m q) (div n q)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times q (plus (div m q) (div n q))) (mod m q)) (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat (plus (mod m q) (times q (plus (div m q) (div n q)))) X--)) (rewrite-r lzero (lsuc lzero) nat (plus (mod m q) (times q (plus (div m q) (div n q)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat X-- (plus (times q (plus (div m q) (div n q))) (mod m q))) (eq lzero nat (plus (mod m q) (times q (plus (div m q) (div n q)))) (plus (mod m q) (times q (plus (div m q) (div n q)))))) (rewrite-r lzero (lsuc lzero) nat (plus (mod m q) (times q (plus (div m q) (div n q)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (mod m q) (times q (plus (div m q) (div n q)))) X--) (eq lzero nat (plus (mod m q) (times q (plus (div m q) (div n q)))) (plus (mod m q) (times q (plus (div m q) (div n q)))))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (mod m q) (times q (plus (div m q) (div n q)))) (plus (mod m q) (times q (plus (div m q) (div n q)))))) (plus (times q (plus (div m q) (div n q))) (mod m q)) (commutative-plus (times q (plus (div m q) (div n q))) (mod m q))) (plus (times q (plus (div m q) (div n q))) (mod m q)) (commutative-plus (times q (plus (div m q) (div n q))) (mod m q))) (plus (times q (plus (div m q) (div n q))) (mod m q)) (commutative-plus (times q (plus (div m q) (div n q))) (mod m q))) (times (plus (div m q) (div n q)) q) (commutative-times (plus (div m q) (div n q)) q)) (plus (times q (div m q)) (times q (div n q))) (distributive-times-plus q (div m q) (div n q))) (plus (times q (div m q)) (plus (mod m q) (times q (div n q)))) (rewrite-l lzero lzero nat (plus (plus (mod m q) (times q (div m q))) (times q (div n q))) (λ (X-- : nat) -> eq lzero nat (plus (times q (div m q)) (plus (mod m q) (times q (div n q)))) X--) (assoc-plus1 (times q (div n q)) (mod m q) (times q (div m q))) (plus (mod m q) (plus (times q (div m q)) (times q (div n q)))) (associative-plus (mod m q) (times q (div m q)) (times q (div n q))))) (times (div n q) q) (commutative-times (div n q) q)) (times (div m q) q) (commutative-times (div m q) q)) (plus (plus (times (div m q) q) (mod m q)) (times (div n q) q)) (associative-plus (times (div m q) q) (mod m q) (times (div n q) q)))) m (div-mod m q))) (rewrite-r lzero (lsuc lzero) nat (plus m (plus (times (div n q) q) (mod n q))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat X-- (plus (plus (times (plus (div m q) (div n q)) q) (mod m q)) (mod n q))) (eq lzero nat (plus m (plus (times (div n q) q) (mod n q))) (plus (times (plus (div m q) (div n q)) q) (plus (mod m q) (mod n q))))) (rewrite-r lzero (lsuc lzero) nat (plus (times (plus (div m q) (div n q)) q) (plus (mod m q) (mod n q))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus m (plus (times (div n q) q) (mod n q))) X--) (eq lzero nat (plus m (plus (times (div n q) q) (mod n q))) (plus (times (plus (div m q) (div n q)) q) (plus (mod m q) (mod n q))))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (plus m (plus (times (div n q) q) (mod n q))) (plus (times (plus (div m q) (div n q)) q) (plus (mod m q) (mod n q))))) (plus (plus (times (plus (div m q) (div n q)) q) (mod m q)) (mod n q)) (associative-plus (times (plus (div m q) (div n q)) q) (mod m q) (mod n q))) (plus (plus m (times (div n q) q)) (mod n q)) (associative-plus m (times (div n q) q) (mod n q)))) n (div-mod n q)))))) (decidable-le q (plus (mod m q) (mod n q)))

le-plus-div : (m : nat) -> (n : nat) -> (q : nat) -> (X-- : lt O q) -> le (plus (div m q) (div n q)) (div (plus m n) q)
le-plus-div = λ (m : nat) -> λ (n : nat) -> λ (q : nat) -> λ (posq : lt O q) -> le-times-to-le q (plus (div m q) (div n q)) (div (plus m n) q) posq (le-plus-to-le-r (mod (plus m n) q) (times q (plus (div m q) (div n q))) (times q (div (plus m n) q)) (eq-ind-r lzero lzero nat (times (div (plus m n) q) q) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (div (plus m n) q) q)) -> le (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) (plus x (mod (plus m n) q))) (eq-ind lzero lzero nat (plus m n) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus m n) x-1) -> le (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) x-1) (eq-ind-r lzero lzero nat (plus (times (div m q) q) (mod m q)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div m q) q) (mod m q))) -> le (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) (plus x n)) (eq-ind-r lzero lzero nat (plus (times (div n q) q) (mod n q)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div n q) q) (mod n q))) -> le (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) (plus (plus (times (div m q) q) (mod m q)) x)) (eq-ind-r lzero lzero nat (plus (mod m q) (times (div m q) q)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (mod m q) (times (div m q) q))) -> le (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) (plus x (plus (times (div n q) q) (mod n q)))) (eq-ind-r lzero lzero nat (plus (mod m q) (plus (times (div m q) q) (plus (times (div n q) q) (mod n q)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (mod m q) (plus (times (div m q) q) (plus (times (div n q) q) (mod n q))))) -> le (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) x) (eq-ind lzero lzero nat (plus (plus (times (div m q) q) (times (div n q) q)) (mod n q)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (plus (plus (times (div m q) q) (times (div n q) q)) (mod n q)) x-1) -> le (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) (plus (mod m q) x-1)) (eq-coerc lzero (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (plus (mod m q) (mod n q)) (times q (plus (div m q) (div n q))))) (le (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) (plus (mod m q) (plus (plus (times (div m q) q) (times (div n q) q)) (mod n q)))) (monotonic-le-plus-l (times q (plus (div m q) (div n q))) (mod (plus m n) q) (plus (mod m q) (mod n q)) (le-plus-mod m n q posq)) (rewrite-r lzero (lsuc lzero) nat (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (plus (mod m q) (mod n q)) (times q (plus (div m q) (div n q))))) (le X-- (plus (mod m q) (plus (plus (times (div m q) q) (times (div n q) q)) (mod n q))))) (rewrite-r lzero (lsuc lzero) nat (times q (div m q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (plus (mod m q) (mod n q)) (times q (plus (div m q) (div n q))))) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (mod m q) (plus (plus X-- (times (div n q) q)) (mod n q))))) (rewrite-r lzero (lsuc lzero) nat (times q (div n q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (plus (mod m q) (mod n q)) (times q (plus (div m q) (div n q))))) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (mod m q) (plus (plus (times q (div m q)) X--) (mod n q))))) (rewrite-l lzero (lsuc lzero) nat (times q (plus (div m q) (div n q))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (plus (mod m q) (mod n q)) (times q (plus (div m q) (div n q))))) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (mod m q) (plus X-- (mod n q))))) (rewrite-r lzero (lsuc lzero) nat (plus (mod n q) (times q (plus (div m q) (div n q)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (plus (mod m q) (mod n q)) (times q (plus (div m q) (div n q))))) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (mod m q) X--))) (rewrite-r lzero (lsuc lzero) nat (plus (mod m q) (plus (mod n q) (times q (plus (div m q) (div n q))))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) X--) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (mod m q) (plus (mod n q) (times q (plus (div m q) (div n q))))))) (refl (lsuc lzero) (Set (lzero)) (le (plus (mod (plus m n) q) (times q (plus (div m q) (div n q)))) (plus (mod m q) (plus (mod n q) (times q (plus (div m q) (div n q))))))) (plus (plus (mod m q) (mod n q)) (times q (plus (div m q) (div n q)))) (associative-plus (mod m q) (mod n q) (times q (plus (div m q) (div n q))))) (plus (times q (plus (div m q) (div n q))) (mod n q)) (commutative-plus (times q (plus (div m q) (div n q))) (mod n q))) (plus (times q (div m q)) (times q (div n q))) (distributive-times-plus q (div m q) (div n q))) (times (div n q) q) (commutative-times (div n q) q)) (times (div m q) q) (commutative-times (div m q) q)) (plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)) (commutative-plus (times q (plus (div m q) (div n q))) (mod (plus m n) q)))) (plus (times (div m q) q) (plus (times (div n q) q) (mod n q))) (associative-plus (times (div m q) q) (times (div n q) q) (mod n q))) (plus (plus (mod m q) (times (div m q) q)) (plus (times (div n q) q) (mod n q))) (associative-plus (mod m q) (times (div m q) q) (plus (times (div n q) q) (mod n q)))) (plus (times (div m q) q) (mod m q)) (commutative-plus (times (div m q) q) (mod m q))) n (div-mod n q)) m (div-mod m q)) (plus (times (div (plus m n) q) q) (mod (plus m n) q)) (div-mod (plus m n) q)) (times q (div (plus m n) q)) (commutative-times q (div (plus m n) q))))

le-times-to-le-div : (a : nat) -> (b : nat) -> (c : nat) -> (X-- : lt O b) -> (X--1 : le (times b c) a) -> le c (div a b)
le-times-to-le-div = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (posb : lt O b) -> λ (Hle : le (times b c) a) -> le-S-S-to-le c (div a b) (lt-times-n-to-lt-l b c (S (div a b)) (le-to-lt-to-lt (times c b) a (times (S (div a b)) b) (eq-coerc lzero (le (times b c) a) (le (times c b) a) Hle (rewrite-r lzero (lsuc lzero) nat (times b c) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times b c) a) (le X-- a)) (refl (lsuc lzero) (Set (lzero)) (le (times b c) a)) (times c b) (commutative-times c b))) (lt-div-S a b posb)))

le-times-to-le-div2 : (m : nat) -> (n : nat) -> (q : nat) -> (X-- : lt O q) -> (X--1 : le n (times m q)) -> le (div n q) m
le-times-to-le-div2 = λ (m : nat) -> λ (n : nat) -> λ (q : nat) -> λ (posq : lt O q) -> λ (Hle : le n (times m q)) -> le-times-to-le q (div n q) m posq (le-plus-to-le (mod n q) (times q (div n q)) (times q m) (le-plus-a (mod n q) (plus (mod n q) (times q (div n q))) (times q m) (eq-coerc lzero (le n (times m q)) (le (plus (mod n q) (times q (div n q))) (times q m)) Hle (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n (times m q)) (le X-- (times q m))) (rewrite-r lzero (lsuc lzero) nat (times m q) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le n (times m q)) (le n X--)) (refl (lsuc lzero) (Set (lzero)) (le n (times m q))) (times q m) (commutative-times q m)) (plus (mod n q) (times q (div n q))) (rewrite-l lzero lzero nat (plus (times q (div n q)) (mod n q)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n q) q) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n q))) (div-mod n q) (times q (div n q)) (commutative-times (div n q) q)) (plus (mod n q) (times q (div n q))) (commutative-plus (times q (div n q)) (mod n q)))))))

lt-times-to-lt-div : (m : nat) -> (n : nat) -> (q : nat) -> (X-- : lt n (times m q)) -> lt (div n q) m
lt-times-to-lt-div = λ (m : nat) -> λ (n : nat) -> λ (q : nat) -> λ (Hlt : lt n (times m q)) -> lt-times-n-to-lt-l q (div n q) m (lt-plus-to-lt-l (mod n q) (times (div n q) q) (times m q) (lt-to-le-to-lt (plus (times (div n q) q) (mod n q)) (times m q) (plus (times m q) (mod n q)) (eq-coerc lzero (lt n (times m q)) (lt (plus (times (div n q) q) (mod n q)) (times m q)) Hlt (rewrite-r lzero (lsuc lzero) nat (times q (div n q)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt n (times m q)) (lt (plus X-- (mod n q)) (times m q))) (rewrite-r lzero (lsuc lzero) nat (plus (mod n q) (times q (div n q))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt n (times m q)) (lt X-- (times m q))) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt n (times m q)) (lt X-- (times m q))) (refl (lsuc lzero) (Set (lzero)) (lt n (times m q))) (plus (mod n q) (times q (div n q))) (rewrite-l lzero lzero nat (plus (times q (div n q)) (mod n q)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n q) q) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n q))) (div-mod n q) (times q (div n q)) (commutative-times (div n q) q)) (plus (mod n q) (times q (div n q))) (commutative-plus (times q (div n q)) (mod n q)))) (plus (times q (div n q)) (mod n q)) (commutative-plus (times q (div n q)) (mod n q))) (times (div n q) q) (commutative-times (div n q) q))) (le-plus-n-r (mod n q) (times m q))))

le-div-S-S-div : (n : nat) -> (m : nat) -> (X-- : lt O m) -> le (div (S n) m) (S (div n m))
le-div-S-S-div = λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> le-times-to-le-div2 (S (div n m)) (S n) m posm (lt-div-S n m posm)

le-times-div-div-times : (a : nat) -> (n : nat) -> (m : nat) -> (X-- : lt O m) -> le (times a (div n m)) (div (times a n) m)
le-times-div-div-times = λ (a : nat) -> λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> le-times-to-le-div (times a n) m (times a (div n m)) posm (eq-coerc lzero (le (times m (times a (div n m))) (plus (times a (mod n m)) (times m (times a (div n m))))) (le (times m (times a (div n m))) (times a n)) (le-plus-n (times a (mod n m)) (times m (times a (div n m)))) (rewrite-r lzero (lsuc lzero) nat (times a (times m (div n m))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- (plus (times a (mod n m)) X--)) (le X-- (times a n))) (rewrite-l lzero (lsuc lzero) nat (times a (plus (mod n m) (times m (div n m)))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times a (times m (div n m))) X--) (le (times a (times m (div n m))) (times a n))) (rewrite-l lzero (lsuc lzero) nat n (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le (times a (times m (div n m))) (times a X--)) (le (times a (times m (div n m))) (times a n))) (refl (lsuc lzero) (Set (lzero)) (le (times a (times m (div n m))) (times a n))) (plus (mod n m) (times m (div n m))) (rewrite-l lzero lzero nat (plus (times m (div n m)) (mod n m)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n m) m) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n m))) (div-mod n m) (times m (div n m)) (commutative-times (div n m) m)) (plus (mod n m) (times m (div n m))) (commutative-plus (times m (div n m)) (mod n m)))) (plus (times a (mod n m)) (times a (times m (div n m)))) (distributive-times-plus a (mod n m) (times m (div n m)))) (times m (times a (div n m))) (times-times m a (div n m))))

monotonic-div : (n : nat) -> (X-- : lt O n) -> monotonic lzero lzero nat le (λ (m : nat) -> div m n)
monotonic-div = λ (n : nat) -> λ (posn : lt O n) -> λ (a : nat) -> λ (b : nat) -> λ (leab : le a b) -> le-times-to-le-div b n (div a n) posn (le-plus-b (mod a n) (times n (div a n)) b (eq-coerc lzero (le a b) (le (plus (times n (div a n)) (mod a n)) b) leab (rewrite-r lzero (lsuc lzero) nat (plus (mod a n) (times n (div a n))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le a b) (le X-- b)) (rewrite-r lzero (lsuc lzero) nat (plus (mod a n) (times n (div a n))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- b) (le (plus (mod a n) (times n (div a n))) b)) (refl (lsuc lzero) (Set (lzero)) (le (plus (mod a n) (times n (div a n))) b)) a (rewrite-l lzero lzero nat (plus (times n (div a n)) (mod a n)) (λ (X-- : nat) -> eq lzero nat a X--) (rewrite-l lzero lzero nat (times (div a n) n) (λ (X-- : nat) -> eq lzero nat a (plus X-- (mod a n))) (div-mod a n) (times n (div a n)) (commutative-times (div a n) n)) (plus (mod a n) (times n (div a n))) (commutative-plus (times n (div a n)) (mod a n)))) (plus (times n (div a n)) (mod a n)) (commutative-plus (times n (div a n)) (mod a n)))))

pos-div : (n : nat) -> (m : nat) -> (X-- : lt O m) -> (X--1 : lt O n) -> (X--2 : eq lzero nat (mod n m) O) -> lt O (div n m)
pos-div = λ (n : nat) -> λ (m : nat) -> λ (posm : lt O m) -> λ (posn : lt O n) -> λ (mod0 : eq lzero nat (mod n m) O) -> lt-times-n-to-lt-l m O (div n m) (eq-coerc lzero (lt O n) (lt (times O m) (times (div n m) m)) posn (rewrite-r lzero (lsuc lzero) nat (times m O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O n) (lt X-- (times (div n m) m))) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O n) (lt X-- (times (div n m) m))) (rewrite-r lzero (lsuc lzero) nat (times m (div n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O n) (lt O X--)) (rewrite-l lzero (lsuc lzero) nat (times m (div n m)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt O X--) (lt O (times m (div n m)))) (refl (lsuc lzero) (Set (lzero)) (lt O (times m (div n m)))) n (rewrite-r lzero lzero nat (minus n O) (λ (X-- : nat) -> eq lzero nat (times m (div n m)) X--) (rewrite-l lzero lzero nat (mod n m) (λ (X-- : nat) -> eq lzero nat (times m (div n m)) (minus n X--)) (rewrite-l lzero lzero nat (times (div n m) m) (λ (X-- : nat) -> eq lzero nat X-- (minus n (mod n m))) (eq-times-div-minus-mod n m) (times m (div n m)) (commutative-times (div n m) m)) O mod0) n (minus-n-O n))) (times (div n m) m) (commutative-times (div n m) m)) (times m O) (times-n-O m)) (times O m) (commutative-times O m)))

let-clause-1034 : (n : nat) -> (m : nat) -> (q : nat) -> (posn : lt O n) -> (posm : lt O m) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (mod x2515 x2516) (times x2516 (div x2515 x2516)))
let-clause-1034 = λ (n : nat) -> λ (m : nat) -> λ (q : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> λ (x2515 : nat) -> λ (x2516 : nat) -> rewrite-l lzero lzero nat (plus (times x2516 (div x2515 x2516)) (mod x2515 x2516)) (λ (X-- : nat) -> eq lzero nat x2515 X--) (rewrite-l lzero lzero nat (times (div x2515 x2516) x2516) (λ (X-- : nat) -> eq lzero nat x2515 (plus X-- (mod x2515 x2516))) (div-mod x2515 x2516) (times x2516 (div x2515 x2516)) (commutative-times (div x2515 x2516) x2516)) (plus (mod x2515 x2516) (times x2516 (div x2515 x2516))) (commutative-plus (times x2516 (div x2515 x2516)) (mod x2515 x2516))

eq-div-div-div-times : (n : nat) -> (m : nat) -> (q : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> eq lzero nat (div (div q n) m) (div q (times n m))
eq-div-div-div-times = λ (n : nat) -> λ (m : nat) -> λ (q : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> div-mod-spec-to-eq q (times n m) (div (div q n) m) (plus (mod q n) (times n (mod (div q n) m))) (div q (times n m)) (mod q (times n m)) (div-mod-spec-intro q (times n m) (div (div q n) m) (plus (mod q n) (times n (mod (div q n) m))) (lt-to-le-to-lt (plus (mod q n) (times n (mod (div q n) m))) (times n (S (mod (div q n) m))) (times n m) (eq-coerc lzero (lt (plus (mod q n) (times n (mod (div q n) m))) (plus n (times n (mod (div q n) m)))) (lt (plus (mod q n) (times n (mod (div q n) m))) (times n (S (mod (div q n) m)))) (monotonic-lt-plus-l (times n (mod (div q n) m)) (mod q n) n (lt-mod-m-m q n posn)) (rewrite-l lzero (lsuc lzero) nat (plus n (times n (mod (div q n) m))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (plus (mod q n) (times n (mod (div q n) m))) (plus n (times n (mod (div q n) m)))) (lt (plus (mod q n) (times n (mod (div q n) m))) X--)) (refl (lsuc lzero) (Set (lzero)) (lt (plus (mod q n) (times n (mod (div q n) m))) (plus n (times n (mod (div q n) m))))) (times n (S (mod (div q n) m))) (times-n-Sm n (mod (div q n) m)))) (monotonic-le-times-r n (S (mod (div q n) m)) m (lt-mod-m-m (div q n) m posm))) (rewrite-r lzero lzero nat (times n (times (div (div q n) m) m)) (λ (X-- : nat) -> eq lzero nat q (plus X-- (plus (mod q n) (times n (mod (div q n) m))))) (rewrite-r lzero lzero nat (times m (div (div q n) m)) (λ (X-- : nat) -> eq lzero nat q (plus (times n X--) (plus (mod q n) (times n (mod (div q n) m))))) (rewrite-r lzero lzero nat (plus (mod q n) (plus (times n (times m (div (div q n) m))) (times n (mod (div q n) m)))) (λ (X-- : nat) -> eq lzero nat q X--) (rewrite-r lzero lzero nat (plus (times n (mod (div q n) m)) (times n (times m (div (div q n) m)))) (λ (X-- : nat) -> eq lzero nat q (plus (mod q n) X--)) (rewrite-l lzero lzero nat (times n (plus (mod (div q n) m) (times m (div (div q n) m)))) (λ (X-- : nat) -> eq lzero nat q (plus (mod q n) X--)) (rewrite-l lzero lzero nat (div q n) (λ (X-- : nat) -> eq lzero nat q (plus (mod q n) (times n X--))) (rewrite-l lzero lzero nat q (λ (X-- : nat) -> eq lzero nat q X--) (refl lzero nat q) (plus (mod q n) (times n (div q n))) (let-clause-1034 n m q posn posm q n)) (plus (mod (div q n) m) (times m (div (div q n) m))) (let-clause-1034 n m q posn posm (div q n) m)) (plus (times n (mod (div q n) m)) (times n (times m (div (div q n) m)))) (distributive-times-plus n (mod (div q n) m) (times m (div (div q n) m)))) (plus (times n (times m (div (div q n) m))) (times n (mod (div q n) m))) (commutative-plus (times n (times m (div (div q n) m))) (times n (mod (div q n) m)))) (plus (times n (times m (div (div q n) m))) (plus (mod q n) (times n (mod (div q n) m)))) (rewrite-l lzero lzero nat (plus (plus (mod q n) (times n (times m (div (div q n) m)))) (times n (mod (div q n) m))) (λ (X-- : nat) -> eq lzero nat (plus (times n (times m (div (div q n) m))) (plus (mod q n) (times n (mod (div q n) m)))) X--) (assoc-plus1 (times n (mod (div q n) m)) (mod q n) (times n (times m (div (div q n) m)))) (plus (mod q n) (plus (times n (times m (div (div q n) m))) (times n (mod (div q n) m)))) (associative-plus (mod q n) (times n (times m (div (div q n) m))) (times n (mod (div q n) m))))) (times (div (div q n) m) m) (commutative-times (div (div q n) m) m)) (times (div (div q n) m) (times n m)) (times-times (div (div q n) m) n m))) (div-mod-spec-div-mod q (times n m) (eq-coerc lzero (lt (times O O) (times n m)) (lt O (times n m)) (lt-times O n O m posn posm) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (times n m)) (lt O (times n m))) (refl (lsuc lzero) (Set (lzero)) (lt O (times n m))) (times O O) (times-O-n O))))

eq-div-div-div-div : (n : nat) -> (m : nat) -> (q : nat) -> (X-- : lt O n) -> (X--1 : lt O m) -> eq lzero nat (div (div q n) m) (div (div q m) n)
eq-div-div-div-div = λ (n : nat) -> λ (m : nat) -> λ (q : nat) -> λ (posn : lt O n) -> λ (posm : lt O m) -> trans-eq lzero nat (div (div q n) m) (div q (times n m)) (div (div q m) n) (eq-div-div-div-times n m q posn posm) (sym-eq lzero nat (div (div q m) n) (div q (times n m)) (eq-coerc lzero (eq lzero nat (div (div q m) n) (div q (times m n))) (eq lzero nat (div (div q m) n) (div q (times n m))) (eq-div-div-div-times m n q posm posn) (rewrite-r lzero (lsuc lzero) nat (times n m) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (div (div q m) n) (div q X--)) (eq lzero nat (div (div q m) n) (div q (times n m)))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (div (div q m) n) (div q (times n m)))) (times m n) (commutative-times m n))))

lt-to-le-times-to-lt-S-to-div : (a : nat) -> (c : nat) -> (b : nat) -> (X-- : lt O b) -> (X--1 : le (times b c) a) -> (X--2 : lt a (times b (S c))) -> eq lzero nat (div a b) c
lt-to-le-times-to-lt-S-to-div = λ (a : nat) -> λ (c : nat) -> λ (b : nat) -> λ (posb : lt O b) -> λ (lea : le (times b c) a) -> λ (lta : lt a (times b (S c))) -> div-mod-spec-to-eq a b (div a b) (mod a b) c (minus a (times b c)) (div-mod-spec-div-mod a b posb) (div-mod-spec-intro a b c (minus a (times b c)) (lt-plus-to-minus a (times b c) b lea (eq-coerc lzero (lt a (times b (S c))) (lt a (plus b (times b c))) lta (rewrite-l lzero (lsuc lzero) nat (plus b (times b c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt a X--) (lt a (plus b (times b c)))) (rewrite-r lzero (lsuc lzero) nat (times c b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt a (plus b X--)) (lt a (plus b (times b c)))) (rewrite-r lzero (lsuc lzero) nat (times c b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt a (plus b (times c b))) (lt a (plus b X--))) (refl (lsuc lzero) (Set (lzero)) (lt a (plus b (times c b)))) (times b c) (commutative-times b c)) (times b c) (commutative-times b c)) (times b (S c)) (times-n-Sm b c)))) (sym-eq lzero nat (plus (times c b) (minus a (times b c))) a (eq-coerc lzero (eq lzero nat (plus (minus a (times c b)) (times c b)) (minus (plus a (times c b)) (times c b))) (eq lzero nat (plus (times c b) (minus a (times b c))) a) (plus-minus (times c b) a (times c b) (eq-coerc lzero (le (times b c) a) (le (times c b) a) lea (rewrite-r lzero (lsuc lzero) nat (times c b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (le X-- a) (le (times c b) a)) (refl (lsuc lzero) (Set (lzero)) (le (times c b) a)) (times b c) (commutative-times b c)))) (rewrite-r lzero (lsuc lzero) nat (times c b) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (minus a (times c b)) (times c b)) (minus (plus a (times c b)) (times c b))) (eq lzero nat (plus (times c b) (minus a X--)) a)) (rewrite-r lzero (lsuc lzero) nat (plus (times c b) (minus a (times c b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat X-- (minus (plus a (times c b)) (times c b))) (eq lzero nat (plus (times c b) (minus a (times c b))) a)) (rewrite-l lzero (lsuc lzero) nat a (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times c b) (minus a (times c b))) X--) (eq lzero nat (plus (times c b) (minus a (times c b))) a)) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (plus (times c b) (minus a (times c b))) a)) (minus (plus a (times c b)) (times c b)) (minus-plus-m-m a (times c b))) (plus (minus a (times c b)) (times c b)) (commutative-plus (minus a (times c b)) (times c b))) (times b c) (commutative-times b c)))))

div-times-times : (a : nat) -> (b : nat) -> (c : nat) -> (X-- : lt O c) -> (X--1 : lt O b) -> eq lzero nat (div a b) (div (times a c) (times b c))
div-times-times = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (posc : lt O c) -> λ (posb : lt O b) -> eq-ind-r lzero lzero nat (times c b) (λ (x : nat) -> λ (X-- : eq lzero nat x (times c b)) -> eq lzero nat (div a b) (div (times a c) x)) (eq-ind lzero lzero nat (div (div (times a c) c) b) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (div (div (times a c) c) b) x-1) -> eq lzero nat (div a b) x-1) (eq-ind-r lzero lzero nat a (λ (x : nat) -> λ (X-- : eq lzero nat x a) -> eq lzero nat (div a b) (div x b)) (refl lzero nat (div a b)) (div (times a c) c) (div-times a c posc)) (div (times a c) (times c b)) (eq-div-div-div-times c b (times a c) posc posb)) (times b c) (commutative-times b c)

times-mod : (a : nat) -> (b : nat) -> (c : nat) -> (X-- : lt O c) -> (X--1 : lt O b) -> eq lzero nat (mod (times a c) (times b c)) (times c (mod a b))
times-mod = λ (a : nat) -> λ (b : nat) -> λ (c : nat) -> λ (posc : lt O c) -> λ (posb : lt O b) -> div-mod-spec-to-eq2 (times a c) (times b c) (div a b) (mod (times a c) (times b c)) (div a b) (times c (mod a b)) (eq-ind-r lzero lzero nat (div (times a c) (times b c)) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (times a c) (times b c))) -> div-mod-spec (times a c) (times b c) x (mod (times a c) (times b c))) (div-mod-spec-div-mod (times a c) (times b c) (eq-coerc lzero (lt (times O O) (times b c)) (lt O (times b c)) (lt-times O b O c posb posc) (rewrite-l lzero (lsuc lzero) nat O (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (times b c)) (lt O (times b c))) (refl (lsuc lzero) (Set (lzero)) (lt O (times b c))) (times O O) (times-O-n O)))) (div a b) (div-times-times a b c posc posb)) (div-mod-spec-intro (times a c) (times b c) (div a b) (times c (mod a b)) (eq-coerc lzero (lt (times c (mod a b)) (times c b)) (lt (times c (mod a b)) (times b c)) (monotonic-lt-times-r c posc (mod a b) b (lt-mod-m-m a b posb)) (rewrite-r lzero (lsuc lzero) nat (times b c) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (times c (mod a b)) X--) (lt (times c (mod a b)) (times b c))) (refl (lsuc lzero) (Set (lzero)) (lt (times c (mod a b)) (times b c))) (times c b) (commutative-times c b))) (eq-coerc lzero (eq lzero nat (times a c) (times (plus (times b (div a b)) (mod a b)) c)) (eq lzero nat (times a c) (plus (times (div a b) (times b c)) (times c (mod a b)))) (eq-f lzero lzero nat nat (λ (x : nat) -> times x c) a (plus (times b (div a b)) (mod a b)) (rewrite-r lzero lzero nat (plus (mod a b) (times b (div a b))) (λ (X-- : nat) -> eq lzero nat a X--) (rewrite-l lzero lzero nat a (λ (X-- : nat) -> eq lzero nat a X--) (refl lzero nat a) (plus (mod a b) (times b (div a b))) (rewrite-l lzero lzero nat (plus (times b (div a b)) (mod a b)) (λ (X-- : nat) -> eq lzero nat a X--) (rewrite-l lzero lzero nat (times (div a b) b) (λ (X-- : nat) -> eq lzero nat a (plus X-- (mod a b))) (div-mod a b) (times b (div a b)) (commutative-times (div a b) b)) (plus (mod a b) (times b (div a b))) (commutative-plus (times b (div a b)) (mod a b)))) (plus (times b (div a b)) (mod a b)) (commutative-plus (times b (div a b)) (mod a b)))) (rewrite-l lzero (lsuc lzero) nat (times c (plus (times b (div a b)) (mod a b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (times a c) X--) (eq lzero nat (times a c) (plus (times (div a b) (times b c)) (times c (mod a b))))) (rewrite-r lzero (lsuc lzero) nat (times b (times (div a b) c)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (times a c) (times c (plus (times b (div a b)) (mod a b)))) (eq lzero nat (times a c) (plus X-- (times c (mod a b))))) (rewrite-r lzero (lsuc lzero) nat (times c (div a b)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (times a c) (times c (plus (times b (div a b)) (mod a b)))) (eq lzero nat (times a c) (plus (times b X--) (times c (mod a b))))) (rewrite-r lzero (lsuc lzero) nat (plus (times b (times c (div a b))) (times c (mod a b))) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (eq lzero nat (times a c) X--) (eq lzero nat (times a c) (plus (times b (times c (div a b))) (times c (mod a b))))) (refl (lsuc lzero) (Set (lzero)) (eq lzero nat (times a c) (plus (times b (times c (div a b))) (times c (mod a b))))) (times c (plus (times b (div a b)) (mod a b))) (rewrite-l lzero lzero nat (times c (times b (div a b))) (λ (X-- : nat) -> eq lzero nat (times c (plus (times b (div a b)) (mod a b))) (plus X-- (times c (mod a b)))) (distributive-times-plus c (times b (div a b)) (mod a b)) (times b (times c (div a b))) (times-times c b (div a b)))) (times (div a b) c) (commutative-times (div a b) c)) (times (div a b) (times b c)) (times-times (div a b) b c)) (times (plus (times b (div a b)) (mod a b)) c) (commutative-times c (plus (times b (div a b)) (mod a b))))))

le-div-times-m : (a : nat) -> (i : nat) -> (m : nat) -> (X-- : lt O i) -> (X--1 : lt O m) -> le (div (times a (div m i)) m) (div a i)
le-div-times-m = λ (a : nat) -> λ (i : nat) -> λ (m : nat) -> λ (posi : lt O i) -> λ (posm : lt O m) -> transitive-le (div (times a (div m i)) m) (div (div (times a m) i) m) (div a i) (monotonic-div m posm (times a (div m i)) (div (times a m) i) (le-times-div-div-times a m i posi)) (eq-ind-r lzero lzero nat (div (div (times a m) m) i) (λ (x : nat) -> λ (X-- : eq lzero nat x (div (div (times a m) m) i)) -> le x (div a i)) (eq-ind-r lzero lzero nat a (λ (x : nat) -> λ (X-- : eq lzero nat x a) -> le (div x i) (div a i)) (le-n (div a i)) (div (times a m) m) (div-times a m posm)) (div (div (times a m) i) m) (eq-div-div-div-div i m (times a m) posi posm))