Theory number

⊢ ∀n. Euler n = {i | 0 < i ∧ i < n ∧ coprime n i}

⊢ ∀n x.
    1 < n ∧ 0 < x ∧ x < n ∧ coprime n x ⇒
    0 < GCD_MOD_MUL_INV n x ∧ GCD_MOD_MUL_INV n x < n ∧
    coprime n (GCD_MOD_MUL_INV n x) ∧ GCD_MOD_MUL_INV n x * x MOD n = 1

⊢ ∀p x.
    prime p ∧ 0 < x ∧ x < p ⇒
    0 < MOD_MULT_INV p x ∧ MOD_MULT_INV p x < p ∧
    MOD_MULT_INV p x * x MOD p = 1

⊢ ∀x y f. (x == y) f ⇔ f x = f y

⊢ ∀f s y. preimage f s y = {x | x ∈ s ∧ f x = y}

⊢ ∀n. residue n = {i | 0 < i ∧ i < n}

⊢ ∀n. totient n = CARD (Euler n)

⊢ ∀m n. 0 < m ∧ 0 < n ∧ m + n = 2 ⇒ m = 1 ∧ n = 1

⊢ ∀a b c. c ≤ a ⇒ a + b − (a − c) = c + b

⊢ ∀m n.
    0 < m ∧ 1 < n ∧ (∀p. prime p ∧ p divides m ⇒ p MOD n = 1) ⇒ m MOD n = 1

⊢ ∀b c d. b ∧ (c ⇒ d) ⇒ (b ⇒ c) ⇒ d

⊢ ∀p q. p ∧ q ⇒ p ∨ ¬q

⊢ ∀s. BIGUNION (IMAGE (λx. {x}) s) = s

⊢ ∀f s t. BIJ f s t ⇒ ∀x. x ∈ t ⇒ LINV f s x ∈ s

⊢ ∀f s t.
    BIJ f s t ⇒
    (∀x. x ∈ s ⇒ LINV f s (f x) = x) ∧ ∀x. x ∈ t ⇒ f (LINV f s x) = x

⊢ ∀f s t. BIJ f s t ∧ (∀y. y ∈ t ⇒ RINV f s y ∈ s) ⇒ BIJ (RINV f s) t s

⊢ ∀f s t.
    BIJ f s t ∧ (∀y. y ∈ t ⇒ RINV f s y ∈ s) ⇒
    ∀x. x ∈ s ⇒ RINV f s (f x) = x

⊢ ∀b1 b2 f. (b1 ⇔ b2) ⇒ f b1 = f b2

⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
      CARD (BIGUNION P) = ∑ CARD P

⊢ ∀s. FINITE s ⇒ (CARD s = 1 ⇔ SING s)

⊢ ∀s. FINITE s ⇒ CARD (PPOW s) = PRE (2 ** CARD s)

⊢ ∀s. FINITE s ⇒ CARD (PPOW s) = tops 2 (CARD s)

⊢ ∀a b c.
    FINITE a ∧ FINITE b ∧ FINITE c ∧ DISJOINT a b ∧ DISJOINT b c ∧
    DISJOINT a c ⇒
    CARD (a ∪ b ∪ c) = CARD a + CARD b + CARD c

⊢ ∀a b c.
    FINITE a ∧ FINITE b ∧ FINITE c ⇒
    CARD (a ∪ b ∪ c) =
    CARD a + CARD b + CARD c + CARD (a ∩ b ∩ c) − CARD (a ∩ b) −
    CARD (b ∩ c) − CARD (a ∩ c)

⊢ count 0 = ∅

⊢ count 1 = {0}

⊢ ∀n. n ∉ count n

⊢ ∀m n. m ≤ n ⇒ count m ⊆ count n

⊢ ∀n. upto n = 0 INSERT natural n

⊢ ∀n t. upto n ⊆ t ⇔ count n ⊆ t ∧ n ∈ t

⊢ ∀n t. t DIFF upto n = t DIFF count n DELETE n

⊢ ∀s t x. s DIFF t DELETE x = s DIFF (x INSERT t)

⊢ ∀s t. s DIFF (s DIFF t) = s ∩ t

⊢ ∀s t. DISJOINT (s DIFF t) t ∧ DISJOINT t (s DIFF t)

⊢ ∀s t. DISJOINT s t ⇔ s DIFF t = s

⊢ ∀k. 0 < k ⇒ ∀m n. m divides n ⇔ m * k divides n * k

⊢ ∀m n k. m divides n ⇒ k * m divides k * n

⊢ ∀m n. 0 < n ∧ n divides m ⇒ m DIV n divides m

⊢ ∀m n. 0 < n ∧ n divides m ⇒ m = n * (m DIV n)

⊢ ∀m n. 0 < n ∧ m divides n ⇒ ∀x. x MOD n MOD m = x MOD m

⊢ ∀m n k. k ≠ 0 ⇒ (m divides n ⇔ k * m divides k * n)

⊢ ∀m n. 0 < n ∧ 0 < m ⇒ ∀x. n divides x ⇒ m * x DIV (m * n) = x DIV n

⊢ ∀m n x.
    0 < n ∧ 0 < m ∧ 0 < m DIV n ∧ n divides m ∧ m divides x ∧
    m DIV n divides x ⇒
    x DIV (m DIV n) = n * (x DIV m)

⊢ ∀x y. 0 < x ∧ 0 < y ∧ x < y ⇒ ∀n. 0 < n ∧ n MOD x = 0 ⇒ n DIV y < n DIV x

⊢ ∀m n. 0 < m ∧ 0 < n ∧ n MOD m = 0 ⇒ n DIV SUC m < n DIV m

⊢ ∀m n. 0 < m ⇒ m * (n DIV m) ≤ n ∧ n < m * SUC (n DIV m)

⊢ ∀A B. (A ⇔ B) ⇔ (A ⇒ B) ∧ ((A ⇒ B) ⇒ B ⇒ A)

⊢ ∀a b. EVEN (TWICE a + b) ⇔ EVEN b

⊢ EVEN 0

⊢ EVEN 2

⊢ ∀n. EVEN n ⇒ n = TWICE (HALF n)

⊢ ∀m. EVEN m ∧ m ≠ 0 ⇒ ∀n. EVEN n ⇔ EVEN (n MOD m)

⊢ ∀m. EVEN m ∧ m ≠ 0 ⇒ ∀n. ODD n ⇔ ODD (n MOD m)

⊢ ∀n. 0 < n ⇒ (EVEN n ⇔ ODD (PRE n)) ∧ (ODD n ⇔ EVEN (PRE n))

⊢ ∀n. (EVEN n ⇔ ODD (SUC n)) ∧ (ODD n ⇔ EVEN (SUC n))

⊢ ∀n. EVEN (n * (n + 1))

⊢ ∀n. EVEN n ∧ prime n ⇔ n = 2

⊢ ∀n. EVEN n² ⇔ EVEN n

⊢ ∀n. EVEN n ⇒ HALF (SUC n) = HALF n

⊢ ∀n. n² = 0 ⇔ n = 0

⊢ ∀n. 0 < n ⇒ EVEN (2 ** n)

⊢ ∀n. 0 < n ⇒ HALF (2 ** n) = 2 ** (n − 1)

