Comment: num_thy_1_summary
Elementary divisibility theory over the integers.
Gcd function and relation introduced. Chinese remainder
theorem proven. 

Comment: num_thy_1_intro
Some elementary number theory is developed. Theory
demonstrates rewriter handling multiple equality and 
inequality relations over the integers.

The approach taken here is similar to that taken in 
the factor_1 theory in the algebra theory collection.  

Definition: divides
==  ∃c:ℤ(a (b c) ∈ ℤ)

Lemma: divides_wf
[a,b:ℤ].  (a b ∈ ℙ)

Lemma: comb_for_divides_wf
λa,b,z. (a b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ

Lemma: zero_divs_only_zero
[a:ℤ]. 0 ∈ ℤ supposing a

Lemma: one_divs_any
a:ℤ(1 a)

Lemma: any_divs_zero
b:ℤ(b 0)

Lemma: divides_invar_1
a,b:ℤ.  (a ⇐⇒ (-a) b)

Lemma: divides_invar_2
a,b:ℤ.  (a ⇐⇒ (-b))

Lemma: divisors_bound
[a:ℕ]. ∀[b:ℕ+].  a ≤ supposing b

Lemma: only_pm_one_divs_one
b:ℤ((b 1)  = ± 1)

Lemma: divides_of_absvals
a,b:ℤ.  (|a| |b| ⇐⇒ b)

Lemma: absval-divides
a,b:ℤ.  (|a| ⇐⇒ b)

Lemma: divides_reflexivity
a:ℤ(a a)

Lemma: divides_transitivity
a,b,c:ℤ.  ((a b)  (b c)  (a c))

Lemma: divides_preorder
Preorder(ℤ;x,y.x y)

Lemma: divides_anti_sym_n
[a,b:ℕ].  (a b ∈ ℤsupposing ((b a) and (a b))

Lemma: divides_anti_sym
a,b:ℤ.  ((a b)  (b a)  = ± b)

Lemma: assoc_reln
a,b:ℤ.  ((a b) ∧ (b a) ⇐⇒ = ± b)

Lemma: divisor_of_sum
a,b1,b2:ℤ.  ((a b1)  (a b2)  (a (b1 b2)))

Lemma: divisor_of_minus
a,b:ℤ.  ((a b)  (a (-b)))

Lemma: divisor_of_mul
a,b,c:ℤ.  ((a b)  (a (b c)))

Lemma: divides_mul
a,b:ℤ.  ((a b)  (∀n:ℤ((n a) (n b))))

Lemma: divides_add
x,y,z:ℤ.  ((x y)  (x z)  (x (y z)))

Lemma: divides_subtract
x,y,z:ℤ.  ((x y)  (x z)  (x (y z)))

Lemma: divides_product
x,y,z:ℤ.  (((x y) ∨ (x z))  (x (y z)))

Lemma: divisor_bound
[a:ℕ]. ∀[b:ℕ+].  a ≤ supposing b

Lemma: divides_iff_rem_zero
a:ℤ. ∀b:ℤ-o.  (b ⇐⇒ (a rem b) 0 ∈ ℤ)

Lemma: divides_iff_div_exact
a:ℤ. ∀n:ℤ-o.  (n ⇐⇒ ((a ÷ n) n) a ∈ ℤ)

Lemma: decidable__divides
a,b:ℤ.  Dec(a b)

Lemma: decidable__divides_ext
a,b:ℤ.  Dec(a b)

Lemma: decidable__exists-divisor
n:ℕ+. ∀P:ℕ ⟶ ℙ.  ((∀d:ℕDec(P[d]))  Dec(∃d:ℕ((d n) ∧ P[d])))

Lemma: add-div-when-divides
a,b:ℤ. ∀c:ℤ-o.  (((a ÷ c) (b ÷ c)) ((a b) ÷ c) ∈ ℤsupposing ((c a) and (c b))

Lemma: add-div-when-divides2
a,b,x,y:ℤ. ∀c:ℤ-o.  ((((a ÷ c) x) ((b ÷ c) y)) (((a x) (b y)) ÷ c) ∈ ℤsupposing ((c a) and (c b))

Comment: divides_instance_com
The proof here illustrates how the evaluation
of the extract of one theorem (decidable__divides)
can help to prove another theorem.

For neatness, the pattern of proof here could easily
be incorporated into tactic.

Lemma: divides_instance

Lemma: orbit-size-divides-order
[T:Type]. ∀f:T ⟶ T. ∀n:ℕ.  ∀L:T List. ||L|| supposing orbit(T;f;L) supposing ∀x:T. ((f^n x) x ∈ T)

Comment: gcd_p_com
Should redo this not using uncurried antecedents.
Makes forward chaining lot easier.

Definition: assoced
==  (a b) ∧ (b a)

Lemma: assoced_wf
[a,b:ℤ].  (a b ∈ ℙ)

Lemma: comb_for_assoced_wf
λa,b,z. (a b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ

Lemma: assoced_equiv_rel
EquivRel(ℤ;x,y.x y)

Lemma: decidable__assoced
a,b:ℤ.  Dec(a b)

Lemma: divides_functionality_wrt_assoced
a,a',b,b':ℤ.  ((a a')  (b b')  (a ⇐⇒ a' b'))

Lemma: divides_weakening
a,b:ℤ.  ((a b)  (a b))

Lemma: assoced_weakening
a,b:ℤ.  supposing b ∈ ℤ

Lemma: assoced_transitivity
a,b,c:ℤ.  ((a b)  (b c)  (a c))

Lemma: multiply_functionality_wrt_assoced
a,a',b,b':ℤ.  ((a a')  (b b')  ((a b) (a' b')))

Lemma: assoced_inversion
a,b:ℤ.  ((a b)  (b a))

Lemma: assoced_functionality_wrt_assoced
a,b,a',b':ℤ.  ((a a')  (b b')  (a ⇐⇒ a' b'))

Lemma: assoced_elim
a,b:ℤ.  (a ⇐⇒ (a b ∈ ℤ) ∨ (a (-b) ∈ ℤ))

Lemma: mul_cancel_in_assoced
a,b:ℤ. ∀n:ℤ-o.  (((n a) (n b))  (a b))

Lemma: neg_assoced
a:ℤ((-a) a)

Lemma: absval_assoced
a:ℤ(|a| a)

Lemma: unit_chars
a:ℤ(a ⇐⇒ 1)

Lemma: assoced_nelim
a,b:ℕ.  (a ⇐⇒ b ∈ ℤ)

Lemma: pdivisor_bound
a:ℕ. ∀b:ℕ+.  ((a b) ∧ (b a)) ⇐⇒ a < b ∧ (a b))

Lemma: divides_nchar
a,b:ℕ+.  (a ⇐⇒ ∃c:ℕ+(b (a c) ∈ ℕ+))

Definition: gcd_p
GCD(a;b;y) ==  (y a) ∧ (y b) ∧ (∀z:ℤ(((z a) ∧ (z b))  (z y)))

Lemma: gcd_p_wf
[a,b,y:ℤ].  (GCD(a;b;y) ∈ ℙ)

Lemma: comb_for_gcd_p_wf
λa,b,y,z. GCD(a;b;y) ∈ a:ℤ ⟶ b:ℤ ⟶ y:ℤ ⟶ (↓True) ⟶ ℙ

Lemma: gcd_p_functionality_wrt_assoced
a,a',b,b',y,y':ℤ.  ((a a')  (b b')  (y y')  (GCD(a;b;y) ⇐⇒ GCD(a';b';y')))

Lemma: gcd_p_eq_args

Lemma: gcd_p_zero

Lemma: gcd_p_one

Lemma: gcd_p_zero_rel
a,b:ℤ.  (GCD(a;0;b)  ((a b ∈ ℤ) ∨ (a (-b) ∈ ℤ)))

Lemma: gcd_p_sym
a,b,y:ℤ.  (GCD(a;b;y)  GCD(b;a;y))

Lemma: gcd_p_sym_a
a,b,y:ℤ.  (GCD(a;b;y)  GCD(b;a;y))

Lemma: gcd_p_neg_arg
a,b,y:ℤ.  (GCD(a;b;y)  GCD(a;-b;y))

Lemma: gcd_p_neg_arg_a
a,b,y:ℤ.  (GCD(a;b;y)  GCD(-a;b;y))

Lemma: gcd_p_neg_arg_2
a,b,y:ℤ.  (GCD(a;b;y) ⇐⇒ GCD(a;-b;y))

Lemma: gcd_p_shift
a,b,y,k:ℤ.  (GCD(a;b;y)  GCD(a;b (k a);y))

Lemma: gcd_unique
a,b,y1,y2:ℤ.  (GCD(a;b;y1)  GCD(a;b;y2)  (y1 y2))

Lemma: gcd_of_triple
  (GCD(a;b;x)  GCD(x;c;y)  (((y a) ∧ (y b) ∧ (y c)) ∧ (∀z:ℤ((z a)  (z b)  (z c)  (z y)))))

Lemma: gcd_sat_gcd_p
a,b:ℤ.  GCD(a;b;gcd(a;b))

Lemma: gcd_sat_pred
a,b:ℤ.  GCD(a;b;gcd(a;b))

Lemma: gcd_elim
a,b:ℤ.  ∃y:ℤ(GCD(a;b;y) ∧ (gcd(a;b) y ∈ ℤ))

Lemma: gcd_sym
a,b:ℤ.  (gcd(a;b) gcd(b;a))

Lemma: gcd_eq_args
a:ℤ(gcd(a;a) a)

Lemma: gcd_is_divisor_1
a,b:ℤ.  (gcd(a;b) a)

Lemma: gcd_is_divisor_2
a,b:ℤ.  (gcd(a;b) b)

Lemma: gcd_is_gcd
a,b,c:ℤ.  ((c a)  (c b)  (c gcd(a;b)))

Lemma: gcd_properties
a,b:ℤ.  (((gcd(a;b) a) ∧ (gcd(a;b) b)) ∧ (∀c:ℤ((c a)  (c b)  (c gcd(a;b)))))

Comment: quot_rem_exists_com
The and computed by the extracts of these theorems are
not the same as those returned by the divides(a;b) and 
remainder(a;b) built-in arithmetic functions: with those
functions, the sign of follows the sign of and div
has simple symmetry properties. Here, things are set up
so that the same inequalities for are satisfied over
adjacent quadrants of a,b: is closer to the `mod'
function. This makes the gcd_exists and bezout_ident_ 
theorems simpler to prove, since two quadrants can be 
easily taken care of on the first induction.

Lemma: quot_rem_exists_n
a:ℕ. ∀b:ℕ+.  ∃q:ℕ. ∃r:ℕb. (a ((q b) r) ∈ ℤ)

Lemma: quot_rem_exists
a:ℤ. ∀b:ℕ+.  ∃q:ℤ. ∃r:ℕb. (a ((q b) r) ∈ ℤ)

Lemma: gcd_exists_n
b:ℕ. ∀a:ℤ.  ∃y:ℤGCD(a;b;y)

Lemma: gcd_ex_n
b:ℕ. ∀a:ℤ.  (∃y:ℤ [GCD(a;b;y)])

Lemma: gcd_exists
a,b:ℤ.  ∃y:ℤGCD(a;b;y)

Lemma: bezout_ident_n
b:ℕ. ∀a:ℤ.  ∃u,v:ℤGCD(a;b;(u a) (v b))

Lemma: bezout_ident
a,b:ℤ.  ∃u,v:ℤGCD(a;b;(u a) (v b))

Lemma: gcd_p_mul
a,b,y,n:ℤ.  (GCD(a;b;y)  GCD(n a;n b;n y))

Lemma: gcd_mul
a,b,n:ℤ.  ((n gcd(a;b)) gcd(n a;n b))

Lemma: gcd_assoc
a,b,c:ℤ.  (gcd(gcd(a;b);c) gcd(a;gcd(b;c)))

Definition: coprime
CoPrime(a,b) ==  GCD(a;b;1)

Lemma: coprime_wf
[a,b:ℤ].  (CoPrime(a,b) ∈ ℙ)

Lemma: coprime_inversion
a,b:ℤ.  (CoPrime(a,b) ⇐⇒ CoPrime(b,a))

Lemma: comb_for_coprime_wf
λa,b,z. CoPrime(a,b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ

Lemma: sq_stable__coprime
i,j:ℤ.  SqStable(CoPrime(i,j))

Comment: prime_com
We follow more abstract characterization of primeness here,
defining separately notions of primeness and irreducibility. 

See algebra/factor_1 theory for more details of this. 

Approach here to dealing with in lemmas and definitions has
been bit ad-hoc. Is there something more principled that 
could be done? 

Definition: reducible
reducible(a) ==  ∃b,c:ℤ-o((¬(b 1)) ∧ (c 1)) ∧ (a (b c) ∈ ℤ))

Lemma: reducible_wf
[a:ℤ]. (reducible(a) ∈ ℙ)

Definition: atomic
atomic(a) ==  (a 0 ∈ ℤ)) ∧ (a 1)) ∧ reducible(a))

Lemma: atomic_wf
[a:ℤ]. (atomic(a) ∈ ℙ)

Comment: atomic_char_com
This theorem was quite tedious to prove. 
Could the proof be simpler?

7/7/98 Proof changed to avoid use of 
sq_stable_iff_stable which has inappropriate 
use of Xmiddle. The first tactic proving the first
subgoal was modified. See theory not_good for old

Lemma: atomic_char
a:ℤ(atomic(a) ⇐⇒ {(¬(a 1)) ∧ (∀b:ℤ((b a)  ((b 1) ∨ (b a))))})

Definition: prime
prime(a) ==  (a 0 ∈ ℤ)) ∧ (a 1)) ∧ (∀b,c:ℤ.  ((a (b c))  ((a b) ∨ (a c))))

Lemma: prime_wf
[a:ℤ]. (prime(a) ∈ ℙ)

Lemma: self_divisor_mul
a:ℤ-o. ∀b:ℤ.  (((a b) a)  (b 1))

Lemma: prime_imp_atomic
[a:ℤ]. atomic(a) supposing prime(a)

Lemma: prime_elim
p:ℤ(prime(p)  ((¬(p 0 ∈ ℤ)) ∧ (p 1)) ∧ (∀a:ℤ((a p)  ((a 1) ∨ (a p))))))

Lemma: assoced-prime
p,q:ℤ.  ((p q)  prime(p)  prime(q))

Lemma: prime-mul
x,y:ℤ.  (prime(x y)  ((x 1) ∨ (y 1)))

Lemma: prime-mult
n:{2...}. ∀x:ℤ.  (prime(n x)  (prime(n) ∧ (x 1)))

Lemma: not-prime-mult
[n,m:{2...}]. ∀[x:ℤ].  prime((n m) x))

Lemma: not-prime-square
[x:ℤ]. prime(x x))

Lemma: coprime_intro
a,b:ℤ.  ((∀c:ℤ((c a)  (c b)  (c 1)))  CoPrime(a,b))

Lemma: coprime_elim
a,b:ℤ.  (CoPrime(a,b) ⇐⇒ ∀c:ℤ((c a)  (c b)  (c 1)))

Lemma: coprime_elim_a
a,b:ℤ.  (CoPrime(a,b) ⇐⇒ gcd(a;b) 1)

Lemma: coprime_iff_ndivides
a,p:ℤ.  (prime(p)  (CoPrime(p,a) ⇐⇒ ¬(p a)))

Lemma: coprime_bezout_id0
a,b:ℤ.  (CoPrime(a,b)  (∃x,y:ℤ(((a x) (b y)) 1)))

Lemma: coprime_bezout_id1
a,b:ℤ.  (CoPrime(a,b)  (∃x,y:ℤ(((a x) (b y)) 1 ∈ ℤ)))

Lemma: coprime_bezout_id2
a,b:ℤ.  ((∃x,y:ℤ(((a x) (b y)) 1 ∈ ℤ))  CoPrime(a,b))

Lemma: coprime_bezout_id
a,b:ℤ.  (CoPrime(a,b) ⇐⇒ ∃x,y:ℤ(((a x) (b y)) 1 ∈ ℤ))

Lemma: coprime_prod
a,b1,b2:ℤ.  (CoPrime(a,b1)  CoPrime(a,b2)  CoPrime(a,b1 b2))

Lemma: coprime-exp1
a,b:ℤ.  (CoPrime(a,b)  (∀n:ℕCoPrime(a,b^n)))

Lemma: coprime_divisors_prod
a1,a2,b:ℤ.  (CoPrime(a1,a2)  (a1 b)  (a2 b)  ((a1 a2) b))

Lemma: coprime_divides_prod
a1,a2,b:ℤ.  ((b (a1 a2))  CoPrime(b,a1)  (b a2))

Lemma: atomic_imp_prime
a:ℤprime(a) supposing atomic(a)

Lemma: prime_divs_prod
p:ℤ(prime(p)  (∀a1,a2:ℤ.  ((p (a1 a2))  ((p a1) ∨ (p a2)))))

Lemma: decidable__reducible

Lemma: decidable__prime

Lemma: mul_assoc
[a,b,c:ℤ].  ((a c) ((a b) c) ∈ ℤ)

Definition: eqmod
a ≡ mod ==  (a b)

Lemma: eqmod_wf
[m,a,b:ℤ].  (a ≡ mod m ∈ ℙ)

Lemma: rem-eqmod
a:ℤ. ∀m:ℤ-o.  ((a rem m) ≡ mod m)

Lemma: decidable__eqmod
m,a,b:ℤ.  Dec(a ≡ mod m)

Lemma: sq_stable__eqmod
m,a,b:ℤ.  SqStable(a ≡ mod m)

Lemma: comb_for_eqmod_wf
λm,a,b,z. (a ≡ mod m) ∈ m:ℤ ⟶ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ

Lemma: eqmod_weakening
m,a,b:ℤ.  a ≡ mod supposing b ∈ ℤ

Lemma: eqmod_refl
m,a:ℤ.  (a ≡ mod m)

Lemma: eqmod_transitivity
m,a,b,c:ℤ.  ((a ≡ mod m)  (b ≡ mod m)  (a ≡ mod m))

Lemma: eqmod_inversion
m,a,b:ℤ.  ((a ≡ mod m)  (b ≡ mod m))

Lemma: eqmod-eqmod-div
m,m',a,a',b,b':ℤ.  ((m' m)  (a ≡ a' mod m)  (b ≡ b' mod m)  (a ≡ mod m' ⇐⇒ a' ≡ b' mod m'))

Lemma: eqmod-divides-implies
m,m':ℤ.  ((m' m)  {∀a,b:ℤ.  ((a ≡ mod m)  (a ≡ mod m'))})

Lemma: eqmod_functionality_wrt_eqmod
m,m',a,a',b,b':ℤ.  (a ≡ a' mod m)  (b ≡ b' mod m)  (a ≡ mod ⇐⇒ a' ≡ b' mod m') supposing m' ∈ ℤ

Lemma: eqmod_fun
m,a,a',b,b':ℤ.  ((a ≡ a' mod m)  (b ≡ b' mod m)  (a ≡ mod ⇐⇒ a' ≡ b' mod m))

Lemma: eqmod_equiv_rel
n:ℤEquivRel(ℤ;x,y.x ≡ mod n)

Lemma: eqmod-zero
m:ℤ(m ≡ mod m)

Lemma: add_functionality_wrt_eqmod
m,a,a',b,b':ℤ.  ((a ≡ a' mod m)  (b ≡ b' mod m)  ((a b) ≡ (a' b') mod m))

Lemma: add_reduce_eqmod
m,x,y:ℤ.  ((x y) ≡ mod ⇐⇒ y ≡ mod m)

Lemma: add_eqmod_zero
m,x,y:ℤ.  ((x ≡ mod m)  (y ≡ mod m)  ((x y) ≡ mod m))

Lemma: minus_functionality_wrt_eqmod
m,a,a':ℤ.  ((a ≡ a' mod m)  ((-a) ≡ (-a') mod m))

Lemma: subtract-elim
[x,y:ℤ].  (x (-y))

Lemma: subtract_functionality_wrt_eqmod
m,a,a',b,b':ℤ.  ((a ≡ a' mod m)  (b ≡ b' mod m)  ((a b) ≡ (a' b') mod m))

Lemma: multiply_functionality_wrt_eqmod
m,a,a',b,b':ℤ.  ((a ≡ a' mod m)  (b ≡ b' mod m)  ((a b) ≡ (a' b') mod m))

Lemma: small-eqmod
m:ℕ+. ∀a:ℤ.  ∃b:ℤ(((2 |b|) ≤ m) ∧ (b ≡ mod m))

Lemma: multiply_eqmod_zero_left
m,x,y:ℤ.  ((x ≡ mod m)  ((x y) ≡ mod m))

Lemma: gcd_functionality_wrt_eqmod
a,a',m:ℤ.  ((a' ≡ mod m)  (gcd(a';m) gcd(a;m)))

Lemma: coprime_functionality_wrt_eqmod
a,a',m:ℤ.  ((a' ≡ mod m)  (CoPrime(a',m) ⇐⇒ CoPrime(a,m)))

Lemma: coprime_functionality_wrt_eqmod2
a,a',m:ℤ.  ((a' ≡ mod m)  (CoPrime(m,a') ⇐⇒ CoPrime(m,a)))

Lemma: eqmod_cancellation
m,x,a,b:ℤ.  (CoPrime(x,m)  ((x a) ≡ (x b) mod m)  (a ≡ mod m))

Lemma: product-eq-0-mod-prime
p,a,b:ℤ.  (prime(p)  ((a b) ≡ mod p)  ((a ≡ mod p) ∨ (b ≡ mod p)))

Lemma: modulus-idempotent
x:ℤ. ∀m:ℕ+.  (((x mod m) mod m) (x mod m) ∈ ℤ)

Lemma: modulus-equal
x,y:ℤ. ∀m:ℕ+.  ((x mod m) (y mod m) ∈ ℤ ⇐⇒ (x y))

Lemma: modulus-equal-iff-eqmod
x,y:ℤ. ∀m:ℕ+.  ((x mod m) (y mod m) ∈ ℤ ⇐⇒ x ≡ mod m)

Lemma: mod-eqmod
x:ℤ. ∀m:ℕ+.  ((x mod m) ≡ mod m)

Lemma: modulus_functionality_wrt_eqmod
[m:ℕ+]. ∀[x,y:ℤ].  (x mod m) (y mod m) ∈ ℤ supposing x ≡ mod m

Lemma: add-one-mod-2
[x:ℤ]. (((x 1) mod 2) (1 mod 2) ∈ ℤ)

Lemma: impossible-equation-by-eqmod
[x,z,a:ℤ].  (((27 x) (z z) (3 z) z) (1 (999 a)) ∈ ℤ))

Definition: isOdd
isOdd(n) ==  (n mod =z 1)

Lemma: isOdd_wf
[n:ℤ]. (isOdd(n) ∈ 𝔹)

Definition: isEven
isEven(n) ==  (n mod =z 0)

Lemma: isEven_wf
[n:ℤ]. (isEven(n) ∈ 𝔹)

Lemma: assert-isOdd
n:ℤ(↑isOdd(n) ⇐⇒ ∃k:ℤ(n ((2 k) 1) ∈ ℤ))

Lemma: isOdd-2n+1
n:ℤ(isOdd((2 n) 1) tt)

Lemma: assert-isEven
n:ℤ(↑isEven(n) ⇐⇒ ∃k:ℤ(n (2 k) ∈ ℤ))

Lemma: isEven-2n
n:ℤ(isEven(2 n) tt)

Lemma: rem-zero-implies-minus
x:ℤ. ∀y:ℤ-o.  (((x rem y) 0 ∈ ℤ ((-x rem y) 0 ∈ ℤ))

Lemma: not-even-succ-implies-even
n:ℤ((¬↑isEven(n 1))  (↑isEven(n)))

Lemma: even-succ-implies-not-even
n:ℤ((↑isEven(n 1))  (¬↑isEven(n)))

Lemma: even-implies-two-times
n:ℕ((↑isEven(n))  (∃k:ℕ(n (2 k) ∈ ℤ)))

Lemma: odd-implies-succ-two-times
n:ℕ((↑isOdd(n))  (∃k:ℕ(n ((2 k) 1) ∈ ℤ)))

Lemma: odd-or-even
n:ℤ(↑(isOdd(n) ∨bisEven(n)))

Lemma: odd-implies
n:ℤ((↑isOdd(n))  {((↑isEven(n 1)) ∧ (¬↑isEven(n))) ∧ (↑isEven(n 1))})

Lemma: even-implies
n:ℤ((↑isEven(n))  {((↑isOdd(n 1)) ∧ (¬↑isOdd(n))) ∧ (↑isOdd(n 1))})

Lemma: even-iff-not-odd
[n:ℤ]. uiff(↑isEven(n);¬↑isOdd(n))

Lemma: odd-iff-not-even
[n:ℤ]. uiff(↑isOdd(n);¬↑isEven(n))

Lemma: small-eqmod-odd
m:ℕ+((↑isOdd(m))  (∀a:ℤ. ∃b:ℤ(2 |b| < m ∧ (b ≡ mod m))))

Definition: same-parity
same-parity(n;m) ==  if isEven(n) then isEven(m) else isOdd(m) fi 

Lemma: same-parity_wf
[n,m:ℤ].  (same-parity(n;m) ∈ 𝔹)

Lemma: same-parity-implies
[n,m:ℤ].  ((↑same-parity(n;m))  {(¬↑same-parity(n;m 1)) ∧ (¬↑same-parity(n;m 1))})

Lemma: not-same-parity-implies
[n,m:ℤ].  ((¬↑same-parity(n;m))  {(↑same-parity(n;m 1)) ∧ (↑same-parity(n;m 1))})

Lemma: same-parity-implies-even-odd
n,m:ℤ.  ((↑same-parity(n;m))  (((↑isEven(n)) ∧ (↑isEven(m))) ∨ ((↑isOdd(n)) ∧ (↑isOdd(m)))))

Lemma: not-same-parity-implies-even-odd
n,m:ℤ.  ((¬↑same-parity(n;m))  (((↑isEven(n)) ∧ (↑isOdd(m))) ∨ ((↑isOdd(n)) ∧ (↑isEven(m)))))

Lemma: isOdd-isEven-add
[n,m:ℤ].  (uiff(↑isOdd(n m);¬↑same-parity(n;m)) ∧ uiff(↑isEven(n m);↑same-parity(n;m)))

Lemma: isEven-add
[n,m:ℤ].  uiff(↑isEven(n m);↑same-parity(n;m))

Lemma: isOdd-add
[n,m:ℤ].  uiff(↑isOdd(n m);¬↑same-parity(n;m))

Lemma: odd-plus-even
[n,m:ℤ].  ↑isOdd(n m) supposing (↑isOdd(n)) ∧ (↑isEven(m))

Lemma: odd-plus-odd
[n,m:ℤ].  ↑isEven(n m) supposing (↑isOdd(n)) ∧ (↑isOdd(m))

Lemma: even-plus-odd
[n,m:ℤ].  ↑isOdd(n m) supposing (↑isOdd(m)) ∧ (↑isEven(n))

Lemma: even-plus-even
[n,m:ℤ].  ↑isEven(n m) supposing (↑isEven(m)) ∧ (↑isEven(n))

Lemma: isOdd-sum
[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  uiff(↑isOdd(Σ(f[x] x < n));↑isOdd(||filter(λx.isOdd(f[x]);upto(n))||))

Lemma: isEven-sum
[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  uiff(↑isEven(Σ(f[x] x < n));↑isEven(||filter(λx.isOdd(f[x]);upto(n))||))

Lemma: lsum-of-even
[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)}  ⟶ ℤ].  ↑isEven(Σ(f[x] x ∈ L)) supposing (∀x∈L.↑isEven(f[x]))

Lemma: odd-lsum-of-odd
[T:Type]. ∀[L:T List].
  ∀[f:{x:T| (x ∈ L)}  ⟶ ℤ]. ↑isOdd(Σ(f[x] x ∈ L)) supposing (∀x∈L.↑isOdd(f[x])) supposing ↑isOdd(||L||)

Lemma: odd-l_sum
[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)}  ⟶ ℤ].  uiff(↑isOdd(l_sum(map(f;L)));↑isOdd(||filter(λx.isOdd(f x);L)||))

Lemma: all-even-implies-sum-even
[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  ↑isEven(Σ(f[x] x < n)) supposing ∀x:ℕn. (↑isEven(f[x]))

Comment: chrem_com
Here is the existential half of the chinese remainder theorem for
pairs of integers.

Missing is the proof of uniqueness mod (r s)

Theorems with _a extensions are proved with extraction in mind.

Lemma: chrem_exists_aux
r,s:ℕ+.  (CoPrime(r,s)  (∃x:ℤ((x ≡ mod r) ∧ (x ≡ mod s))))

Lemma: chrem_exists_aux_a
r:ℕ+. ∀s:{s':ℕ+CoPrime(r,s')} .  (∃x:ℤ [((x ≡ mod r) ∧ (x ≡ mod s))])

Lemma: chrem_exists
r,s:ℕ+.  (CoPrime(r,s)  (∀a,b:ℤ.  ∃x:ℤ((x ≡ mod r) ∧ (x ≡ mod s))))

Lemma: chrem_exists_a
r:ℕ+. ∀s:{s':ℕ+CoPrime(r,s')} . ∀a,b:ℤ.  (∃x:ℤ [((x ≡ mod r) ∧ (x ≡ mod s))])

Definition: fib
fib(n) ==  fix((λfib,n. if (n =z 0) ∨b(n =z 1) then else (fib (n 1)) (fib (n 2)) fi )) n

Lemma: fib_wf
[n:ℕ]. (fib(n) ∈ ℕ)

Lemma: comb_for_fib_wf
λn,z. fib(n) ∈ n:ℕ ⟶ (↓True) ⟶ ℕ

Lemma: fib_coprime
n:ℕCoPrime(fib(n),fib(n 1))

Lemma: fib-exists
n:ℕ(∃m:ℕ [(m fib(n) ∈ ℕ)])

Lemma: fast-fib
n:ℕ(∃m:ℕ [(m fib(n) ∈ ℕ)])

Lemma: fast-fib-ext
n:ℕ(∃m:ℕ [(m fib(n) ∈ ℕ)])

Definition: fastfib
fastfib(n) ==  TERMOF{fast-fib-ext:o, 1:l} n

Lemma: less-fast-fib
n:ℕ{m:ℕfib(n) ∈ ℕ

Lemma: less-fast-fib-ext
n:ℕ{m:ℕfib(n) ∈ ℕ

Lemma: assert-pushdownC-test
  ((↑(((a =z c) ∧b c <b) ∧b b((a =z b) ∨b(b =z c)))))
   {(¬(a b ∈ ℤ)) ∧ ((b 2) c ∈ ℤ)) ∧ c < b ∧ (a c ∈ ℤ)})

Definition: slowfib
slowfib(n) ==  TERMOF{less-fast-fib-ext:o, 1:l} n

Definition: genfact
genfact(n;b;m.f[m]) ==
  if (n) < (1)  then b  else eval f[n] in eval b' in eval n' in   genfact(n';b';m.f[m])

Lemma: genfact_wf
[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ].  (genfact(n;b;m.f[m]) ∈ ℤ)

Lemma: genfact-base-linear
[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ].  (genfact(n;b;m.f[m]) (b genfact(n;1;m.f[m])) ∈ ℤ)

Lemma: genfact-step
[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ].  (genfact(n;b;m.f[m]) if n <then else f[n] genfact(n 1;b;m.f[m]) fi  ∈ ℤ)

Lemma: genfact-unbounded
f:ℕ+ ⟶ ℤ. ∀b:ℕ+. ∀N:ℤ.  (∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]) supposing ∀m:ℕ+1 < f[m]

Lemma: genfact-unbounded-ext
f:ℕ+ ⟶ ℤ. ∀b:ℕ+. ∀N:ℤ.  (∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]) supposing ∀m:ℕ+1 < f[m]

Definition: genfact-inv
genfact-inv(N;b;m.f[m]) ==
  eval in
  letrec g(k)=λx.if (x) < (M)  then eval k' in eval f[k'] in eval x' in   k' x'  else in g(0) b

Lemma: genfact-inv_wf
[f:ℕ+ ⟶ ℤ]. ∀[b:ℕ+]. ∀[N:ℤ].  (genfact-inv(N;b;m.f[m]) ∈ {n:ℕN ≤ genfact(n;b;m.f[m])} supposing ∀m:ℕ+1 < f[m]

Lemma: exp-as-genfact
[x:ℤ]. ∀[n:ℕ].  (x^n genfact(n;1;m.x))

Lemma: exp_functionality_wrt_eqmod
m,i,j:ℤ.  ((i ≡ mod m)  (∀n:ℕ(i^n ≡ j^n mod m)))

Lemma: cube-mod-9
n:ℤ((n^3 ≡ mod 9) ∨ (n^3 ≡ mod 9) ∨ (n^3 ≡ (-1) mod 9))

Lemma: three-cubes-mod-9
a,b,c,k:ℤ.  (((a^3 b^3 c^3) k ∈ ℤ ((¬(k ≡ mod 9)) ∧ (k ≡ mod 9))))

Lemma: three-cubes-3-mod-9
a,b,c,k:ℤ.  (((a^3 b^3 c^3) k ∈ ℤ (k ≡ mod 9)  ((a^3 ≡ mod 9) ∧ (b^3 ≡ mod 9) ∧ (c^3 ≡ mod 9)))

Lemma: three-cubes-6-mod-9
  (((a^3 b^3 c^3) k ∈ ℤ (k ≡ mod 9)  ((a^3 ≡ (-1) mod 9) ∧ (b^3 ≡ (-1) mod 9) ∧ (c^3 ≡ (-1) mod 9)))

Lemma: exp-of-mul
[x,y:ℤ]. ∀[n:ℕ].  ((x y)^n (x^n y^n) ∈ ℤ)

Lemma: exp-divides
x,y:ℤ.  ((x y)  (∀n:ℕ(x^n y^n)))

Lemma: exp-one
[n:ℕ]. (1^n 1 ∈ ℤ)

Lemma: exp-zero
[n:ℕ+]. (0^n 0 ∈ ℤ)

Lemma: exp_mul
[i:ℤ]. ∀[n,m:ℕ].  (i^(m n) i^m^n ∈ ℤ)

Lemma: exp_preserves_le
[n,x,y:ℕ].  x^n ≤ y^n supposing x ≤ y

Lemma: exp_preserves_lt
[n:ℕ+]. ∀[x,y:ℕ].  x^n < y^n supposing x < y

Lemma: exp-le-iff
[n:ℕ+]. ∀[x,y:ℕ].  uiff(x ≤ y;x^n ≤ y^n)

Lemma: exp-greater
[x:{2...}]. ∀[n:ℕ].  n < x^n

Lemma: exp-positive
[n,x:ℕ+].  0 < x^n

Lemma: exp-non-neg
[n,x:ℕ].  (0 ≤ x^n)

Lemma: exp-positive-stronger
n:ℕ. ∀x:ℕ+.  0 < x^n

Lemma: exp-is-zero
[x:ℤ]. ∀[n:ℕ].  uiff(x^n 0 ∈ ℤ;0 < n ∧ (x 0 ∈ ℤ))

Lemma: exp-non-zero
[n:ℕ]. ∀[x:ℤ].  ¬(x^n 0 ∈ ℤsupposing ¬(x 0 ∈ ℤ)

Lemma: exp_functionality_wrt_le_1
[b:ℕ+]. ∀[x,y:ℕ].  b^x ≤ b^y supposing x ≤ y

Lemma: divides-prime
p,q:ℤ.  (prime(q)  (p q)  ((p q) ∨ (p 1) ∨ (p 0 ∈ ℤ)))

Lemma: prime-divides-prime
p,q:ℤ.  (prime(p)  prime(q)  (p q)  (p q))

Lemma: prime-power-divides-product
p:ℕ(prime(p)  (∀n:ℕ+. ∀x,y:ℤ.  ((¬(p x))  (p^n (x y))  (p^n y))))

Lemma: prime-isOdd
p:ℕ(prime(p)  (p 2 ∈ ℤ))  (↑isOdd(p)))

Lemma: positive-prime-divides-prime
[p,q:ℕ].  (p q ∈ ℕsupposing ((p q) and prime(q) and prime(p))

Lemma: positive-prime-divides-product
p:{p:ℕprime(p)} . ∀qs:{p:ℕprime(p)}  List.  ((p reduce(λx,y. (x y);1;qs))  (p ∈ qs))

Definition: quadratic-residue
is quadratic residue mod ==  ∃x:ℤ((x x) ≡ mod p)

Lemma: quadratic-residue_wf
[a,p:ℤ].  (a is quadratic residue mod p ∈ ℙ)

Lemma: quadratic-residue_functionality
a,a',p:ℤ.  ((a' ≡ mod p)  (a' is quadratic residue mod ⇐⇒ is quadratic residue mod p))

Lemma: mul_wf_nzero
[a,b:ℤ-o].  (a b ∈ ℤ-o)

Lemma: mul_nzero
[a,b:ℤ-o].  b ≠ 0

Lemma: mul_add_distrib
[a,b,c:ℤ].  (((a b) c) ((a c) (b c)) ∈ ℤ)

Lemma: left_mul_add_distrib
[a,b,c:ℤ].  ((c (a b)) ((c a) (c b)) ∈ ℤ)

Lemma: left_mul_subtract_distrib
[a,b,c:ℤ].  ((c (a b)) ((c a) b) ∈ ℤ)

Lemma: exp_difference_factor
[n:ℕ+]. ∀[x,y:ℤ].  ((x^n y^n) (x^(n 1) y^i i < n) (x y)) ∈ ℤ)

Lemma: absval_exp
[x:ℤ]. ∀[n:ℕ].  (|x^n| |x|^n)

Lemma: exp_difference_bound
[n:ℕ+]. ∀[M:ℕ]. ∀[x,y:ℤ].  |x^n y^n| ≤ ((n M^(n 1)) |x y|) supposing (|x| ≤ M) ∧ (|y| ≤ M)

Definition: sign
sign(x) ==  if 0 ≤then else -1 fi 

Lemma: sign_wf
[x:ℤ]. (sign(x) ∈ ℤ)

Lemma: sign-absval
[x:ℤ]. ((sign(x) |x|) x ∈ ℤ)

Lemma: sign-squared
[x:ℤ]. ((sign(x) sign(x)) 1 ∈ ℤ)

Definition: permutation-sign
The sign of permutation can be defined in various ways.
The crucial properties are 
1)  permutation-sign-id (sign of identity 1)
2)  sign-flip  (sign of transposition -1)
3)  permutation-sign-compose  (sign of g  sign(f)*sign(g))
Properties and make sign character of the group of permutations on
n  (the symmetric group Sn).

The definition used here suffices to prove these properties,
so it is equivalent to any other definition -- e.g parity of the number
of transpositons in decompositon, etc.⋅

permutation-sign(n;f) ==  Π(sign((f j) i) i < j) j < n)

Lemma: permutation-sign_wf
[n:ℕ]. ∀[f:ℕn ⟶ ℕn].  (permutation-sign(n;f) ∈ {s:ℤ|s| 1 ∈ ℤ)

Lemma: permutation-sign-id
[n:ℕ]. (permutation-sign(n;λx.x) 1)

Lemma: permutation-sign-flip-adjacent
[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[u:ℕ1].
  (permutation-sign(n;f (u, 1)) (-permutation-sign(n;f)) ∈ ℤ)

Lemma: permutation-sign-flip
[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[u,v:ℕn].
  permutation-sign(n;f (u, v)) (-permutation-sign(n;f)) ∈ ℤ supposing ¬(u v ∈ ℤ)

Lemma: sign-flip
[n:ℕ]. ∀[u,v:ℕn].  permutation-sign(n;(u, v)) (-1) ∈ ℤ supposing ¬(u v ∈ ℤ)

Lemma: permutation-sign-compose
[n:ℕ]. ∀[f,g:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ].
  (permutation-sign(n;f g) (permutation-sign(n;f) permutation-sign(n;g)) ∈ {s:ℤ|s| 1 ∈ ℤ)

Lemma: sign-inverse
[n:ℕ]. ∀[f:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ].  (permutation-sign(n;inv(f)) permutation-sign(n;f) ∈ {s:ℤ|s| 1 ∈ ℤ)

Lemma: divides-add
x,y,z:ℤ.  ((z x)  (z y)  (z (x y)))

Lemma: divides-mul
x,y,z:ℤ.  (((z x) ∨ (z y))  (z (x y)))

Lemma: gcd-property
x,y:ℤ.  ∃a,b:ℤ(CoPrime(a,b) ∧ (x (gcd(x;y) a) ∈ ℤ) ∧ (y (gcd(x;y) b) ∈ ℤ))

Lemma: gcd-positive
[y,x:ℕ].  (0 < gcd(x;y)) supposing ((0 ≤ y) and 0 < x)

Lemma: gcd-non-neg
[y,x:ℕ].  (0 ≤ gcd(x;y))

Lemma: gcd_sym_nat
a,b:ℕ.  (gcd(a;b) gcd(b;a))

Lemma: gcd_assoc_nat
a,b,c:ℕ.  (gcd(gcd(a;b);c) gcd(a;gcd(b;c)))

Lemma: gcd_subtract
a,b:ℕ.  gcd(a b;b) gcd(a;b) supposing b ≤ a

Lemma: gcd-reduce
p,q:ℤ.  ∃g:ℕ. ∃a,b,x,y:ℤ((p (a g) ∈ ℤ) ∧ (q (b g) ∈ ℤ) ∧ (((x a) (y b)) 1 ∈ ℤ))

Lemma: gcd-reduce-ext
p,q:ℤ.  ∃g:ℕ. ∃a,b,x,y:ℤ((p (a g) ∈ ℤ) ∧ (q (b g) ∈ ℤ) ∧ (((x a) (y b)) 1 ∈ ℤ))

Lemma: gcd-reduce-coprime
p,q:ℤ.  ∃x,y:ℤ(((x p) (y q)) 1 ∈ ℤsupposing CoPrime(p,q)

Lemma: gcd-reduce-prime
p,q:ℤ.  ∃x,y:ℤ(((x p) (y q)) 1 ∈ ℤsupposing prime(p) ∧ (p q))

Definition: gcd_reduce
gcd_reduce(p;q) ==  let g,a,b,rest TERMOF{gcd-reduce-ext:o, 1:l} in <g, a, b>  

Lemma: gcd_reduce_wf
[p,q:ℤ].  (gcd_reduce(p;q) ∈ ℕ × ℤ × ℤ)

Lemma: gcd_reduce_property
p,q:ℤ.  let g,a,b gcd_reduce(p;q) in (p (a g) ∈ ℤ) ∧ (q (b g) ∈ ℤ) ∧ CoPrime(a,b) ∧ ((p b) (a q) ∈ ℤ)

Lemma: gcd_com
[n,m:ℕ].  (gcd(n;m) gcd(m;n))

Lemma: gcd-non-zero
a,b:ℤ.  ((a ≠ 0 ∨ b ≠ 0)  gcd(a;b) ≠ 0)

Definition: lcm
lcm(a;b) ==
  eval a' in
  eval b' in
    if (a' =z 0) then 0
    if (b' =z 0) then 0
    else eval gcd(a';b') in
         (a' b') ÷ g

Lemma: lcm_wf
[a,b:ℤ].  (lcm(a;b) ∈ ℤ)

Lemma: lcm-positive
[a,b:ℕ+].  0 < lcm(a;b)

Lemma: lcm-property
x,y:ℤ.  ∃a,b:ℤ(CoPrime(a,b) ∧ ((x b) lcm(x;y) ∈ ℤ) ∧ ((y a) lcm(x;y) ∈ ℤ))

Lemma: lcm-is-lcm
n,m:ℕ+.  (((n lcm(n;m)) ∧ (m lcm(n;m))) ∧ (∀v:ℤ((n v)  (m v)  (lcm(n;m) v))))

Lemma: lcm-is-lcm-nat
n,m:ℕ.  (((n lcm(n;m)) ∧ (m lcm(n;m))) ∧ (∀v:ℤ((n v)  (m v)  (lcm(n;m) v))))

Lemma: lcm-unique
n,m,l:ℕ+.  ((((n l) ∧ (m l)) ∧ (∀v:ℤ((n v)  (m v)  (l v))))  (l lcm(n;m) ∈ ℤ))

Lemma: lcm-unique-nat
n,m,l:ℕ.  ((((n l) ∧ (m l)) ∧ (∀v:ℤ((n v)  (m v)  (l v))))  (l lcm(n;m) ∈ ℤ))

Lemma: gcd-unique-nat
n,m,g:ℕ.  ((((g n) ∧ (g m)) ∧ (∀v:ℤ((v n)  (v m)  (v g))))  (g gcd(n;m) ∈ ℤ))

Lemma: lcm_wf_nat
[n,m:ℕ].  (lcm(n;m) ∈ ℕ)

Lemma: lcm-com-nat
n,m:ℕ.  (lcm(n;m) lcm(m;n) ∈ ℤ)

Lemma: lcm-assoc-nat
[n,m,k:ℕ].  (lcm(n;lcm(m;k)) lcm(lcm(n;m);k) ∈ ℤ)

Lemma: lcm-gcd-absorption
[n,m:ℕ].  (lcm(n;gcd(n;m)) n ∈ ℤ)

Lemma: gcd-lcm-absorption
[n,m:ℕ].  (gcd(n;lcm(n;m)) n ∈ ℤ)

Definition: int_mod
_n ==  x,y:ℤ//(x ≡ mod n)

Lemma: int_mod_wf
[n:ℤ]. (ℤ_n ∈ Type)

Lemma: int-subtype-int_mod
[n:ℤ]. (ℤ ⊆r ℤ_n)

Lemma: modulus_wf_int_mod
[n:ℕ+]. ∀[x:ℤ_n].  (x mod n ∈ ℕn)

Lemma: modulus-int_mod-nonzero
[n:ℕ+]. ∀[x:ℤ_n].  mod n ∈ ℕ+supposing x ≠ 0 ∈ ℤ_n 

Lemma: equal_int_mod_iff_modulus
[n:ℕ+]. ∀[x,y:ℤ_n].  uiff((x mod n) (y mod n) ∈ ℤ;x y ∈ ℤ_n)

Lemma: minus_wf_int_mod
[n:ℤ]. ∀[x:ℤ_n].  (-x ∈ ℤ_n)

Lemma: add_wf_int_mod
[n:ℤ]. ∀[x,y:ℤ_n].  (x y ∈ ℤ_n)

Lemma: add_is_int_counterexample
[n:ℤ]. ∀[x:ℤ_n].  (x (-x) ∈ ℤ)

Lemma: add_com_int_mod
[n:ℤ]. ∀[x,y:ℤ_n].  ((x y) (y x) ∈ ℤ_n)

Lemma: add_zero_int_mod
[n:ℤ]. ∀[x:ℤ_n].  ((x 0) x ∈ ℤ_n)

Lemma: add_inverse_int_mod
[n:ℤ]. ∀[x:ℤ_n].  ((x (-x)) 0 ∈ ℤ_n)

Lemma: add_assoc_int_mod
[n:ℤ]. ∀[x,y,z:ℤ_n].  (((x y) z) (x z) ∈ ℤ_n)

Lemma: multiply_wf_int_mod
[n:ℤ]. ∀[x,y:ℤ_n].  (x y ∈ ℤ_n)

Lemma: multiply_com_int_mod
[n:ℤ]. ∀[x,y:ℤ_n].  ((x y) (y x) ∈ ℤ_n)

Lemma: multiply_one_int_mod
[n:ℤ]. ∀[x:ℤ_n].  ((x 1) x ∈ ℤ_n)

Lemma: multiply_assoc_int_mod
[n:ℤ]. ∀[x,y,z:ℤ_n].  (((x y) z) (x z) ∈ ℤ_n)

Lemma: multiply_distrib_int_mod
[n:ℤ]. ∀[a,x,y:ℤ_n].  ((a (x y)) ((a x) (a y)) ∈ ℤ_n)

Lemma: multiply_distrib2_int_mod
[n:ℤ]. ∀[a,x,y:ℤ_n].  (((x y) a) ((x a) (y a)) ∈ ℤ_n)

Lemma: subtype_rel_int_mod
[a,b:ℤ].  ((a b)  (ℤ_b ⊆r ℤ_a))

Lemma: int_mod_union_int_mod
[n,m:ℕ+].  ℤ_n ⋃ ℤ_m ≡ ℤ_gcd(n;m)

Lemma: int_mod_isect_int_mod
[n,m:ℕ+].  ℤ_n ⋂ ℤ_m ≡ ℤ_lcm(n;m)

Lemma: int_mod_2_union_int_mod_3
_2 ⋃ ℤ_3 ≡ ⇃(ℤ)

Lemma: int_mod_2_isect_int_mod_3
_2 ⋂ ℤ_3 ≡ ℤ_6

Lemma: equipollent-int_mod
m:ℕ+. ℤ_m ~ ℕm

Comment: fibs and nats as streams
Here are some examples about the "stream" of fibonacci numbers.
They would be part of the streams theory (part of co-recursion)
except that the definition of the fibonacci numbers is in 

Definition: fibs
fibs() ==  fix((λλx,y. (x y);fibs;s-tl(fibs))))

Lemma: fibs_wf
fibs() ∈ stream(ℕ)

Lemma: nth-fibs
n:ℕ(s-nth(n;fibs()) fib(n) ∈ ℤ)

Lemma: fibs-equal-map
fibs() stream-map(λn.fib(n);nats()) ∈ stream(ℕ)

Definition: better-fibs
better-fibs() ==  stream-map(λp.(fst(p));mk-stream(λp.let a,b in eval in <b, c>;<1, 1>))

Lemma: better-fibs_wf
better-fibs() ∈ stream(ℕ)

Lemma: nth-better-fibs
n:ℕ(s-nth(n;better-fibs()) fib(n) ∈ ℤ)

Lemma: better-fibs-equal-map
better-fibs() stream-map(λn.fib(n);nats()) ∈ stream(ℕ)

Lemma: eqmod-by-orbits
     ∃f:T ⟶ T
      (T ~ ℕn
      ∧ Inj(T;T;f)
      ∧ {x:T| (f x) x ∈ T}  ~ ℕk
      ∧ (∀L:T List. (||L|| 1 ∈ ℤ) ∨ (p ||L||) supposing orbit(T;f;L))))
   (n ≡ mod p))

Lemma: eqmod-prime-order-fixedpoints
   (∃T:Type. ∃f:T ⟶ T. (T ~ ℕn ∧ Inj(T;T;f) ∧ {x:T| (f x) x ∈ T}  ~ ℕk ∧ (∀x:T. ((f^p x) x ∈ T))))
   (n ≡ mod p))

Lemma: fermat-little
p:ℕ(prime(p)  (∀x:ℕ(x^p ≡ mod p)))

Lemma: fermat-little2
p:ℕ(prime(p)  (∀x:ℕx^(p 1) ≡ mod supposing ¬(p x)))

Definition: nondecreasing
nondecreasing(f;k) ==  ∀i:ℕ1. ((f i) ≤ (f (i 1)))

Lemma: nondecreasing_wf
[k:ℕ]. ∀[f:ℕk ⟶ ℤ].  (nondecreasing(f;k) ∈ ℙ)

Lemma: const_nondecreasing
[k:ℕ]. ∀[x:ℤ].  nondecreasing(λi.x;k)

Definition: fadd
fadd(f;g) ==  λi.((f i) (g i))

Lemma: fadd_wf
[n,m,k:ℕ]. ∀[f:ℕn ⟶ ℕm]. ∀[g:ℕn ⟶ ℕ1].  (fadd(f;g) ∈ ℕn ⟶ ℕk)

Lemma: fadd_increasing
[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ].  (increasing(fadd(f;g);n)) supposing (nondecreasing(g;n) and increasing(f;n))

Definition: fshift
fshift(f;x) ==  λi.if (i =z 0) then else (i 1) fi 

Lemma: fshift_wf
[n,k:ℕ]. ∀[f:ℕn ⟶ ℕk]. ∀[x:ℕk].  (fshift(f;x) ∈ ℕ1 ⟶ ℕk)

Lemma: fshift_increasing
[n:ℕ]. ∀[x:ℤ]. ∀[f:ℕn ⟶ ℤ].  (increasing(fshift(f;x);n 1)) supposing (x < and 0 < and increasing(f;n))

Definition: fappend
f[n:=x] ==  λi.if (i =z n) then else fi 

Lemma: fappend_wf
[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm]. ∀[x:ℕm].  (f[n:=x] ∈ ℕ1 ⟶ ℕm)

Lemma: increasing_split
  ∀[P:ℕm ⟶ ℙ]
    ((∀i:ℕm. Dec(P i))
         ∃f:ℕn ⟶ ℕm
          ∃g:ℕk ⟶ ℕm
           ∧ increasing(g;k)
           ∧ (∀i:ℕn. (P (f i)))
           ∧ (∀j:ℕk. (P (g j))))
           ∧ (∀i:ℕm. ((∃j:ℕn. (i (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i (g j) ∈ ℤ)))))))

Lemma: pair_support
[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m,k:ℕn].
  (f[x] x < n) (f[m] f[k]) ∈ ℤsupposing 
     ((∀x:ℕn. ((¬(x m ∈ ℤ))  (x k ∈ ℤ))  (f[x] 0 ∈ ℤ))) and 
     (m k ∈ ℤ)))

Definition: double_sum
sum(f[x; y] x < n; y < m) ==  Σ(f[x; y] y < m) x < n)

Lemma: double_sum_wf
[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm ⟶ ℤ].  (sum(f[x;y] x < n; y < m) ∈ ℤ)

Lemma: pair_support_double_sum
[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm ⟶ ℤ]. ∀[x1,x2:ℕn]. ∀[y1,y2:ℕm].
  (sum(f[x;y] x < n; y < m) (f[x1;y1] f[x2;y2]) ∈ ℤsupposing 
     ((∀x:ℕn. ∀y:ℕm.  ((¬((x x1 ∈ ℤ) ∧ (y y1 ∈ ℤ)))  ((x x2 ∈ ℤ) ∧ (y y2 ∈ ℤ)))  (f[x;y] 0 ∈ ℤ))) and 
     ((¬(x1 x2 ∈ ℤ)) ∨ (y1 y2 ∈ ℤ))))

Lemma: double_sum_difference
[n,m:ℕ]. ∀[f,g:ℕn ⟶ ℕm ⟶ ℤ]. ∀[d:ℤ].
  sum(f[x;y] x < n; y < m) (sum(g[x;y] x < n; y < m) d) ∈ ℤ 
  supposing sum(f[x;y] g[x;y] x < n; y < m) d ∈ ℤ

Lemma: double_sum_functionality
[n,m:ℕ]. ∀[f,g:ℕn ⟶ ℕm ⟶ ℤ].
  sum(f[x;y] x < n; y < m) sum(g[x;y] x < n; y < m) ∈ ℤ supposing ∀x:ℕn. ∀y:ℕm.  (f[x;y] g[x;y] ∈ ℤ)

Lemma: sum_switch
[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[i:ℕ1].  (f[(i, 1) x] x < n) = Σ(f[x] x < n) ∈ ℤ)

Definition: fact
(n)! ==  primrec(n;1;λi,j. ((i 1) j))

Lemma: fact0_redex_lemma
(0)! 1

Lemma: fact_unroll
[n:ℤ]. ((n)! if n <then else (n 1)! fi )

Lemma: fact_unroll_1
[n:ℤ]. (n)! (n 1)! supposing ¬n < 1

Lemma: fact-as-genfact
[n:ℕ]. ((n)! genfact(n;1;m.m))

Lemma: fact_wf
[n:ℕ]. ((n)! ∈ ℕ+)

Lemma: exp-fact-as-genfact
[a,x:ℤ]. ∀[n:ℕ].  (a x^n (n)! genfact(n;a;m.x m))

Lemma: fact_add1
[n:ℕ]. ((n 1)! (n 1) (n)!)

Lemma: fact_add2
[n:ℕ]. ((n 2)! (n 2) (n 1) (n)!)

Lemma: fact-increasing
[m:ℕ]. ∀[n:ℕ+].  (n <  (n)! < (m)!)

Lemma: fact-non-decreasing
[m,n:ℕ].  ((n ≤ m)  ((n)! ≤ (m)!))

Lemma: fact-positive
[m:ℕ]. (1 ≤ (m)!)

Lemma: fact-non-zero
[m:ℕ]. ((m)! 0 ∈ ℤ))

Lemma: fact-greater-exp
k,n:ℕ.  ∃m:ℕk^m < (m)!

Definition: expfact
==r if p ≤then else eval n' in eval p' in eval b' n' in   expfact(n';x;p';b') fi 

Lemma: expfact_wf
[m:ℕ+]. ∀[k:ℕ]. ∀[n:ℕ+].  ∀b:{b:ℕk^b < (b)!} ((m ≤ b)  (expfact(m;k;n k^m;(m)!) ∈ {b:ℕ+(n k^b) ≤ (b)!} \000C))

Lemma: expfact-property
k:ℕ. ∀n:ℕ+.  ∃m:ℕ+((n k^m) ≤ (m)!)

Definition: exp-ratio
==r if p <then else eval n' in eval p' in eval q' in   exp-ratio(a;b;n';p';q') fi 

Lemma: exp-ratio_wf
[a:ℕ]. ∀[b:{a 1...}]. ∀[k:ℕ].
  ∀c:{n:ℕa^n < b^n} . ∀n:ℕ.  ((n ≤ c)  (exp-ratio(a;b;n;k a^n;b^n) ∈ {n:ℕa^n < b^n} ))

Lemma: exp-ratio_wf2
b:{2...}. ∀k:ℕ. ∀M:ℕ+.  (exp-ratio(1;b;0;k;M) ∈ {n:ℕk < b^n} )

Lemma: exp-ratio-property
a:ℕ. ∀b:{a 1...}. ∀k:ℕ.  (exp-ratio(a;b;0;k;1) ∈ {n:ℕa^n < b^n} )

Lemma: exp-ratio-property2
M:ℕ+. ∀b:{2...}. ∀k:ℕ.  (exp-ratio(1;b;0;k;M) ∈ {n:ℕk < b^n} )

Definition: super-fact
(n)!! ==  primrec(n;1;λi,j. ((i 1)! j))

Lemma: super-fact_wf
[n:ℕ]. ((n)!! ∈ ℕ+)

Lemma: super-fact-unroll
[n:ℕ+]. ((n)!! (n)! (n 1)!!)

Lemma: super-fact-int-prod-exp
[k:ℕ]. ((k)!! = Π((k i)^(i 1) i < k) ∈ ℤ)

Lemma: fact-bound
n:ℕ((n)! ≤ n^n)

Comment: xxxxx

No Annotations
n:ℕ((n)! ≤ n^n)

BY ](InductionOnNat THEN Auto)[

1. : ℤ
2. 0 < n
3. (n 1)! ≤ (n 1)^(n 1)
⊢ (n)! ≤ n^n

BY ](RWO "exp_step fact_unroll_1" THEN Auto)[


⊢ (n (n 1)!) ≤ (n n^(n 1))

BY ](InstLemma `exp_preserves_le` [⌜1⌝;⌜1⌝;⌜n⌝]⋅ THEN Auto)[


⊢ (n (n 1)!) ≤ (n n^(n 1))

BY ](RWW "-2 -1" THEN Auto)[

No Annotations
[+]∀n:ℕ((n)! ≤ n^n)

BY ]((InductionOnNat THEN Auto)
       THEN (RWO "exp_step fact_unroll_1" THEN Auto)
       THEN (InstLemma `exp_preserves_le` [⌜1⌝;⌜1⌝;⌜n⌝]⋅ THEN Auto)
       THEN RWW "-2 -1" 0
       THEN Auto)[

Definition: doublefact
doublefact(n) ==  if n <then else doublefact(n 2) fi 

Lemma: doublefact_wf
[n:ℤ]. (doublefact(n) ∈ ℕ+)

Lemma: add-plus-1-div-2-implies-lt
[n,m:ℕ].  n < supposing n < ((n m) 1) ÷ 2

Lemma: exp-minusone
[n:ℕ]. ((-1)^n if (n mod =z 0) then else -1 fi  ∈ ℤ)

Lemma: exp-minusone-2n-add
[n,k:ℕ].  ((-1)^((2 n) k) (-1)^k ∈ ℤ)

Lemma: exp-minus
[n:ℕ]. ∀[x:ℤ].  ((-x)^n if (n mod =z 0) then x^n else -x^n fi  ∈ ℤ)

Lemma: exp-convex
[a,b,c:ℕ]. ∀[n:ℕ+].  |a b| ≤ supposing |a^n b^n| ≤ c^n

Lemma: exp-convex2
[a,b:ℤ]. ∀[c:ℕ]. ∀[n:ℕ+].  |a b| ≤ supposing (|a^n b^n| ≤ c^n) ∧ (0 ≤ ⇐⇒ 0 ≤ b)

Lemma: mul-assoced-one
x,y:ℤ.  (((x y) 1)  (x 1))

Lemma: exp-assoced-one
x:ℤ. ∀n:ℕ+.  ((x^n 1)  (x 1))

Lemma: exp-equal-one
x:ℤ. ∀n:ℕ.  (x^n 1 ∈ ℤ ⇐⇒ (x 1 ∈ ℤ) ∨ (n 0 ∈ ℤ) ∨ ((x (-1) ∈ ℤ) ∧ ((n mod 2) 0 ∈ ℤ)))

Lemma: exp-equal-minusone
[x:ℤ]. ∀[n:ℕ].  uiff(x^n (-1) ∈ ℤ;(x (-1) ∈ ℤ) ∧ ((n mod 2) 1 ∈ ℤ))

Lemma: div_mono1
[i,k:ℕ].  (i ÷ k < i) supposing (1 < and 0 < i)

Lemma: efficient-exp
i:ℤ. ∀n:ℕ.  (∃j:ℤ [(j i^n ∈ ℤ)])

Lemma: less-efficient-exp
i:ℤ. ∀n:ℕ.  (∃j:ℤ [(j i^n ∈ ℤ)])

Lemma: efficient-exp-ext
i:ℤ. ∀n:ℕ.  (∃j:ℤ [(j i^n ∈ ℤ)])

Definition: fastexp
i^n ==  TERMOF{efficient-exp-ext:o, 1:l} n

Lemma: fastexp_wf
[i:ℤ]. ∀[n:ℕ].  (i^n ∈ ℤ)

Lemma: less-efficient-exp-ext
i:ℤ. ∀n:ℕ.  (∃j:ℤ [(j i^n ∈ ℤ)])

Lemma: exp-fastexp
[i:ℤ]. ∀[n:ℕ].  (i^n i^n)

Definition: exp-rem
exp-rem(i;n;m) ==
  fix((λexp-rem,n. if n=1
                   then rem m
                   else if n=0
                        then rem m
                        else eval n' n ÷ in
                             eval exp-rem n' in
                               if rem 2=0 then rem else (i rem m))) 

Lemma: exp-rem_wf
[m:ℕ+]. ∀[i:ℤ]. ∀[n:ℕ].  (exp-rem(i;n;m) ∈ ℤ)

Lemma: rem_mul
[x,y:ℕ]. ∀[m:ℕ+].  ((x rem m) ((x rem m) (y rem m) rem m) ∈ ℤ)

Lemma: rem_mul2
[x,y:ℕ]. ∀[m:ℕ+].  ((x rem m) ((x rem m) rem m) ∈ ℤ)

Lemma: thm_1a
n:ℕ(↑isEven((n n) n))

Lemma: exp-rem-property
[m:ℕ+]. ∀[n,i:ℕ].  (exp-rem(i;n;m) i^n rem m)

Definition: log
log(b;n) ==  genfact-inv(n;1;x.b)

Lemma: log_wf
[b:{i:ℤ1 < i} ]. ∀[x:ℤ].  (log(b;x) ∈ ℕ)

Lemma: log-property
[b:{i:ℤ1 < i} ]. ∀[x:ℤ].  (x ≤ b^log(b;x))

Lemma: coprime_symmetry
a,b:ℤ.  (CoPrime(a,b)  CoPrime(b,a))

Lemma: coprime-mod
n:ℕ+. ∀x:ℤ.  (CoPrime(n,x) ⇐⇒ CoPrime(n,x mod n))

Lemma: coprime-exp
a,b:ℤ.  (CoPrime(a,b)  (∀n,m:ℕ.  CoPrime(a^m,b^n)))

Lemma: gcd-exp
x,y:ℤ. ∀n:ℕ.  (gcd(x^n;y^n) gcd(x;y)^n)

Lemma: divides-iff-gcd
x,y:ℤ.  (x ⇐⇒ gcd(y;x) x ∈ ℤ)

Lemma: divides-iff-gcd-assoced
x,y:ℤ.  (x ⇐⇒ gcd(x;y) x)

Lemma: exp_functionality_wrt_assoced
n:ℕ. ∀x,y:ℤ.  ((x y)  (x^n y^n))

Lemma: exp-divides-exp
x,y:ℤ.  (x ⇐⇒ ∀n:ℕ+(x^n y^n))

Lemma: exp-divides-exp2
x,y:ℤ.  (x ⇐⇒ ∃n:ℕ+(x^n y^n))

Lemma: exp_assoced
n:ℕ+. ∀x,y:ℤ.  (x^n y^n ⇐⇒ y)

Lemma: div_induction
b:{b:ℤ1 < b} . ∀[P:ℤ ⟶ ℙ]. (P[0]  (∀i:ℤ-o(P[i ÷ b]  P[i]))  (∀i:ℤP[i]))

Lemma: div_induction-ext
b:{b:ℤ1 < b} . ∀[P:ℤ ⟶ ℙ]. (P[0]  (∀i:ℤ-o(P[i ÷ b]  P[i]))  (∀i:ℤP[i]))

Lemma: div_nat_induction
b:{b:ℤ1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0]  (∀i:ℕ+(P[i ÷ b]  P[i]))  (∀i:ℕP[i]))

Lemma: div_nat_induction-ext
b:{b:ℤ1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0]  (∀i:ℕ+(P[i ÷ b]  P[i]))  (∀i:ℕP[i]))

Lemma: int-sq-root
x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])

Lemma: int-sqrt-ext
x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])

Lemma: integer-nth-root
n:ℕ+. ∀x:ℕ.  (∃r:ℕ [((r^n ≤ x) ∧ x < (r 1)^n)])

Lemma: integer-nth-root-ext
n:ℕ+. ∀x:ℕ.  (∃r:ℕ [((r^n ≤ x) ∧ x < (r 1)^n)])

Lemma: integer-nth-root2
n:{n:ℕ+(n mod 2) 1 ∈ ℤ. ∀x:{...0}.  (∃r:{...0} [((r 1)^n < x ∧ (x ≤ r^n))])

Definition: iroot
iroot(n;x) ==  TERMOF{integer-nth-root-ext:o, 1:l} x

Lemma: iroot_wf
[n:ℕ+]. ∀[x:ℕ].  (iroot(n;x) ∈ ℕ)

Lemma: iroot-property
[n:ℕ+]. ∀[x:ℕ].  ((iroot(n;x)^n ≤ x) ∧ x < (iroot(n;x) 1)^n)

Definition: is-power
is-power(n;x) ==  eval iroot(n;x) in (r^n =z x)

Lemma: is-power_wf
[n:ℕ+]. ∀[x:ℕ].  (is-power(n;x) ∈ 𝔹)

Lemma: assert-is-power
n:ℕ+. ∀x:ℕ.  (↑is-power(n;x) ⇐⇒ ∃r:ℕ(x r^n ∈ ℤ))

Definition: is_power
is_power(n;z) ==  if (z) < (0)  then (n mod =z 1) ∧b is-power(n;-z)  else is-power(n;z)

Lemma: is_power_wf
[n:ℕ+]. ∀[x:ℤ].  (is_power(n;x) ∈ 𝔹)

Lemma: assert-is_power
n:ℕ+. ∀x:ℤ.  (↑is_power(n;x) ⇐⇒ ∃r:ℤ(x r^n ∈ ℤ))

Lemma: iroot-zero
[n:ℕ+]. (iroot(n;0) 0)

Lemma: iroot-positive
[n,x:ℕ+].  (1 ≤ iroot(n;x))

Definition: general-iroot
general-iroot(n;x) ==
  eval in
  eval in
    if (y) < (0)  then if mod 2=1 then TERMOF{integer-nth-root2:o, 1:l} else 0  else iroot(m;y)

Lemma: general-iroot_wf
[n:ℕ+]. ∀[x:ℤ].  (general-iroot(n;x) ∈ ℤ)

Lemma: general-iroot-property
[n:ℕ+]. ∀[x:ℤ].
  (((0 ≤ x)  ((general-iroot(n;x)^n ≤ x) ∧ x < (general-iroot(n;x) 1)^n))
  ∧ ((x < 0 ∧ ((n mod 2) 1 ∈ ℤ))  ((x ≤ general-iroot(n;x)^n) ∧ (general-iroot(n;x) 1)^n < x))
  ∧ ((x < 0 ∧ ((n mod 2) 0 ∈ ℤ))  (general-iroot(n;x) 0 ∈ ℤ)))

Lemma: isqrrrt
n:ℕ(∃r:ℕ [(((r r) ≤ n) ∧ n < (r 1) (r 1))])

Lemma: isqrrrt-program
n:ℕ(∃r:ℕ [(((r r) ≤ n) ∧ n < (r 1) (r 1))])

Lemma: integer-sqrt
x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])

Lemma: integer-sqrt-xover
x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])

Lemma: integer-sqrt-bin-search
x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])

Definition: isqrt_newton
==r eval (n ÷ x) in
    eval s ÷ in
      if z=x then else if (x) < (z)  then x  else isqrt_newton(n;z)

Lemma: isqrt_newton_wf
n,x:ℕ+.  isqrt_newton(n;x) ∈ ∃r:ℕ [(((r r) ≤ n) ∧ n < (r 1) (r 1))] supposing n < (x 1) (x 1)

Lemma: integer-sqrt-newton
x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])

Lemma: integer-sqrt-newton-ext
x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])

Definition: isqrtn
isqrtn(x) ==  TERMOF{integer-sqrt-newton-ext:o, 1:l} x

Lemma: isqrtn_wf
x:ℕ(isqrtn(x) ∈ {r:ℕ((r r) ≤ x) ∧ x < (r 1) (r 1)} )

Lemma: integer-sqrt-ext
x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])

Definition: isqrt
isqrt(x) ==  TERMOF{integer-sqrt-ext:o, 1:l} x

Lemma: isqrt_wf
[x:ℕ]. (isqrt(x) ∈ ℕ)

Lemma: isqrt-property
[x:ℕ]. (((isqrt(x) isqrt(x)) ≤ x) ∧ x < (isqrt(x) 1) (isqrt(x) 1))

Lemma: isqrt-non-decreasing
[x,y:ℕ].  isqrt(x) ≤ isqrt(y) supposing x ≤ y

Lemma: square-iff-isqrt
x:ℕ(∃y:ℕ((y y) x ∈ ℤ⇐⇒ (isqrt(x) isqrt(x)) x ∈ ℤ)

Lemma: isqrt-of-square
[z:ℕ]. (isqrt(z z) z ∈ ℤ)

Lemma: two-squares-iff
  (∃y,z:ℕ(((y y) (z z)) x ∈ ℤ)
  ⇐⇒ ∃y:ℕisqrt(x) 1. ((isqrt(x y) isqrt(x y)) (x y) ∈ ℤ))

Lemma: isqrt-convex
a,b:ℕ.  (|isqrt(a) isqrt(b)| ≤ isqrt(|a b|))

Lemma: int-between
i,j:ℤ.  ∃k:ℤ((i ≤ k) ∧ k < j) supposing i < j

Definition: triangular-num
t(n) ==  (n (n 1)) ÷ 2

Lemma: triangular-num_wf
[n:ℕ]. (t(n) ∈ ℕ)

Lemma: triangular-num-alt
[n:ℕ]. (t(n) (((n ÷ 2) (n rem 2)) ((2 (n ÷ 2)) 1)) ∈ ℤ)

Lemma: triangular-num-add1
[n:ℕ]. (t(n 1) (t(n) 1) ∈ ℤ)

Lemma: triangular-num-le
[n,m:ℕ].  t(n) ≤ t(m) supposing n ≤ m

Lemma: twice-triangular
[n:ℕ]. ((2 t(n)) ((n n) n) ∈ ℤ)

Definition: tsqrt
tsqrt(n) ==  eval isqrt(2 n) in if (r r) r ≤then else fi 

Lemma: tsqrt_wf
[n:ℕ]. (tsqrt(n) ∈ ℕ)

Lemma: tsqrt-property
[n:ℕ]. ((t(tsqrt(n)) ≤ n) ∧ n < t(tsqrt(n) 1))

Lemma: tsqrt-unique
[n,x:ℕ].  (((t(x) ≤ n) ∧ n < t(x 1))  (x tsqrt(n) ∈ ℤ))

Definition: coded-pair
coded-pair(m) ==  eval in eval tsqrt(n) in eval t(x) in eval in   <a, b>

Lemma: coded-pair_wf
[n:ℕ]. (coded-pair(n) ∈ ℕ × ℕ)

Definition: code-pair
code-pair(a;b) ==  t(a b) a

Lemma: code-pair_wf
[a,b:ℕ].  (code-pair(a;b) ∈ ℕ)

Lemma: coded-code-pair
[a,b:ℕ].  (coded-pair(code-pair(a;b)) = <a, b> ∈ (ℕ × ℕ))

Lemma: code-coded-pair
n:ℕ(let a,b coded-pair(n) in code-pair(a;b) n ∈ ℤ)

Lemma: code-pair-bijection
Bij(ℕ;ℕ × ℕx.coded-pair(x))

Definition: code-seq1
code-seq1(k;s) ==  primrec(k;0;λi,x. if (i =z 0) then else code-pair(x;s i) fi )

Lemma: code-seq1_wf
[k:ℕ]. ∀[s:ℕk ⟶ ℕ].  (code-seq1(k;s) ∈ ℕ)

Definition: coded-seq1
==r if (k =z 0) then else let y,m coded-pair(x) in if (n =z k) then else coded-seq1(k 1;y;n) fi  fi 

Lemma: coded-seq1_wf
[k:ℕ]. ∀[n:ℕ1]. ∀[x:ℕ].  (coded-seq1(k;x;n) ∈ ℕ)

Lemma: coded-code-seq1
[k:ℕ+]. ∀s:ℕk ⟶ ℕ. ∀[n:ℕk]. (coded-seq1(k 1;code-seq1(k;s);n) (s n) ∈ ℤ)

Lemma: code-coded-seq1
[k:ℕ+]. ∀[x:ℕ].  (code-seq1(k;λn.coded-seq1(k 1;x;n)) x ∈ ℤ)

Definition: code-seq
code-seq(k;s) ==  if (k =z 0) then else code-pair(k 1;code-seq1(k;s)) fi 

Lemma: code-seq_wf
[k:ℕ]. ∀[s:ℕk ⟶ ℕ].  (code-seq(k;s) ∈ ℕ)

Definition: coded-seq
coded-seq(x) ==  if (x =z 0) then <0, λx.x> else let a,b coded-pair(x 1) in <1, λn.coded-seq1(a;b;n)> fi 

Lemma: coded-seq_wf
x:ℕ(coded-seq(x) ∈ k:ℕ × (ℕk ⟶ ℕ))

Lemma: code-coded-seq
x:ℕ(let k,s coded-seq(x) in code-seq(k;s) x ∈ ℤ)

Lemma: coded-code-seq
k:ℕ. ∀s:ℕk ⟶ ℕ.  (coded-seq(code-seq(k;s)) = <k, s> ∈ (k:ℕ × (ℕk ⟶ ℕ)))

Lemma: code-seq-bijection
Bij(ℕ;k:ℕ × (ℕk ⟶ ℕ);λx.coded-seq(x))

Lemma: countable-nsub-family
B:ℕ ⟶ ℕ+. ∃g:ℕ ⟶ (i:ℕ × ℕB[i]). Surj(ℕ;i:ℕ × ℕB[i];g)

Definition: twosquareinv
This function defines an involution on the type
x:ℕ × y:ℕ × {z:ℕ((x x) (4 z)) p ∈ ℤwhere is prime.

It is used in 
"A One-Sentence Proof that Every Prime == (mod 4) Is Sum of Two Squares"
by D. Zaiger.

He says that it is simplification of an argument by Heath-Brown.⋅

twosquareinv(t) ==
  let x,y,z in 
  if x <then <z, z, x>
  if x <then <(y y) x, y, (x y) z>
  else <y, (x y) z, y>

Lemma: twosquareinv_wf
[p:{2...}]. ∀[t:x:ℕ × y:ℕ × {z:ℕ((x x) (4 z)) p ∈ ℤ].
  (twosquareinv(t) ∈ x:ℕ × y:ℕ × {z:ℕ((x x) (4 z)) p ∈ ℤ)

Lemma: twosquareinv-involution
p:{p:{2...}| prime(p)} . ∀t:x:ℕ × y:ℕ × {z:ℕ((x x) (4 z)) p ∈ ℤ.  (twosquareinv(twosquareinv(t)) t)

Lemma: twosquareinv-fixpoint
p:{p:{2...}| prime(p)} . ∀t:x:ℕ × y:ℕ × {z:ℕ((x x) (4 z)) p ∈ ℤ.
  ((twosquareinv(t) t ∈ (ℕ × ℕ × ℕ))  (t ~ <1, 1, (p 1) ÷ 4>))

Lemma: twosquare-type-finite
p:{p:{2...}| prime(p)} finite(x:ℕ × y:ℕ × {z:ℕ((x x) (4 z)) p ∈ ℤ)

Lemma: prime-sum-of-two-squares-if-one-mod-four
This proof that every prime that is mod is the sum of two squares
comes from the article by D. Zagier called
"A One-Sentence Proof that Every Prime == (mod 4) Is Sum of Two Squares".

It uses the properties 
twosquareinv-involution and
that certain involution has unique fixed point to deduce
that the given finite set (see twosquare-type-finite)
has odd cardinality
 (see involution-with-unique-fixpoint,
so every invoulution has fixed point (see involution-has-fixpoint),
and this proves the theorem.

p:{p:{2...}| prime(p)} ((∃k:ℤ(p (1 (4 k)) ∈ ℤ))  (∃a,b:ℤ(p ((a a) (b b)) ∈ ℤ)))

Lemma: prime-sum-of-two-squares-iff-one-mod-four
p:{p:{2...}| prime(p)} ((p 2 ∈ ℤ) ∨ (∃k:ℤ(p (1 (4 k)) ∈ ℤ)) ⇐⇒ ∃a,b:ℤ(p ((a a) (b b)) ∈ ℤ))

Lemma: three-cubes-lemma
  (∃a,b:ℤ((((a a) ((b b) b)) e ∈ ℤ) ∧ ((a b) d ∈ ℤ))
  ⇐⇒ ∃n:ℕ(((4 e) d) (3 n) ∈ ℤ))

Lemma: sum-of-three-cubes-iff-1
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on super-computer in Bristol.

The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅

k:ℕ. ∀a,b,c:ℤ.
  ((0 ≤ (a b))
   ((((a a) (b b)) (c c)) k ∈ ℤ
     ⇐⇒ ∃d:ℕ
          (((a b) d ∈ ℤ)
          ∧ (((d 0 ∈ ℤ) ∧ ((c c) k ∈ ℤ))
            ∨ ((¬(d 0 ∈ ℤ))
              ∧ ((k rem d) 0 ∈ ℤ)
              ∧ (((a a) ((b b) b)) ((k c) ÷ d) ∈ ℤ))))))

Lemma: sum-of-three-cubes-iff-2
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on super-computer in Bristol.

The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅

  (∃a,b,c:ℤ(((a a) (b b) (c c)) k ∈ ℤ)
  ⇐⇒ ∃c:ℤ
       (((c c) k ∈ ℤ)
       ∨ (∃d:ℕ
           ((¬(d 0 ∈ ℤ))
           ∧ ((k rem d) 0 ∈ ℤ)
           ∧ (∃n:ℕ(((4 ((k c) ÷ d)) d) (3 n) ∈ ℤ))))))

Lemma: sum-of-three-cubes-iff-3
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on super-computer in Bristol.

The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅

  (∃a,b,c:ℤ(((a a) (b b) (c c)) k ∈ ℤ)
  ⇐⇒ ∃d:ℕ. ∃e:ℤ((∃c:ℤ(((d e) k) (c c) ∈ ℤ)) ∧ (∃n:ℕ(((4 e) d) (3 n) ∈ ℤ))))

Lemma: sum-of-three-cubes-iff-4
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on super-computer in Bristol.

The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅

  (∃a,b,c:ℤ(((a a) (b b) (c c)) k ∈ ℤ)
  ⇐⇒ ∃d,n:ℕ
       ((((d d) (3 n) rem 4) 0 ∈ ℤ)
       ∧ (∃c:ℤ(((d (((d d) (3 n)) ÷ 4)) k) (c c) ∈ ℤ))))

Lemma: sum-of-three-cubes-iff
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on super-computer in Bristol.

The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅

  (∃a,b,c:ℤ(((a a) (b b) (c c)) k ∈ ℤ)
  ⇐⇒ ∃d,n:ℕ
       ((↑is_power(3;((2 d) ((d d) (3 n))) k))
       ∨ (↑is_power(3;(((2 d) 1) (((d (d 1)) (3 (n 1))) 1)) k))))

Lemma: 33-is-sum-of-three-cubes
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on super-computer in Bristol.

The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅

a,b,c:ℤ(((a a) (b b) (c c)) 33 ∈ ℤ)

Lemma: 33-is-sum-of-three-cubes-implies
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on super-computer in Bristol.

The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅

 ((∃c:ℤ((((2 d) ((d d) (3 n))) 33) (c c) ∈ ℤ))
 ∨ (∃c:ℤ(((((2 d) 1) (((d (d 1)) (3 (n 1))) 1)) 33) (c c) ∈ ℤ)))

Lemma: 2-is-sum-of-three-cubes
According to wikipedia, as of 2018 these are the only
known ways of writing as the sum of three cubes .⋅

   let (6 x) in
    let in
    let -(6 x) in
    ((a a) (b b) (c c)) 2 ∈ ℤ)
∧ let 1214928 in
   let 3480205 in
   let -3528875 in
   ((a a) (b b) (c c)) 2 ∈ ℤ

Lemma: olympiad-problem-six
k:ℤ. ∀a,b:ℕ.  ((((a a) (b b)) (k ((a b) 1)) ∈ ℤ (∃n:ℤ(k (n n) ∈ ℤ)))

Lemma: Vieta-jumping-example2
k:ℤ. ∀a,b:ℕ.  (((((a a) (b b)) 1) (k b) ∈ ℤ (k 3 ∈ ℤ))

Definition: vexample
vexample(n;a;b) ==  if n=0 then <a, b> else eval b' (3 b) in eval in   vexample(m;b;b')

Lemma: vexample_wf
n,a:ℕ. ∀b:{b:ℕ(((a a) (b b)) 1) ((a b) 3) ∈ ℤ.
  (vexample(n;a;b) ∈ a:ℕ × {b:ℕ(((a a) (b b)) 1) ((a b) 3) ∈ ℤ)

Lemma: Vieta-jumping-example2-corollary
k:ℤ. ∀a,b:ℕ.  (((((a a) (b b)) 1) (k b) ∈ ℤ (a ≤ b)  (∃n:ℕ(<a, b> vexample(n;1;1) ∈ (ℤ × ℤ)))\000C)

Lemma: ab-divides-a^2+b^2+1
  ((a b) (((a a) (b b)) 1)
  ⇐⇒ ∃n:ℕ((<|a|, |b|> vexample(n;1;1) ∈ (ℤ × ℤ)) ∨ (<|b|, |a|> vexample(n;1;1) ∈ (ℤ × ℤ))))

Definition: search
search(k;P) ==  primrec(k;0;λi,j. if 0 <then if then else fi )

Lemma: search_wf
[k:ℕ]. ∀[P:ℕk ⟶ 𝔹].  (search(k;P) ∈ ℕ1)

Lemma: search_property
k:ℕ. ∀P:ℕk ⟶ 𝔹.
  ((∃i:ℕk. (↑(P i)) ⇐⇒ 0 < search(k;P))
  ∧ (↑(P (search(k;P) 1))) ∧ (∀j:ℕk. ¬↑(P j) supposing j < search(k;P) 1) supposing 0 < search(k;P))

Lemma: search_succ
[k:ℕ]. ∀[P:ℕ1 ⟶ 𝔹].
  (search(k 1;P) if then if 0 <search(k;λi.(P (i 1))) then search(k;λi.(P (i 1))) else fi  ∈ ℤ)

Comment: parametricity (theorems for free)
Parametricity or "theorems for free" allows one to deduce
certain facts about functions with polymorphic type.

Those polymorphic types are often expressed in type system
with impredicative quantification over all types.
But we can often get the same results using predicative quantification
over the types in universe.

So, for example, instead of the  type  
  (FORALL alpha. alpha-> alpha)  in an impredicative system,
we can consider the type ⌜⋂A:Type. (A ⟶ A)⌝.
Since the universe ⌜Type⌝ (note that it is just our display for Universe{i})
contains "enough" types, in particular singleton types and types that
contain bottom, we can get many of the results of parametricity theory.

For example:

The only functions of type alpha->alpha->alpha
are  \x y. x  and \x y. y, see polymorphic-choice.

The only functions of type alpha->List(alpha) are
  \x. repn(n,x)   see polymorphic-list

Lemma: polymorphic-id-unique
f,g:⋂T:Type. (T ⟶ T).  (f g ∈ (⋂T:Type. (T ⟶ T)))

Lemma: polymorphic-id-unique-sq
f:⋂T:Type. (T ⟶ T). (f ~ λx.x)

Lemma: polymorphic-constant-base
[T:Type]. ∀f:Base ⟶ T. ∃t:T. ∀x:Base. ((f x) t ∈ T) supposing mono(T) ∧ value-type(T)

Lemma: polymorphic-constant
[T:Type]. ∀f:⋂A:Type. (A ⟶ T). ∃t:T. ∀A:Type. ∀x:A.  ((f x) t ∈ T) supposing mono(T) ∧ value-type(T)

Lemma: polymorphic-constant-bool
f:⋂A:Type. (A ⟶ 𝔹). ∃t:𝔹. ∀A:Type. ∀x:A.  t

Lemma: polymorphic-constant-nat
f:⋂A:Type. (A ⟶ ℕ). ∃n:ℕ. ∀A:Type. ∀x:A.  ((f x) n ∈ ℕ)

Lemma: polymorphic-list
f:⋂A:Type. (A ⟶ (A List)). ∃n:ℕ(f x.repn(n;x)) ∈ (⋂A:Type. (A ⟶ (A List))))

Lemma: type-equating-some
T:Type. ∀P:T ⟶ ℙ.
   ((T ⊆T') ∧ (∀x,y:T.  (P[x]  P[y]  (x y ∈ T'))) ∧ (∀x,y:T.  ((¬P[x])  (x y ∈ ⇐⇒ y ∈ T'))))

Lemma: exists-type-equating-ints
  ((¬(x y ∈ ℤ))
   (n m ∈ ℤ))
   (x m ∈ ℤ))
   (y n ∈ ℤ))
   (∃T:Type. ((x n ∈ T) ∧ (y m ∈ T) ∧ (x y ∈ T)))))

Definition: EquatePairs
EquatePairs(x;n;y;m) ==
  pertype(λ2b.(a b ∈ Base)
  ∨ (((x a ∈ Base) ∧ (n b ∈ Base)) ∨ ((x b ∈ Base) ∧ (n a ∈ Base)))
  ∨ (((y a ∈ Base) ∧ (m b ∈ Base)) ∨ ((y b ∈ Base) ∧ (m a ∈ Base)))
  ∨ ((x y ∈ Base) ∧ (((n a ∈ Base) ∧ (m b ∈ Base)) ∨ ((n b ∈ Base) ∧ (m a ∈ Base)))))

Lemma: EquatePairs_wf
  (EquatePairs(x;n;y;m) ∈ Type) supposing ((¬(n m ∈ Base)) and (x m ∈ Base)) and (y n ∈ Base)))

Lemma: EquatePairs-equality
     (a b ∈ EquatePairs(x;n;y;m)
     ⇐⇒ ↓(a b ∈ Base)
          ∨ (((x a ∈ Base) ∧ (n b ∈ Base)) ∨ ((x b ∈ Base) ∧ (n a ∈ Base)))
          ∨ (((y a ∈ Base) ∧ (m b ∈ Base)) ∨ ((y b ∈ Base) ∧ (m a ∈ Base)))
          ∨ ((x y ∈ Base) ∧ (((n a ∈ Base) ∧ (m b ∈ Base)) ∨ ((n b ∈ Base) ∧ (m a ∈ Base)))))) supposing 
     ((¬(n m ∈ Base)) and 
     (x m ∈ Base)) and 
     (y n ∈ Base)))

Lemma: type-separation
  (((x)↓ ∨ is-exception(x))
   ((y)↓ ∨ is-exception(y))
   (∀n,m:ℤ. ∀T:Type.  ((x n ∈ T)  (y m ∈ T)  (x y ∈ T)))
   (x y ∈ Base))

Lemma: polymorphic-choice-int
f:⋂A:Type. (A ⟶ A ⟶ A). ((∀x,y:ℤ.  ((f y) x ∈ ℤ)) ∨ (∀x,y:ℤ.  ((f y) y ∈ ℤ)))

Lemma: type-with-x=0-y=1
x,y:Base.  ∃T:Type. ((x 0 ∈ T) ∧ (y 1 ∈ T) ∧ ((0 1 ∈ T)  (↓(x y ∈ Base) ∨ (x 1 ∈ Base) ∨ (y 0 ∈ Base))))

Lemma: type-with-y=n
n,m:ℤ.  ((¬(n m ∈ ℤ))  (∀y:Base. ∃T:Type. ((y n ∈ T) ∧ (m m ∈ T) ∧ ((n m ∈ T)  (y m ∈ Base)))))

Lemma: polymorphic-choice-base
f:⋂A:Type. (A ⟶ A ⟶ A). ((∀x,y:Base.  ((f y) x ∈ Base)) ∨ (∀x,y:Base.  ((f y) y ∈ Base)))

Lemma: polymorphic-choice
f:⋂A:Type. (A ⟶ A ⟶ A). ((f x,y. x) ∈ (⋂A:Type. (A ⟶ A ⟶ A))) ∨ (f x,y. y) ∈ (⋂A:Type. (A ⟶ A ⟶ A))))

Lemma: poly-choice-eta-1
f:Base. ((∀x,y:Base.  ((f y) y ∈ Base))  (f ~ λx,y. y))

Lemma: not-poly-choice-eta-2
¬(∀f:Base. ((∀x,y:Base.  ((f y) x ∈ Base))  (f ~ λx,y. (f y))))

Lemma: not-poly-choice-eta-2'
¬(∀f:Base. ((∀x,y:Base.  ((f y) x ∈ Base))  (f ~ λx,y. x)))

Lemma: poly-choice-eta-2
f:Base. ((∀x,y:Base.  ((f y) x ∈ Base))  (f ~ λx.if is lambda then λy.x otherwise ⊥))

Lemma: polymorphic-choice-base-sq
f:Base. ((f ∈ ⋂A:Type. (A ⟶ A ⟶ A))  ((f ~ λx.if is lambda then λy.x otherwise ⊥) ∨ (f ~ λx,y. y)))

Lemma: polymorphic-choice-sq
f:⋂A:Type. (A ⟶ A ⟶ A). ((f ~ λx.if is lambda then λy.x otherwise ⊥) ∨ (f ~ λx,y. y))

Lemma: base-is-base-list
[T:Type]. ∀[x:Base].  ((x ∈ List)  (x ∈ Base List))

Definition: testxx
testxx(x;y)==r if (x =z 0) then else testxx(x 1;y) fi 

Home Index