-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmatita-arithmetics-congruence.agda
54 lines (38 loc) · 37.2 KB
/
matita-arithmetics-congruence.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
open import Agda.Primitive
open import matita-basics-relations
open import matita-arithmetics-primes
open import matita-basics-logic
open import matita-arithmetics-div-and-mod
open import matita-arithmetics-nat
S-mod : (X-n : nat) -> (X-m : nat) -> nat
S-mod = λ (n : nat) -> λ (m : nat) -> mod (S m) n
congruent : (X-n : nat) -> (X-m : nat) -> (X-p : nat) -> Set (lzero)
congruent = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> eq lzero nat (mod n p) (mod m p)
congruent-n-n : (n : nat) -> (p : nat) -> congruent n n p
congruent-n-n = λ (n : nat) -> λ (p : nat) -> refl lzero nat (mod n p)
transitive-congruent : (p : nat) -> transitive lzero lzero nat (λ (n : nat) -> λ (m : nat) -> congruent n m p)
transitive-congruent = λ (p : nat) -> λ (x : nat) -> λ (y : nat) -> λ (z : nat) -> λ (auto : congruent x y p) -> λ (auto' : congruent y z p) -> rewrite-l lzero lzero nat (mod x p) (λ (X-- : nat) -> eq lzero nat (mod x p) X--) (refl lzero nat (mod x p)) (mod z p) (rewrite-r lzero lzero nat (mod y p) (λ (X-- : nat) -> eq lzero nat X-- (mod z p)) auto' (mod x p) auto)
le-to-mod : (n : nat) -> (m : nat) -> (X-- : lt n m) -> eq lzero nat n (mod n m)
le-to-mod = λ (n : nat) -> λ (m : nat) -> λ (ltnm : lt n m) -> div-mod-spec-to-eq2 n m O n (div n m) (mod n m) (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))) (div-mod-spec-intro n m (div n m) (mod n m) (lt-mod-m-m n m (ltn-to-ltO n m ltnm)) (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)))
mod-mod : (n : nat) -> (p : nat) -> (X-- : lt O p) -> eq lzero nat (mod n p) (mod (mod n p) p)
mod-mod = λ (n : nat) -> λ (p : nat) -> λ (posp : lt O p) -> eq-ind-r lzero lzero nat (plus (times (div (mod n p) p) p) (mod (mod n p) p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div (mod n p) p) p) (mod (mod n p) p))) -> eq lzero nat x (mod (mod n p) p)) (eq-ind-r lzero lzero nat O (λ (x : nat) -> λ (X-- : eq lzero nat x O) -> eq lzero nat (plus (times x p) (mod (mod n p) p)) (mod (mod n p) p)) (rewrite-r lzero lzero nat (times p O) (λ (X-- : nat) -> eq lzero nat (plus X-- (mod (mod n p) p)) (mod (mod n p) p)) (rewrite-l lzero lzero nat O (λ (X-- : nat) -> eq lzero nat (plus X-- (mod (mod n p) p)) (mod (mod n p) p)) (rewrite-l lzero lzero nat (mod (mod n p) p) (λ (X-- : nat) -> eq lzero nat X-- (mod (mod n p) p)) (refl lzero nat (mod (mod n p) p)) (plus O (mod (mod n p) p)) (plus-O-n (mod (mod n p) p))) (times p O) (times-n-O p)) (times O p) (commutative-times O p)) (div (mod n p) p) (eq-div-O (mod n p) p (lt-mod-m-m n p posp))) (mod n p) (div-mod (mod n p) p)
mod-times-mod : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt O p) -> (X--1 : lt O m) -> eq lzero nat (mod n p) (mod (mod n (times m p)) p)
mod-times-mod = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (posp : lt O p) -> λ (posm : lt O m) -> div-mod-spec-to-eq2 n p (div n p) (mod n p) (plus (times (div n (times m p)) m) (div (mod n (times m p)) p)) (mod (mod n (times m p)) p) (div-mod-spec-div-mod n p posp) (div-mod-spec-intro n p (plus (times (div n (times m p)) m) (div (mod n (times m p)) p)) (mod (mod n (times m p)) p) (lt-mod-m-m (mod n (times m p)) p posp) (eq-ind-r lzero lzero nat (plus (times (times (div n (times m p)) m) p) (times (div (mod n (times m p)) p) p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (times (div n (times m p)) m) p) (times (div (mod n (times m p)) p) p))) -> eq lzero nat n (plus x (mod (mod n (times m p)) p))) (eq-ind-r lzero lzero nat (plus (times (times (div n (times m p)) m) p) (plus (times (div (mod n (times m p)) p) p) (mod (mod n (times m p)) p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (times (div n (times m p)) m) p) (plus (times (div (mod n (times m p)) p) p) (mod (mod n (times m p)) p)))) -> eq lzero nat n x) (eq-ind lzero lzero nat (mod n (times m p)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (mod n (times m p)) x-1) -> eq lzero nat n (plus (times (times (div n (times m p)) m) p) x-1)) (rewrite-r lzero lzero nat (times m (div n (times m p))) (λ (X-- : nat) -> eq lzero nat n (plus (times X-- p) (mod n (times m p)))) (rewrite-r lzero lzero nat (times p (times m (div n (times m p)))) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n (times m p)))) (rewrite-r lzero lzero nat (times m (times p (div n (times m p)))) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n (times m p)))) (rewrite-r lzero lzero nat (plus (mod n (times m p)) (times m (times p (div n (times m p))))) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-r lzero lzero nat (plus (mod n (times m p)) (times m (times p (div n (times m p))))) (λ (X-- : nat) -> eq lzero nat X-- (plus (mod n (times m p)) (times m (times p (div n (times m p)))))) (refl lzero nat (plus (mod n (times m p)) (times m (times p (div n (times m p)))))) n (rewrite-l lzero lzero nat (times (times m p) (div n (times m p))) (λ (X-- : nat) -> eq lzero nat n (plus (mod n (times m p)) X--)) (rewrite-l lzero lzero nat (plus (times (times m p) (div n (times m p))) (mod n (times m p))) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n (times m p)) (times m p)) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n (times m p)))) (div-mod n (times m p)) (times (times m p) (div n (times m p))) (commutative-times (div n (times m p)) (times m p))) (plus (mod n (times m p)) (times (times m p) (div n (times m p)))) (commutative-plus (times (times m p) (div n (times m p))) (mod n (times m p)))) (times m (times p (div n (times m p)))) (associative-times m p (div n (times m p))))) (plus (times m (times p (div n (times m p)))) (mod n (times m p))) (commutative-plus (times m (times p (div n (times m p)))) (mod n (times m p)))) (times p (times m (div n (times m p)))) (times-times p m (div n (times m p)))) (times (times m (div n (times m p))) p) (commutative-times (times m (div n (times m p))) p)) (times (div n (times m p)) m) (commutative-times (div n (times m p)) m)) (plus (times (div (mod n (times m p)) p) p) (mod (mod n (times m p)) p)) (div-mod (mod n (times m p)) p)) (plus (plus (times (times (div n (times m p)) m) p) (times (div (mod n (times m p)) p) p)) (mod (mod n (times m p)) p)) (associative-plus (times (times (div n (times m p)) m) p) (times (div (mod n (times m p)) p) p) (mod (mod n (times m p)) p))) (times (plus (times (div n (times m p)) m) (div (mod n (times m p)) p)) p) (distributive-times-plus-r p (times (div n (times m p)) m) (div (mod n (times m p)) p))))
congruent-n-mod-n : (n : nat) -> (p : nat) -> (X-- : lt O p) -> congruent n (mod n p) p
congruent-n-mod-n = λ (n : nat) -> λ (p : nat) -> λ (posp : lt O p) -> mod-mod n p posp
congruent-n-mod-times : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt O p) -> (X--1 : lt O m) -> congruent n (mod n (times m p)) p
congruent-n-mod-times = λ (n : nat) -> λ (p : nat) -> λ (posp : nat) -> mod-times-mod n p posp
eq-times-plus-to-congruent : (n : nat) -> (m : nat) -> (p : nat) -> (r : nat) -> (X-- : lt O p) -> (X--1 : eq lzero nat n (plus (times r p) m)) -> congruent n m p
eq-times-plus-to-congruent = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (r : nat) -> λ (posp : lt O p) -> λ (Hn : eq lzero nat n (plus (times r p) m)) -> div-mod-spec-to-eq2 n p (div n p) (mod n p) (plus r (div m p)) (mod m p) (div-mod-spec-div-mod n p posp) (div-mod-spec-intro n p (plus r (div m p)) (mod m p) (lt-mod-m-m m p posp) (eq-ind-r lzero lzero nat (times p (plus r (div m p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times p (plus r (div m p)))) -> eq lzero nat n (plus x (mod m p))) (eq-ind-r lzero lzero nat (plus (times p r) (times p (div m p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times p r) (times p (div m p)))) -> eq lzero nat n (plus x (mod m p))) (eq-ind-r lzero lzero nat (times r p) (λ (x : nat) -> λ (X-- : eq lzero nat x (times r p)) -> eq lzero nat n (plus (plus x (times p (div m p))) (mod m p))) (eq-ind-r lzero lzero nat (times (div m p) p) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (div m p) p)) -> eq lzero nat n (plus (plus (times r p) x) (mod m p))) (eq-ind-r lzero lzero nat (plus (times r p) (plus (times (div m p) p) (mod m p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times r p) (plus (times (div m p) p) (mod m p)))) -> eq lzero nat n x) (rewrite-r lzero lzero nat (times p r) (λ (X-- : nat) -> eq lzero nat n (plus X-- (plus (times (div m p) p) (mod m p)))) (rewrite-r lzero lzero nat (times p (div m p)) (λ (X-- : nat) -> eq lzero nat n (plus (times p r) (plus X-- (mod m p)))) (rewrite-r lzero lzero nat (plus (mod m p) (times p (div m p))) (λ (X-- : nat) -> eq lzero nat n (plus (times p r) X--)) (rewrite-l lzero lzero nat m (λ (X-- : nat) -> eq lzero nat n (plus (times p r) X--)) (rewrite-r lzero lzero nat (plus m (times p r)) (λ (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 m (times p r)) (rewrite-l lzero lzero nat (plus (times p r) m) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times r p) (λ (X-- : nat) -> eq lzero nat n (plus X-- m)) Hn (times p r) (commutative-times r p)) (plus m (times p r)) (commutative-plus (times p r) m))) (plus (times p r) m) (commutative-plus (times p r) m)) (plus (mod m p) (times p (div m p))) (rewrite-l lzero lzero nat (plus (times p (div m p)) (mod m p)) (λ (X-- : nat) -> eq lzero nat m X--) (rewrite-l lzero lzero nat (times (div m p) p) (λ (X-- : nat) -> eq lzero nat m (plus X-- (mod m p))) (div-mod m p) (times p (div m p)) (commutative-times (div m p) p)) (plus (mod m p) (times p (div m p))) (commutative-plus (times p (div m p)) (mod m p)))) (plus (times p (div m p)) (mod m p)) (commutative-plus (times p (div m p)) (mod m p))) (times (div m p) p) (commutative-times (div m p) p)) (times r p) (commutative-times r p)) (plus (plus (times r p) (times (div m p) p)) (mod m p)) (associative-plus (times r p) (times (div m p) p) (mod m p))) (times p (div m p)) (commutative-times p (div m p))) (times p r) (commutative-times p r)) (times p (plus r (div m p))) (distributive-times-plus p r (div m p))) (times (plus r (div m p)) p) (commutative-times (plus r (div m p)) p)))
divides-to-congruent : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt O p) -> (X--1 : le m n) -> (X--2 : divides p (minus n m)) -> congruent n m p
divides-to-congruent = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (posp : lt O p) -> λ (lemn : le m n) -> λ (X-clearme : divides p (minus n m)) -> match-divides p (minus n m) lzero (λ (X-- : divides p (minus n m)) -> congruent n m p) (λ (q : nat) -> λ (Hdiv : eq lzero nat (minus n m) (times p q)) -> eq-times-plus-to-congruent n m p q posp (eq-ind-r lzero lzero nat (plus m (times q p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m (times q p))) -> eq lzero nat n x) (minus-to-plus n m (times q p) lemn (rewrite-r lzero lzero nat (times p q) (λ (X-- : nat) -> eq lzero nat X-- (times q p)) (rewrite-r lzero lzero nat (times p q) (λ (X-- : nat) -> eq lzero nat (times p q) X--) (refl lzero nat (times p q)) (times q p) (commutative-times q p)) (minus n m) Hdiv)) (plus (times q p) m) (commutative-plus (times q p) m))) X-clearme
congruent-to-divides : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt O p) -> (X--1 : congruent n m p) -> divides p (minus n m)
congruent-to-divides = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (posp : lt O p) -> λ (Hcong : congruent n m p) -> quotient p (minus n m) (minus (div n p) (div m p)) (eq-ind-r lzero lzero nat (times (minus (div n p) (div m p)) p) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (minus (div n p) (div m p)) p)) -> eq lzero nat (minus n m) x) (eq-ind-r lzero lzero nat (plus (times (div n p) p) (mod n p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div n p) p) (mod n p))) -> eq lzero nat (minus x m) (times (minus (div n p) (div m p)) p)) (eq-ind-r lzero lzero nat (plus (times (div m p) p) (mod m p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (div m p) p) (mod m p))) -> eq lzero nat (minus (plus (times (div n p) p) (mod n p)) x) (times (minus (div n p) (div m p)) p)) (rewrite-r lzero lzero nat (times p (div n p)) (λ (X-- : nat) -> eq lzero nat (minus (plus X-- (mod n p)) (plus (times (div m p) p) (mod m p))) (times (minus (div n p) (div m p)) p)) (rewrite-r lzero lzero nat (plus (mod n p) (times p (div n p))) (λ (X-- : nat) -> eq lzero nat (minus X-- (plus (times (div m p) p) (mod m p))) (times (minus (div n p) (div m p)) p)) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (minus X-- (plus (times (div m p) p) (mod m p))) (times (minus (div n p) (div m p)) p)) (rewrite-r lzero lzero nat (times p (div m p)) (λ (X-- : nat) -> eq lzero nat (minus n (plus X-- (mod m p))) (times (minus (div n p) (div m p)) p)) (rewrite-l lzero lzero nat (mod n p) (λ (X-- : nat) -> eq lzero nat (minus n (plus (times p (div m p)) X--)) (times (minus (div n p) (div m p)) p)) (rewrite-r lzero lzero nat (plus (mod n p) (times p (div m p))) (λ (X-- : nat) -> eq lzero nat (minus n X--) (times (minus (div n p) (div m p)) p)) (rewrite-l lzero lzero nat (minus (minus n (mod n p)) (times p (div m p))) (λ (X-- : nat) -> eq lzero nat X-- (times (minus (div n p) (div m p)) p)) (rewrite-l lzero lzero nat (times p (div n p)) (λ (X-- : nat) -> eq lzero nat (minus X-- (times p (div m p))) (times (minus (div n p) (div m p)) p)) (rewrite-l lzero lzero nat (times p (minus (div n p) (div m p))) (λ (X-- : nat) -> eq lzero nat X-- (times (minus (div n p) (div m p)) p)) (rewrite-r lzero lzero nat (times p (minus (div n p) (div m p))) (λ (X-- : nat) -> eq lzero nat (times p (minus (div n p) (div m p))) X--) (refl lzero nat (times p (minus (div n p) (div m p)))) (times (minus (div n p) (div m p)) p) (commutative-times (minus (div n p) (div m p)) p)) (minus (times p (div n p)) (times p (div m p))) (distributive-times-minus p (div n p) (div m p))) (minus n (mod n p)) (rewrite-l lzero lzero nat (times (div n p) p) (λ (X-- : nat) -> eq lzero nat X-- (minus n (mod n p))) (eq-times-div-minus-mod n p) (times p (div n p)) (commutative-times (div n p) p))) (minus n (plus (mod n p) (times p (div m p)))) (minus-plus n (mod n p) (times p (div m p)))) (plus (times p (div m p)) (mod n p)) (commutative-plus (times p (div m p)) (mod n p))) (mod m p) Hcong) (times (div m p) p) (commutative-times (div m p) p)) (plus (mod n p) (times p (div n p))) (rewrite-l lzero lzero nat (plus (times p (div n p)) (mod n p)) (λ (X-- : nat) -> eq lzero nat n X--) (rewrite-l lzero lzero nat (times (div n p) p) (λ (X-- : nat) -> eq lzero nat n (plus X-- (mod n p))) (div-mod n p) (times p (div n p)) (commutative-times (div n p) p)) (plus (mod n p) (times p (div n p))) (commutative-plus (times p (div n p)) (mod n p)))) (plus (times p (div n p)) (mod n p)) (commutative-plus (times p (div n p)) (mod n p))) (times (div n p) p) (commutative-times (div n p) p)) m (div-mod m p)) n (div-mod n p)) (times p (minus (div n p) (div m p))) (commutative-times p (minus (div n p) (div m p))))
let-clause-1034' : (n : nat) -> (m : nat) -> (p : nat) -> (posp : lt O p) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (mod x2515 x2516) (times x2516 (div x2515 x2516)))
let-clause-1034' = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (posp : lt O p) -> λ (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))
let-clause-73' : (n : nat) -> (m : nat) -> (p : nat) -> (posp : lt O p) -> (x134 : nat) -> (x135 : nat) -> (x136 : nat) -> eq lzero nat (plus x134 (plus x135 x136)) (plus x135 (plus x134 x136))
let-clause-73' = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (posp : lt O p) -> λ (x134 : nat) -> λ (x135 : nat) -> λ (x136 : nat) -> rewrite-l lzero lzero nat (plus (plus x135 x134) x136) (λ (X-- : nat) -> eq lzero nat (plus x134 (plus x135 x136)) X--) (assoc-plus1 x136 x135 x134) (plus x135 (plus x134 x136)) (associative-plus x135 x134 x136)
mod-times : (n : nat) -> (m : nat) -> (p : nat) -> (X-- : lt O p) -> eq lzero nat (mod (times n m) p) (mod (times (mod n p) (mod m p)) p)
mod-times = λ (n : nat) -> λ (m : nat) -> λ (p : nat) -> λ (posp : lt O p) -> eq-times-plus-to-congruent (times n m) (times (mod n p) (mod m p)) p (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) posp (trans-eq lzero nat (times n m) (times (plus (times (div n p) p) (mod n p)) (plus (times (div m p) p) (mod m p))) (plus (times (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) p) (times (mod n p) (mod m p))) (rewrite-r lzero lzero nat (times p (div n p)) (λ (X-- : nat) -> eq lzero nat (times n m) (times (plus X-- (mod n p)) (plus (times (div m p) p) (mod m p)))) (rewrite-r lzero lzero nat (plus (mod n p) (times p (div n p))) (λ (X-- : nat) -> eq lzero nat (times n m) (times X-- (plus (times (div m p) p) (mod m p)))) (rewrite-l lzero lzero nat n (λ (X-- : nat) -> eq lzero nat (times n m) (times X-- (plus (times (div m p) p) (mod m p)))) (rewrite-r lzero lzero nat (times p (div m p)) (λ (X-- : nat) -> eq lzero nat (times n m) (times n (plus X-- (mod m p)))) (rewrite-r lzero lzero nat (plus (mod m p) (times p (div m p))) (λ (X-- : nat) -> eq lzero nat (times n m) (times n X--)) (rewrite-l lzero lzero nat m (λ (X-- : nat) -> eq lzero nat (times n m) (times n X--)) (refl lzero nat (times n m)) (plus (mod m p) (times p (div m p))) (let-clause-1034' n m p posp m p)) (plus (times p (div m p)) (mod m p)) (commutative-plus (times p (div m p)) (mod m p))) (times (div m p) p) (commutative-times (div m p) p)) (plus (mod n p) (times p (div n p))) (let-clause-1034' n m p posp n p)) (plus (times p (div n p)) (mod n p)) (commutative-plus (times p (div n p)) (mod n p))) (times (div n p) p) (commutative-times (div n p) p)) (trans-eq lzero nat (times (plus (times (div n p) p) (mod n p)) (plus (times (div m p) p) (mod m p))) (plus (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (mod n p) (mod m p))) (plus (times (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) p) (times (mod n p) (mod m p))) (eq-ind-r lzero lzero nat (plus (times (times (div n p) p) (plus (times (div m p) p) (mod m p))) (times (mod n p) (plus (times (div m p) p) (mod m p)))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (times (div n p) p) (plus (times (div m p) p) (mod m p))) (times (mod n p) (plus (times (div m p) p) (mod m p))))) -> eq lzero nat x (plus (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (mod n p) (mod m p)))) (eq-ind-r lzero lzero nat (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p)))) -> eq lzero nat (plus x (times (mod n p) (plus (times (div m p) p) (mod m p)))) (plus (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (mod n p) (mod m p)))) (eq-ind-r lzero lzero nat (plus (times (mod n p) (times (div m p) p)) (times (mod n p) (mod m p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (mod n p) (times (div m p) p)) (times (mod n p) (mod m p)))) -> eq lzero nat (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) x) (plus (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (mod n p) (mod m p)))) (rewrite-l lzero lzero nat (plus (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (mod n p) (mod m p))) (λ (X-- : nat) -> eq lzero nat X-- (plus (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (mod n p) (mod m p)))) (refl lzero nat (plus (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (mod n p) (mod m p)))) (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (plus (times (mod n p) (times (div m p) p)) (times (mod n p) (mod m p)))) (associative-plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p)) (times (mod n p) (mod m p)))) (times (mod n p) (plus (times (div m p) p) (mod m p))) (distributive-times-plus (mod n p) (times (div m p) p) (mod m p))) (times (times (div n p) p) (plus (times (div m p) p) (mod m p))) (distributive-times-plus (times (div n p) p) (times (div m p) p) (mod m p))) (times (plus (times (div n p) p) (mod n p)) (plus (times (div m p) p) (mod m p))) (distributive-times-plus-r (plus (times (div m p) p) (mod m p)) (times (div n p) p) (mod n p))) (eq-f2 lzero lzero lzero nat nat nat plus (plus (plus (times (times (div n p) p) (times (div m p) p)) (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) p) (times (mod n p) (mod m p)) (times (mod n p) (mod m p)) (eq-ind lzero lzero nat (times (times (times (div n p) p) (div m p)) p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (times (div n p) p) (div m p)) p) x-1) -> eq lzero nat (plus (plus x-1 (times (times (div n p) p) (mod m p))) (times (mod n p) (times (div m p) p))) (times (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) p)) (eq-ind-r lzero lzero nat (times (div n p) (times p (mod m p))) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (div n p) (times p (mod m p)))) -> eq lzero nat (plus (plus (times (times (times (div n p) p) (div m p)) p) x) (times (mod n p) (times (div m p) p))) (times (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) p)) (eq-ind-r lzero lzero nat (times (mod m p) p) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (mod m p) p)) -> eq lzero nat (plus (plus (times (times (times (div n p) p) (div m p)) p) (times (div n p) x)) (times (mod n p) (times (div m p) p))) (times (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) p)) (eq-ind lzero lzero nat (times (times (div n p) (mod m p)) p) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (times (times (div n p) (mod m p)) p) x-1) -> eq lzero nat (plus (plus (times (times (times (div n p) p) (div m p)) p) x-1) (times (mod n p) (times (div m p) p))) (times (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) p)) (eq-ind-r lzero lzero nat (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) -> eq lzero nat (plus (plus (times (times (times (div n p) p) (div m p)) p) (times (times (div n p) (mod m p)) p)) (times (mod n p) (times (div m p) p))) x) (rewrite-r lzero lzero nat (times p (div n p)) (λ (X-- : nat) -> eq lzero nat (plus (plus (times (times X-- (div m p)) p) (times (times (div n p) (mod m p)) p)) (times (mod n p) (times (div m p) p))) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times (div m p) (times p (div n p))) (λ (X-- : nat) -> eq lzero nat (plus (plus (times X-- p) (times (times (div n p) (mod m p)) p)) (times (mod n p) (times (div m p) p))) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times p (times (div m p) (div n p))) (λ (X-- : nat) -> eq lzero nat (plus (plus (times X-- p) (times (times (div n p) (mod m p)) p)) (times (mod n p) (times (div m p) p))) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times (div n p) (div m p)) (λ (X-- : nat) -> eq lzero nat (plus (plus (times (times p X--) p) (times (times (div n p) (mod m p)) p)) (times (mod n p) (times (div m p) p))) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times p (times p (times (div n p) (div m p)))) (λ (X-- : nat) -> eq lzero nat (plus (plus X-- (times (times (div n p) (mod m p)) p)) (times (mod n p) (times (div m p) p))) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times p (times (div n p) (mod m p))) (λ (X-- : nat) -> eq lzero nat (plus (plus (times p (times p (times (div n p) (div m p)))) X--) (times (mod n p) (times (div m p) p))) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-l lzero lzero nat (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (λ (X-- : nat) -> eq lzero nat (plus X-- (times (mod n p) (times (div m p) p))) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times p (div m p)) (λ (X-- : nat) -> eq lzero nat (plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (times (mod n p) X--)) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times p (times (mod n p) (div m p))) (λ (X-- : nat) -> eq lzero nat (plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) X--) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times (div m p) (mod n p)) (λ (X-- : nat) -> eq lzero nat (plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (times p X--)) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (plus (times p (times (div m p) (mod n p))) (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-l lzero lzero nat (times p (plus (times (div m p) (mod n p)) (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))))) (λ (X-- : nat) -> eq lzero nat X-- (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (plus (times p (times (div n p) (div m p))) (plus (times (div m p) (mod n p)) (times (div n p) (mod m p)))) (λ (X-- : nat) -> eq lzero nat (times p X--) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) X--)) (plus (times (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times p (div n p)) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (plus (times (plus (times X-- (div m p)) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times (div m p) (times p (div n p))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (plus (times (plus X-- (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times p (times (div m p) (div n p))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (plus (times (plus X-- (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times (div n p) (div m p)) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (plus (times (plus (times p X--) (times (div n p) (mod m p))) p) (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (plus X-- (times (times (mod n p) (div m p)) p))) (rewrite-r lzero lzero nat (times (div m p) (mod n p)) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (times X-- p))) (rewrite-r lzero lzero nat (times p (times (div m p) (mod n p))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) X--)) (rewrite-r lzero lzero nat (plus (times p (times (div m p) (mod n p))) (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) X--) (rewrite-l lzero lzero nat (times p (plus (times (div m p) (mod n p)) (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) X--) (rewrite-r lzero lzero nat (plus (times p (times (div n p) (div m p))) (plus (times (div m p) (mod n p)) (times (div n p) (mod m p)))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (times p X--)) (rewrite-r lzero lzero nat (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))) (λ (X-- : nat) -> eq lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p))))) (times p (plus (times p (times (div n p) (div m p))) X--))) (refl lzero nat (times p (plus (times p (times (div n p) (div m p))) (plus (times (div n p) (mod m p)) (times (div m p) (mod n p)))))) (plus (times (div m p) (mod n p)) (times (div n p) (mod m p))) (commutative-plus (times (div m p) (mod n p)) (times (div n p) (mod m p)))) (plus (times (div m p) (mod n p)) (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (let-clause-73' n m p posp (times (div m p) (mod n p)) (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (plus (times p (times (div m p) (mod n p))) (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))))) (distributive-times-plus p (times (div m p) (mod n p)) (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))))) (plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (times p (times (div m p) (mod n p)))) (commutative-plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (times p (times (div m p) (mod n p))))) (times (times (div m p) (mod n p)) p) (commutative-times (times (div m p) (mod n p)) p)) (times (mod n p) (div m p)) (commutative-times (mod n p) (div m p))) (times (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))) p) (commutative-times (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))) p)) (times (div m p) (div n p)) (commutative-times (div m p) (div n p))) (times (div m p) (times p (div n p))) (times-times (div m p) p (div n p))) (times (times p (div n p)) (div m p)) (commutative-times (times p (div n p)) (div m p))) (times (div n p) p) (commutative-times (div n p) p)) (plus (times (div m p) (mod n p)) (times (div n p) (mod m p))) (commutative-plus (times (div m p) (mod n p)) (times (div n p) (mod m p)))) (plus (times (div m p) (mod n p)) (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (let-clause-73' n m p posp (times (div m p) (mod n p)) (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (plus (times p (times (div m p) (mod n p))) (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))))) (distributive-times-plus p (times (div m p) (mod n p)) (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p))))) (plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (times p (times (div m p) (mod n p)))) (commutative-plus (times p (plus (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (times p (times (div m p) (mod n p))))) (times (mod n p) (div m p)) (commutative-times (mod n p) (div m p))) (times (mod n p) (times p (div m p))) (times-times (mod n p) p (div m p))) (times (div m p) p) (commutative-times (div m p) p)) (plus (times p (times p (times (div n p) (div m p)))) (times p (times (div n p) (mod m p)))) (distributive-times-plus p (times p (times (div n p) (div m p))) (times (div n p) (mod m p)))) (times (times (div n p) (mod m p)) p) (commutative-times (times (div n p) (mod m p)) p)) (times (times p (times (div n p) (div m p))) p) (commutative-times (times p (times (div n p) (div m p))) p)) (times (div m p) (div n p)) (commutative-times (div m p) (div n p))) (times (div m p) (times p (div n p))) (times-times (div m p) p (div n p))) (times (times p (div n p)) (div m p)) (commutative-times (times p (div n p)) (div m p))) (times (div n p) p) (commutative-times (div n p) p)) (times (plus (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p))) p) (distributive-times-plus-r p (plus (times (times (div n p) p) (div m p)) (times (div n p) (mod m p))) (times (mod n p) (div m p)))) (times (div n p) (times (mod m p) p)) (associative-times (div n p) (mod m p) p)) (times p (mod m p)) (commutative-times p (mod m p))) (times (times (div n p) p) (mod m p)) (associative-times (div n p) p (mod m p))) (times (times (div n p) p) (times (div m p) p)) (associative-times (times (div n p) p) (div m p) p)) (refl lzero nat (times (mod n p) (mod m p))))))
congruent-times : (n : nat) -> (m : nat) -> (n1 : nat) -> (m1 : nat) -> (p : nat) -> (X-- : lt O p) -> (X--1 : congruent n n1 p) -> (X--2 : congruent m m1 p) -> congruent (times n m) (times n1 m1) p
congruent-times = λ (n : nat) -> λ (m : nat) -> λ (n1 : nat) -> λ (m1 : nat) -> λ (p : nat) -> λ (posp : lt O p) -> λ (Hcongn : congruent n n1 p) -> λ (Hcongm : congruent m m1 p) -> eq-ind-r lzero lzero nat (mod (times (mod n p) (mod m p)) p) (λ (x : nat) -> λ (X-- : eq lzero nat x (mod (times (mod n p) (mod m p)) p)) -> eq lzero nat x (mod (times n1 m1) p)) (eq-ind-r lzero lzero nat (mod n1 p) (λ (x : nat) -> λ (X-- : eq lzero nat x (mod n1 p)) -> eq lzero nat (mod (times x (mod m p)) p) (mod (times n1 m1) p)) (eq-ind-r lzero lzero nat (mod m1 p) (λ (x : nat) -> λ (X-- : eq lzero nat x (mod m1 p)) -> eq lzero nat (mod (times (mod n1 p) x) p) (mod (times n1 m1) p)) (sym-eq lzero nat (mod (times n1 m1) p) (mod (times (mod n1 p) (mod m1 p)) p) (mod-times n1 m1 p posp)) (mod m p) Hcongm) (mod n p) Hcongn) (mod (times n m) p) (mod-times n m p posp)