⊢ ∀n. 0 < n ⇒ ODD (tops 2 n)

⊢ ∀m n.
    m ** n = if n = 0 then 1 else (if EVEN n then 1 else m) * m² ** HALF n

⊢ ∀m n. m ≤ n ⇒ ∀p. p ** n = p ** m * p ** (n − m)

⊢ ∀m n. m < n ⇒ ∀p. p ** n = p ** m * p ** (n − m)

⊢ ∀m n.
    m ** n =
    if n = 0 then 1
    else if EVEN n then SQ m ** HALF n
    else m * SQ m ** HALF n

⊢ ∀m n.
    m ** n =
    if n = 0 then 1 else (if EVEN n then 1 else m) * SQ m ** HALF n

⊢ ∀n. EVEN n ⇒ ∀m. m ** n = SQ m ** HALF n

⊢ ∀b c m n. m ≤ n ∧ 0 < c ⇒ b ** c ** m ≤ b ** c ** n

⊢ ∀a b n. a ≤ b ⇒ a ** n ≤ b ** n

⊢ ∀x y n. x ** y ** SUC n = (x ** y) ** y ** n

⊢ ∀n m. n * m ** (n − 1) + m ** n ≤ (1 + m) ** n

⊢ ∀n m. 1 + n * m ≤ (1 + m) ** n

⊢ ∀n m. 0 < m ∧ 1 < n ⇒ 1 + n * m < (1 + m) ** n

⊢ ∀b n m.
    1 < m ⇒
    b ** n MOD m =
    if n = 0 then 1
    else (if EVEN n then 1 else b) * (SQ b ** HALF n MOD m) MOD m

⊢ ∀b n m.
    1 < m ⇒
    b ** n MOD m =
    if n = 0 then 1
    else
      (let
         result = SQ b ** HALF n MOD m
       in
         if EVEN n then result else b * result MOD m)

⊢ ∀n. ODD n ⇒ ∀m. m ** n = m * SQ m ** HALF n

⊢ ∀m n. 0 < m ⇒ m ** SUC n DIV m = m ** n

⊢ ∀m n.
    m ** n =
    if n = 0 then 1
    else if n = 1 then m
    else if EVEN n then SQ m ** HALF n
    else m * SQ m ** HALF n

⊢ Euler 0 = ∅

⊢ Euler 1 = ∅

⊢ ∀n. totient n ≤ n ∧ (1 < n ⇒ 0 < totient n ∧ totient n < n)

⊢ ∀p. prime p ⇒ totient p = p − 1

⊢ FALLING totient

⊢ ∀n. 1 < n ⇒ totient n < n

⊢ ∀n x. x ∈ Euler n ⇔ 0 < x ∧ x < n ∧ coprime n x

⊢ ∀n. Euler n = ∅ ⇔ n = 0 ∨ n = 1

⊢ ∀n. FINITE (Euler n)

⊢ ∀n. 1 < n ⇒ 1 ∈ Euler n

⊢ ∀n. 1 < n ⇒ Euler n ≠ ∅

⊢ ∀p. prime p ⇒ Euler p = residue p

⊢ ∀n. Euler n = residue n ∩ {j | coprime j n}

⊢ ∀n p.
    0 < n ∧ 1 < p ∧ p divides n ⇒
    ∃m. p ** m divides n ∧ ¬(p divides n DIV p ** m)

⊢ ∀n p.
    0 < n ∧ prime p ∧ p divides n ⇒
    ∃m. 0 < m ∧ p ** m divides n ∧ ∀k. coprime (p ** k) (n DIV p ** m)

⊢ ∀n. FACT n = PROD_SET (natural n)

⊢ ∀n m.
    m < n ⇒ FACT n = PROD_SET (IMAGE SUC (count n DIFF count m)) * FACT m

⊢ ∀P ls j h.
    (let
       fs = FILTER P ls
     in
       ALL_DISTINCT ls ∧ j < h ∧ h < LENGTH fs ⇒
       findi fs❲j❳ ls < findi fs❲h❳ ls)

⊢ ∀s. FINITE s ⇒ ∃f. BIJ f (count (CARD s)) s

⊢ ∀P n. FINITE {P x | x < n}

⊢ ∀f s t. INJ f s t ∧ FINITE s ∧ FINITE t ∧ CARD s = CARD t ⇒ SURJ f s t

⊢ ∀f s t. FINITE s ∧ FINITE t ∧ CARD s = CARD t ∧ INJ f s t ⇒ BIJ f s t

⊢ ∀f s t. FINITE s ∧ FINITE t ∧ CARD s = CARD t ∧ INJ f s t ⇒ SURJ f s t

⊢ ∀s. FINITE s ⇒ FINITE (PPOW s)

⊢ ∀f s t. FINITE s ∧ CARD s = CARD t ∧ SURJ f s t ⇒ INJ f s t

⊢ 5 = SUC 4

⊢ 4 = SUC 3

⊢ ∀m n. FUNPOW SUC n m = m + n

⊢ ∀b m n. 0 < b ⇒ FUNPOW (flip $DIV b) n m = m DIV b ** n

⊢ ∀f s x n. f PERMUTES s ∧ x ∈ s ⇒ FUNPOW (LINV f s) n (FUNPOW f n x) = x

⊢ ∀f g. (∀x. f x ≤ g x) ∧ MONO f ⇒ ∀n x. FUNPOW f n x ≤ FUNPOW g n x

⊢ ∀f m n. FALLING f ∧ m ≤ n ⇒ ∀x. FUNPOW f n x ≤ FUNPOW f m x

⊢ ∀f g. (∀x. f x ≤ g x) ∧ MONO g ⇒ ∀n x. FUNPOW f n x ≤ FUNPOW g n x

⊢ ∀f m n. RISING f ∧ m ≤ n ⇒ ∀x. FUNPOW f m x ≤ FUNPOW f n x

⊢ ∀f s x n. f PERMUTES s ∧ x ∈ s ⇒ FUNPOW f n (FUNPOW (LINV f s) n x) = x

⊢ ∀f s x y n.
    f PERMUTES s ∧ x ∈ s ∧ y ∈ s ⇒
    (x = FUNPOW f n y ⇔ y = FUNPOW (LINV f s) n x)

⊢ ∀f s x m n.
    f PERMUTES s ∧ x ∈ s ∧ m ≤ n ⇒
    FUNPOW (LINV f s) (n − m) x = FUNPOW (LINV f s) n (FUNPOW f m x)

⊢ ∀f s x m n.
    f PERMUTES s ∧ x ∈ s ∧ m ≤ n ⇒
    FUNPOW (LINV f s) (n − m) x = FUNPOW f m (FUNPOW (LINV f s) n x)

⊢ ∀f s x n. f PERMUTES s ∧ x ∈ s ⇒ FUNPOW (LINV f s) n x ∈ s

⊢ ∀f s n. f PERMUTES s ⇒ FUNPOW (LINV f s) n PERMUTES s

⊢ ∀m n k. 0 < n ⇒ FUNPOW (λx. MAX x m) n k = MAX k m

⊢ ∀m n k. 0 < n ⇒ FUNPOW (λx. MIN x m) n k = MIN k m

⊢ ∀f k e.
    0 < k ∧ FUNPOW f k e = e ⇒ ∀n. FUNPOW f n e = FUNPOW f (n MOD k) e

⊢ ∀b m n. FUNPOW ($* b) n m = m * b ** n

⊢ ∀f k e. 0 < k ∧ FUNPOW f k e = e ⇒ ∀n. FUNPOW f (n * k) e = e

⊢ ∀f g n x y.
    FUNPOW (λ(x,y). (f x,g y)) n (x,y) = (FUNPOW f n x,FUNPOW g n y)

⊢ ∀m n. FUNPOW (λn. SQ n) n m = m ** 2 ** n

⊢ ∀m n k. 0 < m ∧ 0 < n ⇒ FUNPOW (λn. SQ n MOD m) n k = k ** 2 ** n MOD m

⊢ ∀m n. FUNPOW PRE n m = m − n

⊢ ∀f s x m n.
    f PERMUTES s ∧ x ∈ s ∧ m ≤ n ⇒
    FUNPOW f (n − m) x = FUNPOW f n (FUNPOW (LINV f s) m x)

⊢ ∀f s x m n.
    f PERMUTES s ∧ x ∈ s ∧ m ≤ n ⇒
    FUNPOW f (n − m) x = FUNPOW (LINV f s) m (FUNPOW f n x)

⊢ ∀f g h n x y z.
    FUNPOW (λ(x,y,z). (f x,g y,h z)) n (x,y,z) =
    (FUNPOW f n x,FUNPOW g n y,FUNPOW h n z)

⊢ ∀f s x n. f PERMUTES s ∧ x ∈ s ⇒ FUNPOW f n x ∈ s

⊢ ∀f s n. f PERMUTES s ⇒ FUNPOW f n PERMUTES s

⊢ ∀n x.
    1 < n ∧ 0 < x ∧ x < n ∧ coprime n x ⇒
    ∃y. 0 < y ∧ y < n ∧ coprime n y ∧ y * x MOD n = 1

⊢ ∀a b k. k * a ≤ b ⇒ gcd a b = gcd a (b − k * a)

⊢ ∀a b k. k * a ≤ b ⇒ gcd b a = gcd a (b − k * a)

⊢ ∀n. 0 < n ⇒ 1 + HALF n ≤ n

⊢ ∀n. 2 < n ⇒ 1 + HALF n < n

⊢ ∀m n. HALF n DIV 2 ** m = n DIV 2 ** SUC m

⊢ ∀n. HALF n = 0 ⇔ n = 0 ∨ n = 1

⊢ ∀n. HALF n = n ⇔ n = 0

⊢ ∀n m. TWICE n < m ⇒ n ≤ HALF m

⊢ ∀n. n * HALF (SQ n)² ≤ HALF (n ** 5)

⊢ ∀n. HALF n ≤ n

⊢ ∀x y. x ≤ y ⇒ HALF x ≤ HALF y

⊢ ∀n. 0 < n ⇒ HALF n < n

⊢ ∀m n. n * HALF m ≤ HALF (n * m)

⊢ ∀m n. EVEN n ⇒ HALF (m * n) = m * HALF n

⊢ ∀n m. TWICE n + 1 < m ⇒ n < HALF m

⊢ ∀n. (HALF n)² ≤ n² DIV 4

⊢ ∀n. HALF (SUC n) ≤ n

⊢ ∀n m. n < HALF (SUC m) ⇒ TWICE n + 1 ≤ m

⊢ ∀n. 0 < n ⇒ HALF (SUC (SUC n)) ≤ n

⊢ ∀n. HALF (TWICE n) = n

⊢ ∀f n. IMAGE f (upto n) = f n INSERT IMAGE f (count n)

⊢ ∀f n. IMAGE f (upto n) = f 0 INSERT IMAGE (f ∘ SUC) (count n)

⊢ ∀s t f.
    s ⊆ t ∧ INJ f t 𝕌(:β) ⇒ IMAGE f (t DIFF s) = IMAGE f t DIFF IMAGE f s

⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇒ ∀s e. e ∈ s ⇔ f e ∈ IMAGE f s

⊢ ∀s. s ≠ ∅ ⇒ ∀e. IMAGE (K e) s = {e}

⊢ ∀f s t. (∀x. x ∈ s ⇒ f x ∈ t) ⇔ IMAGE f s ⊆ t

⊢ ∀f s. INJ f s 𝕌(:β) ∧ FINITE s ⇒ CARD (IMAGE f s) = CARD s

⊢ ∀f s. INJ f s 𝕌(:β) ⇒ BIJ f s (IMAGE f s)

⊢ ∀f s t. INJ f s t ⇒ INJ f s 𝕌(:β)

⊢ ∀s x y. x ≠ y ⇒ (x INSERT s) DELETE y = x INSERT s DELETE y

⊢ ∀x s. x ∉ s ⇒ (x INSERT s) DELETE x = s

⊢ ∀s t x. x ∉ s ∧ x INSERT s ⊆ t ⇒ s ⊆ t DELETE x

⊢ ∀s t. s ∩ (t DIFF s) = ∅ ∧ (t DIFF s) ∩ s = ∅

⊢ ∀s e. e ∈ PPOW s ⇒ e ⊂ s

⊢ ∀b x y. x ∈ (if b then {y} else ∅) ⇒ x = y

⊢ ∀a b c. a * b = c * (a − b) ⇒ lcm a b = lcm a c

⊢ ∀n k. k < HALF n ⇔ k + 1 < n − k

⊢ ∀n. n < SUC n

⊢ ∀a b c d. 0 < c ∧ 0 < d ∧ a * b ≤ c * d ∧ d < b ⇒ a < c

⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ a + c ≤ b + d

⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ a * c ≤ b * d

⊢ ∀m n p. n ≤ p ⇒ m * n ≤ m * p

⊢ ∀n. n ≤ 1 ⇔ n = 0 ∨ n = 1

⊢ ∀m n. n ≤ TWICE m ⇔ n ≠ 0 ⇒ HALF (n − 1) < m

⊢ ∀f s t. INJ f t 𝕌(:β) ∧ s ⊆ t ⇒ ∀x. x ∈ s ⇒ LINV f t (f x) = x

⊢ ∀f s. f PERMUTES s ⇒ LINV f s PERMUTES s

⊢ ∀a b c d. a < b ∧ c < d ⇒ a + c < b + d

⊢ ∀a b c d. a < b ∧ c < d ⇒ a * c < b * d

⊢ ∀n m. MAX 1 (m ** n) = MAX 1 m ** n

⊢ ∀n. 0 < n ⇒ MAX 1 n = n

⊢ ∀a b c. MAX a (b + c) ≤ MAX a b + MAX a c

⊢ ∀m n. MAX m n = if m ≤ n then n else m

⊢ ∀m n. MAX (MAX m n) n = MAX m n ∧ MAX m (MAX m n) = MAX m n

⊢ ∀m n. m ≤ MAX m n ∧ n ≤ MAX m n

⊢ ∀x y n. x < n ∧ y < n ⇒ MAX x y < n

⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ MAX a c ≤ MAX b d

⊢ ∀m n. MAX m n ≤ m + n

⊢ ∀s. FINITE s ∧ s ≠ ∅ ∧ s ≠ {MIN_SET s} ⇒
      MAX_SET (s DELETE MIN_SET s) = MAX_SET s

⊢ ∀n. MAX_SET (natural n) = n

⊢ ∀f b c x. x − b ≤ c ⇒ f x ≤ MAX_SET {f x | x − b ≤ c}

⊢ ∀f b c x. 0 < b ∧ x DIV b ≤ c ⇒ f x ≤ MAX_SET {f x | x DIV b ≤ c}

⊢ ∀f c x. HALF x ≤ c ⇒ f x ≤ MAX_SET {f x | HALF x ≤ c}

⊢ ∀m n. MAX (SUC m) (SUC n) = SUC (MAX m n)

⊢ ∀f. MONO f ⇒ ∀x y. f (MAX x y) = MAX (f x) (f y)

⊢ ∀n m. MIN 1 (m ** n) = MIN 1 m ** n

⊢ ∀n. 0 < n ⇒ MIN 1 n = 1

⊢ ∀a b c. MIN a (b + c) ≤ MIN a b + MIN a c

⊢ ∀m n. MIN m n = if m ≤ n then m else n

⊢ ∀m n. MIN (MIN m n) n = MIN m n ∧ MIN m (MIN m n) = MIN m n

⊢ ∀m n. MIN m n ≤ m ∧ MIN m n ≤ n

⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ MIN a c ≤ MIN b d

⊢ ∀m n. MIN m n ≤ m + n

⊢ ∀m n. MIN (SUC m) (SUC n) = SUC (MIN m n)

⊢ ∀f. MONO f ⇒ ∀x y. f (MIN x y) = MIN (f x) (f y)

⊢ ∀p x. prime p ∧ 0 < x ∧ x < p ⇒ ∃y. 0 < y ∧ y < p ∧ y * x MOD p = 1

⊢ ∀p x y z.
    prime p ∧ x * y MOD p = x * z MOD p ∧ x MOD p ≠ 0 ⇒ y MOD p = z MOD p

⊢ ∀p x y z.
    prime p ∧ y * x MOD p = z * x MOD p ∧ x MOD p ≠ 0 ⇒ y MOD p = z MOD p

⊢ ∀m n. 0 < m ⇒ SUC (n MOD m) = SUC n MOD m + (SUC n DIV m − n DIV m) * m

⊢ ∀f m. (∀k. k < m ⇒ f k < f (k + 1)) ⇒ ∀k. k < m ⇒ f k < f m

⊢ ∀n k. HALF n < k ⇒ n − k ≤ HALF n

⊢ ∀x y z. x * y * z = 0 ⇔ x = 0 ∨ y = 0 ∨ z = 0

⊢ ∀x y z. x * y * z = 1 ⇔ x = 1 ∧ y = 1 ∧ z = 1

⊢ ∀n m. n divides m ⇒ ∀x. m − n < x ∧ x < m + n ∧ n divides x ⇒ x = m

⊢ ∀n k. 0 < n ⇒ k * n + 1 ≤ (k + 1) * n

⊢ ∀n p q. 0 < n ∧ n divides q ⇒ p * (q DIV n) = p * q DIV n

⊢ ∀a b c d. 0 < a ∧ 0 < b ∧ a < c ∧ a * b = c * d ⇒ d < b

⊢ ∀n. EVEN n ⇒ ∀m. m * n = TWICE m * HALF n

⊢ ∀m n k. 0 < k ∧ k * m ≤ n ⇒ m ≤ n

⊢ ∀m n k. 0 < k ∧ k * m < n ⇒ m < n

⊢ ∀n. ODD n ⇒ ∀m. m * n = m + TWICE m * HALF n

⊢ ∀n. ¬(1 < n) ⇔ n = 0 ∨ n = 1

⊢ ¬prime 4

⊢ ∀n. n ≠ 0 ⇔ 1 ≤ n

⊢ ODD 1

⊢ ∀m n. 0 < n ∧ ODD m ⇒ ODD (m ** n)

⊢ ∀n. ODD n ⇒ n = TWICE (HALF n) + 1

⊢ ∀x. ODD x ⇔ x MOD 2 = 1

⊢ ∀n. prime n ∧ n ≠ 2 ⇒ ODD n

⊢ ∀n. ODD n² ⇔ ODD n

⊢ ∀n. ODD n ⇒ HALF (SUC n) = SUC (HALF n)

⊢ ∀n. 1 < n ⇒ 1 < HALF n²

⊢ ∀n. 1 < n ⇒ n ≠ 0

⊢ ∀n. 1 < n ⇒ 0 < n

⊢ 1 ≠ 0

⊢ 1 ≠ 0

⊢ ∀p q r. (p ∨ q ⇒ r) ⇒ p ∧ ¬q ⇒ r

⊢ ∀n. 1 < n ⇒ ∀m. n ** m = n ⇔ m = 1

⊢ ∀n. 0 < n ⇒ PRE n < n

⊢ ∀p q n. prime p ∧ q divides p ** n ⇒ q = 1 ∨ p divides q

⊢ ∀n. 1 < n ∧ ¬prime n ⇒ ∃p. prime p ∧ p < n ∧ p divides n

⊢ ∀s. FINITE s ⇒ ∀n x. x ∈ s ∧ n divides x ⇒ n divides PROD_SET s

⊢ ∀s x. FINITE s ∧ x ∈ s ⇒ x divides PROD_SET s

⊢ ∀s. FINITE s ⇒
      ∀p. prime p ∧ p divides PROD_SET s ⇒ ∃b. b ∈ s ∧ p divides b

⊢ ∀s. FINITE s ⇒ ∀f. INJ f s 𝕌(:num) ⇒ PROD_SET (IMAGE f s) = Π f s

⊢ ∀n. 1 < n ⇒
      ∀m. PROD_SET (IMAGE (λj. n ** j) (count m)) = n ** SUM_SET (count m)

⊢ ∀n m.
    PROD_SET (IMAGE (λj. n ** j) (count m)) =
    PROD_SET (IMAGE (λj. n ** j) (residue m))

⊢ ∀s. FINITE s ∧ s ≠ ∅ ∧ 0 ∉ s ⇒
      ∀f. INJ f s 𝕌(:num) ∧ (∀x. x < f x) ⇒
          PROD_SET s < PROD_SET (IMAGE f s)

⊢ ∀s. FINITE s ⇒
      ∀f g.
        INJ f s 𝕌(:num) ∧ INJ g s 𝕌(:num) ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
        PROD_SET (IMAGE f s) ≤ PROD_SET (IMAGE g s)

⊢ ∀s. FINITE s ∧ s ≠ ∅ ∧ 0 ∉ s ⇒ PROD_SET s < PROD_SET (IMAGE SUC s)

⊢ ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ x ≤ n) ⇒ PROD_SET s ≤ n ** CARD s

⊢ ∀s. FINITE s ∧ 0 ∉ s ⇒ 0 < PROD_SET s

⊢ ∀s. FINITE s ⇒ ∀u v. s =|= u # v ⇒ PROD_SET s = PROD_SET u * PROD_SET v

⊢ ∀s. FINITE s ⇒
      ∀n f g.
        INJ f s 𝕌(:num) ∧ INJ g s 𝕌(:num) ∧ (∀x. x ∈ s ⇒ n ≤ f x * g x) ⇒
        n ** CARD s ≤ PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s)

⊢ ∀x. PROD_SET {x} = x

⊢ ∀b x s t. x ∈ (if b then s else t) ⇔ if b then x ∈ s else x ∈ t

⊢ ∀n. n ≤ n²

⊢ ∀s t. s = t ⇔ s ⊆ t ∧ t DIFF s = ∅

⊢ ∀n s. FINITE s ∧ (∀e. e ∈ s ⇒ n divides CARD e) ⇒ n divides ∑ CARD s

⊢ ∀s x. {x} ⊆ s ∧ SING s ⇔ s = {x}

⊢ ∀s u. u ⊆ s ⇒ (let v = s DIFF u in s =|= u # v)

⊢ ∀s u v. FINITE s ∧ s =|= u # v ⇒ CARD s = CARD u + CARD v

⊢ ∀s t. s =|= ∅ # t ⇔ s = t

⊢ ∀s u v. s =|= u # v ⇔ u ⊆ s ∧ v = s DIFF u

⊢ ∀s u v. s =|= u # v ⇔ u = s DIFF v ∧ v = s DIFF u

⊢ ∀s u v. FINITE s ∧ s =|= u # v ⇒ FINITE u ∧ FINITE v

⊢ ∀s v x. s =|= {x} # v ⇔ x ∈ s ∧ v = s DELETE x

⊢ ∀s u v. s =|= u # v ⇒ u ⊆ s ∧ v ⊆ s

⊢ ∀s u v. s =|= u # v ⇔ s =|= v # u

⊢ ∀s u v. s =|= u # v ⇒ s =|= v # u

⊢ ∀s u v a b. s =|= u # v ∧ v =|= a # b ⇒ s =|= u ∪ a # b ∧ u ∪ a =|= u # a

⊢ 0² = 0

⊢ ∀n. SQ n = 0 ⇔ n = 0

⊢ ∀n. SQ n = 1 ⇔ n = 1

⊢ ∀n. SQ n = n ⇔ n = 0 ∨ n = 1

⊢ ∀m n. m ≤ n ⇒ SQ m ≤ SQ n

⊢ ∀s t. FINITE t ∧ s ⊆ t ⇒ (CARD s = CARD t ⇔ s = t)

⊢ ∀a b. FINITE a ∧ b ⊆ a ⇒ CARD (a DIFF b) = CARD a − CARD b

⊢ ∀s t. t ⊆ s ⇒ s DIFF (s DIFF t) = t

⊢ ∀s1 s2 t. s1 ⊆ t ∧ s2 ⊆ t ∧ t DIFF s1 = t DIFF s2 ⇒ s1 = s2

⊢ ∀s1 s2 x. s1 ⊆ s2 ⇒ x INSERT s1 ⊆ x INSERT s2

⊢ ∀s t u. s ⊆ u ⇒ s ∩ t ⊆ u

⊢ ∀s x. s ⊆ {x} ⇔ s = ∅ ∨ s = {x}

⊢ ∀m n. 0 < n ⇒ (m − n) DIV n = if m < n then 0 else m DIV n − 1

⊢ ∀p. 0 < p ⇒ ∀m n. m − n = p ⇔ m = n + p

⊢ ∀m n. 0 < n ⇒ (m − n) MOD n = if m < n then 0 else m MOD n

⊢ ∀a b c. c ≤ a ⇒ a − b − (a − c) = c − b

⊢ ∀m n. SUC m + SUC n = m + n + 2

⊢ ∀m n. SUC m = SUC n ⇔ m = n

⊢ ∀n. 0 < n ⇒ ∃m. n = SUC m

⊢ ∀m n. SUC (MAX m n) = MAX (SUC m) (SUC n)

⊢ ∀m n. SUC (MIN m n) = MIN (SUC m) (SUC n)

⊢ ∀m n. SUC m * SUC n = m * n + m + n + 1

⊢ ∀n. (SUC n)² = SUC n² + TWICE n

⊢ ∀n. 1 < n ⇒ SUC n < 2 ** n

⊢ ∀s. FINITE s ⇒
      ∀f. (∀x y. f x = f y ⇒ x = y) ⇒ ∑ f s = SUM_SET (IMAGE f s)

⊢ ∀f x y. x ≠ y ⇒ ∑ f {x; y} = f x + f y

⊢ ∀f s t. FINITE s ∧ t ⊂ s ∧ (∀x. x ∈ s ⇒ f x ≠ 0) ⇒ ∑ f t < ∑ f s

⊢ ∀f x y z. x ≠ y ∧ y ≠ z ∧ z ≠ x ⇒ ∑ f {x; y; z} = f x + f y + f z

⊢ ∀m n. 1 < m ∧ 1 < n ⇒ m + n ≤ m * n

⊢ ∀n. SUM_SET (count n) = HALF (n * (n − 1))

⊢ ∀s. FINITE s ⇒ ∀f. INJ f s 𝕌(:num) ⇒ SUM_SET (IMAGE f s) = ∑ f s

⊢ ∀f s t. SURJ f s t ⇒ CARD (IMAGE f s) = CARD t

⊢ 3 = SUC 2

⊢ ∀n. TWICE n = 0 ⇔ n = 0

⊢ ∀n. TWICE (HALF n) ≤ n ∧ n ≤ SUC (TWICE (HALF n))

⊢ ∀m n. TWICE (HALF n * m) ≤ n * m

⊢ ∀p. prime p ⇒ 2 ≤ p

⊢ ∀s t. s ∪ (t DIFF s) = s ∪ t

⊢ ∀n. 0 ≤ n

⊢ ∀m n. (m + n)² = m² + n² + TWICE m * n

⊢ ∀a b. (a + b)² = a² + b² + TWICE a * b

⊢ ∀a b. TWICE a * b ≤ a² + b²

⊢ ∀a b. b ≤ a ⇒ (a − b)² = a² + b² − TWICE a * b

⊢ ∀a b. b ≤ a ⇒ (a − b)² + 4 * a * b = (a + b)²

⊢ ∀a b. b ≤ a ⇒ (a − b)² + TWICE a * b = a² + b²

⊢ ∀s. FINITE s ∧ (∀e. e ∈ s ⇒ CARD e ≠ 0) ∧ CARD s = ∑ CARD s ⇒
      ∀e. e ∈ s ⇒ CARD e = 1

⊢ ∀s. FINITE s ∧ (∀e. e ∈ s ⇒ CARD e ≠ 0) ⇒ CARD s ≤ ∑ CARD s

⊢ ∀s n. 0 < n ⇒ CARD (IMAGE (λx. x MOD n) s) ≤ n

⊢ ∀s n.
    0 < n ∧ 0 ∉ IMAGE (λx. x MOD n) s ⇒ CARD (IMAGE (λx. x MOD n) s) < n

⊢ ∀n. 1 < n ⇒ ∀m. (∀j. 0 < j ∧ j ≤ m ⇒ coprime n j) ⇒ m < n

⊢ ∀m n. 1 < m ∧ (∀j. 1 < j ∧ j ≤ m ⇒ ¬(j divides n)) ⇒ coprime m n

⊢ ∀m n.
    (∀j. 1 < j ∧ j ≤ m ⇒ ¬(j divides n)) ⇔ ∀j. 1 < j ∧ j ≤ m ⇒ coprime j n

⊢ ∀n. 0 < n ⇒ ∀a b. coprime a b ⇔ coprime a (b ** n)

⊢ ∀a b.
    0 < a ∧ 0 < b ∧ coprime a b ⇒
    ∃p q. (p * a + q * b) MOD (a * b) = 1 MOD (a * b)

⊢ ∀a b p q.
    coprime a b ∧ coprime p b ∧ coprime q a ⇒
    coprime (p * a + q * b) (a * b)

⊢ ∀a b p q.
    coprime a b ⇒
    (coprime p b ∧ coprime q a ⇔ coprime (p * a + q * b) (a * b))

⊢ ∀m n a b.
    0 < m ∧ 0 < n ∧ coprime m n ∧ a MOD m = b MOD m ∧ a MOD n = b MOD n ⇒
    a MOD (m * n) = b MOD (m * n)

⊢ ∀m n.
    0 < m ∧ 0 < n ∧ coprime m n ⇒
    ∀a b.
      a MOD (m * n) = b MOD (m * n) ⇔ a MOD m = b MOD m ∧ a MOD n = b MOD n

⊢ ∀m n a b.
    0 < m ∧ 0 < n ∧ coprime m n ⇒
    ∃!x. x < m * n ∧ x MOD m = a MOD m ∧ x MOD n = b MOD n

⊢ ∀a b c.
    0 < a ∧ 0 < b ∧ coprime a b ⇒
    ∃p q. (p * a + q * b) MOD (a * b) = c MOD (a * b)

⊢ ∀m n. 1 < n ∧ coprime n m ⇒ ¬(n divides m)

⊢ ∀b m n. 0 < b ∧ 0 < m ⇒ coprime (b ** n) (tops b m)

⊢ ∀b m n. 0 < b ∧ 0 < m ⇒ coprime (b ** n) (b ** m + 1)

⊢ ∀p n. prime p ∧ 0 < n ⇒ ∀q. coprime q (p ** n) ⇔ ¬(p divides q)

⊢ ∀m. countFrom m 0 = ∅

⊢ ∀m n m n. countFrom m (SUC n) = m INSERT countFrom (m + 1) n

⊢ ∀m n. 0 < n ⇒ m ∈ countFrom m n

⊢ ∀m n x. x < m ⇒ x ∉ countFrom m n

⊢ ∀n. upto n = 0 INSERT countFrom 1 n

⊢ ∀n. count n = countFrom 0 n

⊢ ∀a b. a² − b² = (a − b) * (a + b)

⊢ ∀a b. SQ a − SQ b = (a − b) * (a + b)

⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
      ∀f. SET_ADDITIVE f ⇒ f (BIGUNION P) = ∑ f P

⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
      CARD (BIGUNION P) = ∑ CARD P

⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
      ∀f. SET_MULTIPLICATIVE f ⇒ f (BIGUNION P) = Π f P

⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
      ∀f. ∑ f (BIGUNION P) = ∑ (∑ f) P

⊢ ∀m n. 0 < m ∧ n divides m ⇒ ∀t. m divides t * n ⇔ m DIV n divides t

⊢ ∀a b. a divides b ∧ 0 < b ∧ b < TWICE a ⇒ b = a

⊢ ∀m n. 0 < n ∧ n < TWICE m ⇒ (m divides n ⇔ n = m)

⊢ ∀n p. 0 < n ∧ 1 < p ⇒ p divides p ** n

⊢ ∀R s n.
    FINITE s ∧ R equiv_on s ∧ (∀e. e ∈ partition R s ⇒ CARD e = n) ⇒
    CARD s = n * CARD (partition R s)

⊢ ∀R s n.
    FINITE s ∧ R equiv_on s ∧ (∀e. e ∈ partition R s ⇒ CARD e = n) ⇒
    n divides CARD s

⊢ ∀R s x y. y ∈ equiv_class R s x ⇔ y ∈ s ∧ R x y

⊢ ∀R s x. R equiv_on s ∧ x ∈ s ⇒ equiv_class R s x ≠ ∅

⊢ ∀a b c. coprime a b ∧ b divides a * c ⇒ b divides c

⊢ ∀p a b. prime p ∧ p divides a * b ⇒ p divides a ∨ p divides b

⊢ ∀s. FINITE s ⇒
      ∀x. x ∉ s ∧ (∀z. z ∈ s ⇒ coprime x z) ⇒ coprime x (PROD_SET s)

⊢ ∀m n. 0 < m ∧ m divides n ⇒ (m = n DIV m ⇔ n = m²)

⊢ ∀R s n.
    FINITE s ∧ R equiv_on s ∧ (∀e. e ∈ partition R s ⇒ n divides CARD e) ⇒
    n divides CARD s

⊢ ∀f s x y. x ∈ preimage f s y ⇔ x ∈ s ∧ f x = y

⊢ ∀f s. preimage f s ∘ f = (λx. equiv_class (feq f) s x)

⊢ ∀f s x. preimage f s (f x) = equiv_class (feq f) s x

⊢ ∀s f. feq f equiv_on s

⊢ ∀s f. partition (feq f) s = IMAGE (preimage f s ∘ f) s

⊢ ∀s f t.
    t ∈ partition (feq f) s ⇔ ∃z. z ∈ s ∧ ∀x. x ∈ t ⇔ x ∈ s ∧ f x = f z

⊢ ∀f s x. x ∈ s ⇔ ∃e. e ∈ partition (feq f) s ∧ x ∈ e

⊢ ∀f s e. e ∈ partition (feq f) s ⇒ e ≠ ∅

⊢ ∀s. FINITE s ⇒ ∀f g. ∑ g s = ∑ (∑ g) (partition (feq f) s)

⊢ ∀f. (λx y. (x == y) f) equiv_on 𝕌(:α)

⊢ ∀f x. (x == x) f

⊢ ∀f x y. (x == y) f ⇒ (y == x) f

⊢ ∀f x y z. (x == y) f ∧ (y == z) f ⇒ (x == z) f

⊢ ∀s. FINITE s ⇒ ∀f. CARD s = ∑ CARD (partition (feq f) s)

⊢ ∀s. FINITE s ⇒ ∀f. CARD s = ∑ CARD (IMAGE (preimage f s ∘ f) s)

⊢ ∀f s t. FINITE s ∧ SURJ f s t ⇒ CARD s = ∑ CARD (IMAGE (preimage f s) t)

⊢ ∀s. FINITE s ⇒
      ∀P. (let
             u = {x | x ∈ s ∧ P x};
             v = {x | x ∈ s ∧ ¬P x}
           in
             FINITE u ∧ FINITE v ∧ s =|= u # v)

⊢ ∀s. FINITE s ⇒ ∀u v. s =|= u # v ⇒ (u = ∅ ⇔ v = s)

⊢ 1 + 2 + 3 + 4 = 10

⊢ 1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100

⊢ ∀a b c. 0 < a ⇒ (gcd a b divides c ⇔ ∃p q. p * a = q * b + c)

⊢ ∀m n. 0 < m ∧ 0 < n ⇒ gcd m n ≤ m ∧ gcd m n ≤ n

⊢ ∀a b. 0 < a ⇒ ∃q. q * b MOD a = gcd a b MOD a

⊢ ∀a b. 0 < b ⇒ ∃p. p * a MOD b = gcd a b MOD b

⊢ ∀a b.
    0 < a ∧ 0 < b ⇒ ∃p q. (p * a + q * b) MOD (a * b) = gcd a b MOD (a * b)

⊢ ∀n a b. 0 < n ∧ 0 < a ⇒ ∃p q. (p * a + q * b) MOD n = gcd a b MOD n

⊢ ∀a b c. 0 < a ⇒ (gcd a b divides c ⇔ ∃p q. p * a = q * b + c)

⊢ ∀a b c.
    0 < a ∧ 0 < b ∧ gcd a b divides c ⇒
    ∃p q. (p * a + q * b) MOD (a * b) = c MOD (a * b)

⊢ ∀n a b c.
    0 < n ∧ 0 < a ∧ gcd a b divides c ⇒
    ∃p q. (p * a + q * b) MOD n = c MOD n

⊢ ∀b m n. gcd (b ** m) (b ** n) = b ** MIN m n

⊢ ∀s n. 0 < n ⇒ IMAGE (λx. x MOD n) s ⊆ count n

⊢ ∀f s x y. x ∈ preimage f s y ⇔ x ∈ s ∧ f x = y

⊢ ∀p. p ∈ prime ⇔ prime p

⊢ ∀f s.
    FINITE s ⇒
    (INJ f s (IMAGE f s) ⇔ ∀e. e ∈ partition (feq f) s ⇒ CARD e = 1)

⊢ ∀f s. INJ f s (IMAGE f s) ⇔ ∀e. e ∈ partition (feq f) s ⇒ SING e

⊢ ∀b m n. lcm (b ** m) (b ** n) = b ** MAX m n

⊢ ∀m n. m < n ⇒ [m; n] ≤ [m .. n]

⊢ ∀m n. m + 1 < n ⇒ [m; n − 1] ≤ [m ..< n]

⊢ ∀n a b c d.
    b < n ∧ c < n ⇒
    ((a + b) MOD n = (c + d) MOD n ⇔
     (a + (n − c)) MOD n = (d + (n − b)) MOD n)

⊢ ∀n a b c d.
    0 < n ⇒
    ((a + b) MOD n = (c + d) MOD n ⇔
     (a + (n − c MOD n)) MOD n = (d + (n − b MOD n)) MOD n)

⊢ ∀n a b. 0 < n ∧ b divides n ∧ b divides a MOD n ⇒ b divides a

⊢ ∀n a b c. 0 < n ∧ a MOD n = b ∧ c divides n ∧ c divides a ⇒ c divides b

⊢ ∀n a b c. 0 < n ∧ a MOD n = b ∧ c divides n ⇒ (c divides a ⇔ c divides b)

⊢ ∀n a b. 0 < n ∧ b divides n ⇒ (b divides a MOD n ⇔ b divides a)

⊢ ∀n a b c.
    0 < n ∧ a MOD n = b MOD n ∧ c divides n ∧ c divides a ⇒ c divides b

⊢ ∀n a b c.
    0 < n ∧ a MOD n = b MOD n ∧ c divides n ⇒ (c divides a ⇔ c divides b)

⊢ ∀m n a b.
    0 < m ∧ 0 < n ∧ a MOD (m * n) = b MOD (m * n) ⇒
    a MOD m = b MOD m ∧ a MOD n = b MOD n

⊢ ∀m n a b.
    coprime m n ∧ 0 < a ∧ a < TWICE n ∧ 0 < b ∧ b < TWICE m ∧
    m * a MOD (m * n) = n * b MOD (m * n) ⇒
    a = n ∧ b = m

⊢ ∀n. natural n = upto n DELETE 0

⊢ ∀n. natural n = set (GENLIST SUC n)

⊢ ∀n m. nines n divides nines m ⇔ n divides m

⊢ ∀m n. m ≤ n ⇒ nines n − 10 ** (n − m) * nines m = nines (n − m)

⊢ ∀m n. m ≤ n ⇒ nines n = 10 ** (n − m) * nines m + nines (n − m)

⊢ ∀n. 9 divides nines n

⊢ ∀n m. gcd (nines n) (nines m) = nines (gcd n m)

⊢ ∀n m. m ≤ n ⇒ gcd (nines n) (nines m) = gcd (nines m) (nines (n − m))

⊢ ∀s t. t ⊆ s ∧ PAIR_DISJOINT s ⇒ PAIR_DISJOINT t

⊢ ∀s e.
    e ∉ s ∧ PAIRWISE_COPRIME (e INSERT s) ⇒
    (∀x. x ∈ s ⇒ coprime e x) ∧ PAIRWISE_COPRIME s

⊢ ∀s. FINITE s ∧ PAIRWISE_COPRIME s ⇒
      ∀u v. s =|= u # v ⇒ coprime (PROD_SET u) (PROD_SET v)

⊢ ∀s. FINITE s ∧ PAIRWISE_COPRIME s ⇒
      ∀u v.
        s =|= u # v ⇒
        PROD_SET s = PROD_SET u * PROD_SET v ∧
        coprime (PROD_SET u) (PROD_SET v)

⊢ ∀s. FINITE s ∧ PAIRWISE_COPRIME s ⇒
      ∀t. t ⊆ s ⇒ PROD_SET t divides PROD_SET s

⊢ ∀R s. partition R s = IMAGE (λx. equiv_class R s x) s

⊢ ∀s x. x ∈ s ⇒ s =|= {x} # s DELETE x

⊢ ∀s u. u ⊆ s ⇒ (let v = s DIFF u in s =|= u # v)

⊢ ∀R1 R2 s1 s2. R1 = R2 ∧ s1 = s2 ⇒ partition R1 s1 = partition R2 s2

⊢ ∀R s t. t ∈ partition R s ⇔ ∃x. x ∈ s ∧ t = equiv_class R s x

⊢ ∀R s x. R equiv_on s ⇒ (x ∈ s ⇔ ∃e. e ∈ partition R s ∧ x ∈ e)

⊢ ∀R s e. R equiv_on s ∧ e ∈ partition R s ⇒ e ≠ ∅

⊢ ∀R s. partition R s = IMAGE (λx. equiv_class R s x) s

⊢ ∀R. partition R ∅ = ∅

⊢ ∀p. 1 < p ⇒ ∀m n. p ** m divides p ** n ⇔ m ≤ n

⊢ ∀p. prime p ⇒
      ∀b n m. 0 < m ∧ b ** n = p ** m ⇒ ∃k. b = p ** k ∧ k * n = m

⊢ ∀n. 0 < n ⇒ ∀m. (EVEN m ⇔ EVEN (m ** n)) ∧ (ODD m ⇔ ODD (m ** n))

⊢ ∀t n m. 1 < t ⇒ (tops t n divides tops t m ⇔ n divides m)

⊢ ∀t m n.
    0 < t ∧ m ≤ n ⇒ tops t n − t ** (n − m) * tops t m = tops t (n − m)

⊢ ∀t m n.
    0 < t ∧ m ≤ n ⇒ tops t n = t ** (n − m) * tops t m + tops t (n − m)

⊢ ∀t n. t − 1 divides tops t n

⊢ ∀t n m. gcd (tops t n) (tops t m) = tops t (gcd n m)

⊢ ∀t n m.
    m ≤ n ⇒ gcd (tops t n) (tops t m) = gcd (tops t m) (tops t (n − m))

⊢ ∀f s y. preimage f s y = PREIMAGE f {y} ∩ s

⊢ ∀f s y.
    y ∈ IMAGE f s ⇒
    CHOICE (preimage f s y) ∈ s ∧ f (CHOICE (preimage f s y)) = y

⊢ ∀f s x y. x ∈ preimage f s y ⇔ x ∈ s ∧ f x = y

⊢ ∀f s y. FINITE s ⇒ FINITE (preimage f s y)

⊢ ∀f s. BIJ (preimage f s) (IMAGE f s) (partition (feq f) s)

⊢ ∀f s. INJ (preimage f s) (IMAGE f s) (POW s)

⊢ ∀f s. INJ f s 𝕌(:β) ⇒ ∀x. x ∈ s ⇒ preimage f s (f x) = {x}

⊢ ∀f s. INJ f s 𝕌(:β) ⇒ ∀x. x ∈ s ⇒ CHOICE (preimage f s (f x)) = x

⊢ ∀f s x. x ∈ s ⇒ x ∈ preimage f s (f x)

⊢ ∀f s y x. x ∈ preimage f s y ⇒ f x = y

⊢ ∀f s y. preimage f s y ⊆ s

⊢ ∀m n. prime n ∧ m < n ⇒ ∀j. 0 < j ∧ j ≤ m ⇒ coprime n j

⊢ ∀n. prime n ⇒ ∀m. 0 < m ∧ m < n ⇒ coprime n m

⊢ ∀p n. prime p ∧ 0 < n ⇒ ∀b. p divides b ** n ⇔ p divides b

⊢ ∀n m. prime n ∧ prime m ⇒ (n divides m ⇔ n = m)

⊢ ∀m n k. prime m ∧ prime n ∧ m divides n ** k ⇒ m = n

⊢ ∀p. prime p ⇒ ∀n. 0 < n ⇒ p divides p ** n

⊢ ∀n. prime n ⇔ 1 < n ∧ ∀j. 0 < j ∧ j < n ⇒ coprime n j

⊢ ∀n. prime n ⇔ 1 < n ∧ ∀j. 1 < j ∧ j < n ⇒ ¬(j divides n)

⊢ ∀p. prime p ⇒ ∀m n. p ** m divides p ** n ⇔ m ≤ n

⊢ ∀p n a. prime p ∧ a divides p ** n ⇒ ∃j. j ≤ n ∧ a = p ** j

⊢ ∀n p. 0 < n ∧ prime p ⇒ ∃q m. n = p ** m * q ∧ coprime p q

⊢ ∀p q. prime p ∧ prime q ∧ p ≠ q ⇒ ∀m n. coprime (p ** m) (q ** n)

⊢ ∀p q.
    prime p ∧ prime q ⇒
    ∀m n. 0 < m ⇒ (p ** m divides q ** n ⇔ p = q ∧ m ≤ n)

⊢ ∀p q. prime p ∧ prime q ⇒ ∀m n. 0 < m ∧ p ** m = q ** n ⇒ p = q ∧ m = n

⊢ ∀n. PROD_SET (residue n) = FACT (n − 1)

⊢ residue 0 = ∅

⊢ residue 1 = ∅

⊢ ∀n. 0 < n ⇒ CARD (residue n) = n − 1

⊢ ∀n. 0 < n ⇒ count n = 0 INSERT residue n

⊢ ∀n. 0 < n ⇒ residue n DELETE n = residue n

⊢ ∀n j. j ∈ residue n ⇒ 0 < j ∧ j < n

⊢ ∀n. FINITE (residue n)

⊢ ∀n. 0 < n ⇒ residue (SUC n) = n INSERT residue n

⊢ ∀n. n ∉ residue n

⊢ ∀n. 0 ∉ residue n

⊢ ∀n. 1 < n ⇒ residue n ≠ ∅

⊢ ∀p a n.
    prime p ∧ a ∈ residue p ∧ n ≤ p ⇒
    ∀x. x ∈ residue n ⇒ a * n MOD p ≠ a * x MOD p

⊢ ∀n. 0 < n ⇒ residue (SUC n) = n INSERT residue n

⊢ ∀n. residue n = count n DIFF {0}

⊢ ∀R s.
    R equiv_on s ∧ FINITE s ⇒
    ∀f. SET_ADDITIVE f ⇒ f s = ∑ f (partition R s)

⊢ SET_ADDITIVE CARD

⊢ ∀f. SET_ADDITIVE (∑ f)

⊢ ∀R s. R equiv_on s ∧ FINITE s ⇒ CARD s = ∑ CARD (partition R s)

⊢ ∀R s.
    R equiv_on s ∧ FINITE s ⇒
    ∀f. SET_MULTIPLICATIVE f ⇒ f s = Π f (partition R s)

⊢ ∀R s. R equiv_on s ∧ FINITE s ⇒ ∀f. ∑ f s = ∑ (∑ f) (partition R s)

⊢ ∀p. 1 < p ⇒ ∀n. ∑ (λj. p ** j) (natural n) = p * tops p n DIV (p − 1)

⊢ ∀p. 0 < p ⇒ ∀n. (p − 1) * ∑ (λj. p ** j) (natural n) = p * tops p n

⊢ ∀ls sl j h.
    sl ≤ ls ∧ ALL_DISTINCT ls ∧ j < h ∧ h < LENGTH sl ⇒
    findi sl❲j❳ ls < findi sl❲h❳ ls

⊢ ∀s. FINITE s ⇒ ∀g. INJ g s 𝕌(:α) ⇒ ∀f. ∑ f (IMAGE g s) = ∑ (f ∘ g) s

⊢ ∀s. FINITE s ⇒
      ∀f. f ∅ = 0 ⇒
          ∀g. (∀t. FINITE t ∧ (∀x. x ∈ t ⇒ g x ≠ ∅) ⇒ INJ g t 𝕌(:β -> bool)) ⇒
              ∑ f (IMAGE g s) = ∑ (f ∘ g) s

⊢ ∀s. FINITE s ⇒
      ∀f g.
        (∀x y. x ∈ s ∧ y ∈ s ∧ g x = g y ⇒ x = y ∨ f (g x) = 0) ⇒
        ∑ f (IMAGE g s) = ∑ (f ∘ g) s

⊢ ∀s. FINITE s ⇒ ∀g. g PERMUTES s ⇒ ∀f. ∑ (f ∘ g) s = ∑ f s

⊢ ∀n. upto n = n INSERT count n

⊢ ∀n. upto n = 0 INSERT natural n

⊢ ∀n. CARD (upto n) = SUC n

⊢ ∀n. upto n DELETE n = count n

⊢ ∀n. FINITE (upto n)

⊢ ∀n. n ∈ upto n

⊢ ∀n. upto n = {0} ∪ natural n

⊢ ∀n. upto n = count n ∪ {n}