Theory combinatorics

⊢ (∀e n. MDILATE e n [] = []) ∧
  ∀e n h t.
    MDILATE e n (h::t) =
    if t = [] then [h] else h::GENLIST (K e) (PRE n) ⧺ MDILATE e n t

⊢ PROD [] = 1 ∧ ∀h t. PROD (h::t) = h * PROD t

⊢ (∀acc. PROD_ACC [] acc = acc) ∧
  ∀h t acc. PROD_ACC (h::t) acc = PROD_ACC t (h * acc)

⊢ ∀n k. n arrange k = CARD (list_count n k)

⊢ ∀n k. n choose k = CARD (sub_count n k)

⊢ ∀x ls.
    x interleave ls =
    IMAGE (λk. TAKE k ls ⧺ x::DROP k ls) (upto (LENGTH ls))

⊢ lcm_upto 0 = 1 ∧ ∀n. lcm_upto (SUC n) = lcm (SUC n) (lcm_upto n)

⊢ ∀n k. leibniz n k = (n + 1) * binomial n k

⊢ ∀p1 p2.
    p1 zigzag p2 ⇔ ∃n k x y. p1 = x ⧺ [tb; ta] ⧺ y ∧ p2 = x ⧺ [tb; tc] ⧺ y

⊢ ∀n k.
    list_count n k =
    {ls | ALL_DISTINCT ls ∧ set ls ⊆ count n ∧ LENGTH ls = k}

⊢ list_lcm [] = 1 ∧ ∀h t. list_lcm (h::t) = lcm h (list_lcm t)

⊢ ∀n a.
    monocoloured n a = {ls | ls ∈ necklace n a ∧ (ls ≠ [] ⇒ SING (set ls))}

⊢ ∀n a. multicoloured n a = necklace n a DIFF monocoloured n a

⊢ ∀n a. necklace n a = {ls | LENGTH ls = n ∧ set ls ⊆ count a}

⊢ ∀n. perm_count n = {ls | ALL_DISTINCT ls ∧ set ls = count n}

⊢ ∀n. perm n = CARD (perm_count n)

⊢ ∀s. perm_set s = {ls | ALL_DISTINCT ls ∧ set ls = s}

⊢ ∀n n0 n1. (triple n n0 n1).a = n

⊢ ∀f n n0 n1. triple n n0 n1 with a updated_by f = triple (f n) n0 n1

⊢ ∀n n0 n1. (triple n n0 n1).b = n0

⊢ ∀f n n0 n1. triple n n0 n1 with b updated_by f = triple n (f n0) n1

⊢ ∀n n0 n1. (triple n n0 n1).c = n1

⊢ ∀f n n0 n1. triple n n0 n1 with c updated_by f = triple n n0 (f n1)

⊢ ∀n l. rotate n l = DROP n l ⧺ TAKE n l

⊢ ∀s. set_lcm s = list_lcm (SET_TO_LIST s)

⊢ ∀n k. sub_count n k = {s | s ⊆ count n ∧ CARD s = k}

⊢ ∀P k. sub_sets P k = {s | s ⊆ P ∧ CARD s = k}

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('triple').
             (∀a0'.
                (∃a0 a1 a2.
                   a0' =
                   (λa0 a1 a2.
                        ind_type$CONSTR 0 (a0,a1,a2) (λn. ind_type$BOTTOM))
                     a0 a1 a2) ⇒
                $var$('triple') a0') ⇒
             $var$('triple') a0') rep

⊢ ∀a0 a1 a2 f. triple_CASE (triple a0 a1 a2) f = f a0 a1 a2

⊢ ∀a0 a1 a2. triple_size (triple a0 a1 a2) = 1 + (a0 + (a1 + a2))

⊢ ∀n k.
    triplet n k =
    <|a := leibniz n k; b := leibniz (n + 1) k;
      c := leibniz (n + 1) (k + 1)|>

⊢ ∀l. turn l = if l = [] then [] else LAST l::FRONT l

⊢ ∀l. CARD (set l) = LENGTH (nub l)

⊢ ∀l e. DILATE e 0 0 l = l

⊢ ∀n h t e.
    DILATE e 0 n (h::t) =
    if t = [] then [h] else h::(GENLIST (K e) n ⧺ DILATE e 0 n t)

⊢ ∀l e n k.
    k < LENGTH (DILATE e 0 n l) ⇒
    (DILATE e 0 n l)❲k❳ = if k MOD SUC n = 0 then l❲k DIV SUC n❳ else e

⊢ ∀l e n. DILATE e 0 n l = [] ⇔ l = []

⊢ ∀l e n. LAST (DILATE e 0 n l) = LAST l

⊢ ∀l e n.
    LENGTH (DILATE e 0 n l) =
    if l = [] then 0 else SUC (SUC n * PRE (LENGTH l))

⊢ ∀l e n. LENGTH l ≤ LENGTH (DILATE e 0 n l)

⊢ ∀l e n. LENGTH (DILATE e 0 n l) ≤ SUC (SUC n * PRE (LENGTH l))

⊢ ∀l e n. DILATE e 0 (SUC n) l = DILATE e n 1 (DILATE e 0 n l)

⊢ ∀n m h t e.
    DILATE e n m (h::t) =
    if t = [] then [h]
    else h::(TAKE n t ⧺ GENLIST (K e) m ⧺ DILATE e n m (DROP n t))

⊢ ∀n m e. DILATE e n m [] = []

⊢ ∀n m h e. DILATE e n m [h] = [h]

⊢ (∀n m e. DILATE e n m [] = []) ∧ (∀n m h e. DILATE e n m [h] = [h]) ∧
  ∀v9 v8 n m h e.
    DILATE e n m (h::v8::v9) =
    h::(TAKE n (v8::v9) ⧺ GENLIST (K e) m ⧺ DILATE e n m (DROP n (v8::v9)))

⊢ ∀P. (∀e n m. P e n m []) ∧ (∀e n m h. P e n m [h]) ∧
      (∀e n m h v8 v9. P e n m (DROP n (v8::v9)) ⇒ P e n m (h::v8::v9)) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

⊢ ∀h1 t1 h2 t2 P.
    LENGTH (h1::t1) = LENGTH (h2::t2) ∧
    (∀k. k < LENGTH (h1::t1) ⇒ P (h1::t1)❲k❳ (h2::t2)❲k❳) ⇒
    P h1 h2 ∧ ∀k. k < LENGTH t1 ⇒ P t1❲k❳ t2❲k❳

⊢ ∀lx ly lz n.
    n < MIN (MIN (LENGTH lx) (LENGTH ly)) (LENGTH lz) ⇒
    ∀f. (MAP3 f lx ly lz)❲n❳ = f lx❲n❳ ly❲n❳ lz❲n❳

⊢ ∀p R. EVERY (λc. c ∈ R) p ⇒ ∀k. k < LENGTH p ⇒ p❲k❳ ∈ R

⊢ ∀ls n. EVERY (λj. j < n) ls ⇒ EVERY (λj. j ≤ n) ls

⊢ ∀l f P Q. (∀x. P x ⇒ (Q ∘ f) x) ∧ EVERY P l ⇒ EVERY Q (MAP f l)

⊢ ∀P. (∃t. P t) ⇔ ∃n1 n0 n. P <|a := n1; b := n0; c := n|>

⊢ ∀P ls l1 l2 l3 x y.
    (let
       fs = FILTER P ls
     in
       ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ⧺ y::l3 ∧ P x ∧ P y ⇒
       (findi y fs = 1 + findi x fs ⇔ FILTER P l2 = []))

⊢ ∀f s t. FINITE t ⇒ (SURJ f s t ⇔ CARD (IMAGE f s) = CARD t ∧ over f s t)

⊢ ∀P. (∀t. P t) ⇔ ∀n1 n0 n. P <|a := n1; b := n0; c := n|>

⊢ ∀f u n.
    FUNPOW (λls. f (HD ls)::ls) n [u] = MAP (λj. FUNPOW f j u) (n downto 0)

⊢ ∀f u n.
    0 < n ⇒
    FUNPOW (λls. f (HD ls)::ls) (n − 1) [f u] =
    MAP (λj. FUNPOW f j u) (n downto 1)

⊢ ∀f n ls. HD (FUNPOW (λls. f (HD ls)::ls) n ls) = FUNPOW f n (HD ls)

⊢ ∀P Q. FUNSET P Q = {f | over f P Q}

⊢ ∀f n. RMONO f ⇒ MONO_DEC (GENLIST f n)

⊢ ∀f n. MONO f ⇒ MONO_INC (GENLIST f n)

⊢ ∀n x y.
    GENLIST ((λk. binomial n k * x ** SUC (n − k) * y ** k) ∘ SUC) n =
    GENLIST (λk. binomial n (SUC k) * x ** (n − k) * y ** SUC k) n

⊢ ∀f s t. over f s t ⇒ (INJ f s t ⇔ BIJ f s (IMAGE f s))

⊢ ∀f s t. INJ f s t ⇔ BIJ f s (IMAGE f s) ∧ over f s t

⊢ ∀f s t. INJ f s t ⇔ INJ f s (IMAGE f s) ∧ over f s t

⊢ ∀lx ly lz f.
    LENGTH (MAP3 f lx ly lz) =
    MIN (MIN (LENGTH lx) (LENGTH ly)) (LENGTH lz)

⊢ ∀l1 l2 h.
    ¬MEM h l1 ∧ set (h::l1) = set l2 ⇒
    ∃p1 p2.
      ¬MEM h p1 ∧ ¬MEM h p2 ∧ nub l2 = p1 ⧺ [h] ⧺ p2 ∧
      set l1 = set (p1 ⧺ p2)

⊢ ∀ls a h t. (ls ⧺ h::t)❲LENGTH ls ↦ a❳ = ls ⧺ a::t

⊢ ∀ls a b h k t.
    (ls ⧺ h::k::t)❲LENGTH ls + 1 ↦ b; LENGTH ls ↦ a❳ = ls ⧺ a::b::t

⊢ ∀ls b h k t. (ls ⧺ h::k::t)❲LENGTH ls + 1 ↦ b❳ = ls ⧺ h::b::t

⊢ ∀ls m n p q. m ≠ n ⇒ ls❲n ↦ q; m ↦ p❳ = ls❲m ↦ p; n ↦ q❳

⊢ ∀e n l p. p < LENGTH l ⇒ l❲n ↦ e❳❲p❳ = if p = n then e else l❲p❳

⊢ ∀e n l. LENGTH l❲n ↦ e❳ = LENGTH l

⊢ ∀ls n p q. ls❲n ↦ q; n ↦ p❳ = ls❲n ↦ q❳

⊢ ∀f g.
    (∀x y. f x y ≤ g x y) ⇒ ∀lx ly n. (MAP2 f lx ly)❲n❳ ≤ (MAP2 g lx ly)❲n❳

⊢ (∀f. MAP3 f [] [] [] = []) ∧
  ∀f h1 t1 h2 t2 h3 t3.
    MAP3 f (h1::t1) (h2::t2) (h3::t3) = f h1 h2 h3::MAP3 f t1 t2 t3

⊢ (∀t3 t2 t1 h3 h2 h1 f.
     MAP3 f (h1::t1) (h2::t2) (h3::t3) = f h1 h2 h3::MAP3 f t1 t2 t3) ∧
  (∀z y f. MAP3 f [] y z = []) ∧ (∀z v5 v4 f. MAP3 f (v4::v5) [] z = []) ∧
  ∀v5 v4 v13 v12 f. MAP3 f (v4::v5) (v12::v13) [] = []

⊢ ∀P. (∀f h1 t1 h2 t2 h3 t3. P f t1 t2 t3 ⇒ P f (h1::t1) (h2::t2) (h3::t3)) ∧
      (∀f y z. P f [] y z) ∧ (∀f v4 v5 z. P f (v4::v5) [] z) ∧
      (∀f v4 v5 v12 v13. P f (v4::v5) (v12::v13) []) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

⊢ ∀f g.
    (∀x y z. f x y z ≤ g x y z) ⇒
    ∀lx ly lz n. (MAP3 f lx ly lz)❲n❳ ≤ (MAP3 g lx ly lz)❲n❳

⊢ ∀f g. (∀x. f x ≤ g x) ⇒ ∀ls n. (MAP f ls)❲n❳ ≤ (MAP g ls)❲n❳

⊢ ∀f. MONO f ⇒ ∀ls. ls ≠ [] ⇒ MAX_LIST (MAP f ls) = f (MAX_LIST ls)

⊢ ∀l e. MDILATE e 0 l = l

⊢ ∀l e. MDILATE e 1 l = l

⊢ ∀e n h t.
    MDILATE e n (h::t) =
    if t = [] then [h] else h::GENLIST (K e) (PRE n) ⧺ MDILATE e n t

⊢ ∀l e n k.
    k < LENGTH (MDILATE e n l) ⇒
    (MDILATE e n l)❲k❳ =
    if n = 0 then l❲k❳ else if k MOD n = 0 then l❲k DIV n❳ else e

⊢ ∀l e n. MDILATE e n l = [] ⇔ l = []

⊢ ∀l e n. LAST (MDILATE e n l) = LAST l

⊢ ∀l e n.
    LENGTH (MDILATE e n l) =
    if n = 0 then LENGTH l
    else if l = [] then 0
    else SUC (n * PRE (LENGTH l))

⊢ ∀l e n. LENGTH l ≤ LENGTH (MDILATE e n l)

⊢ ∀l e n. 0 < n ⇒ LENGTH (MDILATE e n l) ≤ SUC (n * PRE (LENGTH l))

⊢ ∀e n. MDILATE e n [] = []

⊢ ∀e n x. MDILATE e n [x] = [x]

⊢ ∀f x l1 l2.
    MEM x (MAP2 f l1 l2) ⇒ ∃y1 y2. x = f y1 y2 ∧ MEM y1 l1 ∧ MEM y2 l2

⊢ ∀f. MONO2 f ⇒
      ∀lx ly e. MEM e (MAP2 f lx ly) ⇒ f (MIN_LIST lx) (MIN_LIST ly) ≤ e

⊢ ∀f. MONO2 f ⇒
      ∀lx ly e. MEM e (MAP2 f lx ly) ⇒ e ≤ f (MAX_LIST lx) (MAX_LIST ly)

⊢ ∀f x l1 l2 l3.
    MEM x (MAP3 f l1 l2 l3) ⇒
    ∃y1 y2 y3. x = f y1 y2 y3 ∧ MEM y1 l1 ∧ MEM y2 l2 ∧ MEM y3 l3

⊢ ∀f. MONO3 f ⇒
      ∀lx ly lz e.
        MEM e (MAP3 f lx ly lz) ⇒
        f (MIN_LIST lx) (MIN_LIST ly) (MIN_LIST lz) ≤ e

⊢ ∀f. MONO3 f ⇒
      ∀lx ly lz e.
        MEM e (MAP3 f lx ly lz) ⇒
        e ≤ f (MAX_LIST lx) (MAX_LIST ly) (MAX_LIST lz)

⊢ ∀f. MONO f ⇒ ∀ls e. MEM e (MAP f ls) ⇒ f (MIN_LIST ls) ≤ e

⊢ ∀f. MONO f ⇒ ∀ls e. MEM e (MAP f ls) ⇒ e ≤ f (MAX_LIST ls)

⊢ ∀f. MONO f ⇒ ∀ls. ls ≠ [] ⇒ MIN_LIST (MAP f ls) = f (MIN_LIST ls)

⊢ ∀x. set [x] = {x}

⊢ ∀l c. PAD_LEFT c 0 l = l

⊢ ∀ls c n. PAD_LEFT c n ls = PAD_LEFT c (n − LENGTH ls) [] ⧺ ls

⊢ ∀ls c n. PAD_LEFT c n ls = PAD_RIGHT c (n − LENGTH ls) [] ⧺ ls

⊢ ∀l n. LENGTH l ≤ n ⇒ ∀c. PAD_LEFT c (SUC n) l = c::PAD_LEFT c n l

⊢ ∀l c n. PAD_LEFT c n l = [] ⇔ l = [] ∧ n = 0

⊢ ∀l c n. n ≤ LENGTH l ⇒ PAD_LEFT c n l = l

⊢ ∀l c n. l ≠ [] ⇒ LAST (PAD_LEFT c n l) = LAST l

⊢ ∀n c s. LENGTH (PAD_LEFT c n s) = MAX n (LENGTH s)

⊢ ∀n c. PAD_LEFT c n [] = GENLIST (K c) n

⊢ ∀n c. 0 < n ⇒ PAD_LEFT c n [] = PAD_LEFT c n [c]

⊢ ∀l c. PAD_RIGHT c 0 l = l

⊢ ∀ls c n. PAD_RIGHT c n ls = ls ⧺ PAD_LEFT c (n − LENGTH ls) []

⊢ ∀ls c n. PAD_RIGHT c n ls = ls ⧺ PAD_RIGHT c (n − LENGTH ls) []

⊢ ∀h t c n. h::PAD_RIGHT c n t = PAD_RIGHT c (SUC n) (h::t)

⊢ ∀l c n. PAD_RIGHT c n l = [] ⇔ l = [] ∧ n = 0

⊢ ∀l c n. n ≤ LENGTH l ⇒ PAD_RIGHT c n l = l

⊢ ∀n c s. LENGTH (PAD_RIGHT c n s) = MAX n (LENGTH s)

⊢ ∀n c. PAD_RIGHT c n [] = GENLIST (K c) n

⊢ ∀n c. 0 < n ⇒ PAD_RIGHT c n [] = PAD_RIGHT c n [c]

⊢ ∀l n. LENGTH l ≤ n ⇒ ∀c. PAD_RIGHT c (SUC n) l = SNOC c (PAD_RIGHT c n l)

⊢ ∀ls. EVERY_POSITIVE ls ⇔ POSITIVE ls

⊢ ∀L n. PROD_ACC L n = PROD L * n

⊢ ∀L n. PROD_ACC L n = PROD L * n

⊢ ∀l1 l2. PROD (l1 ⧺ l2) = PROD l1 * PROD l2

⊢ ∀h t. PROD (h::t) = h * PROD t

⊢ ∀n x. PROD (GENLIST (λj. x) n) = x ** n

⊢ ∀l. PROD l = 0 ⇔ MEM 0 l

⊢ ∀m n. PROD (GENLIST (K m) n) = m ** n

⊢ ∀s. FINITE s ⇒ ∀f. Π f s = PROD (MAP f (SET_TO_LIST s))

⊢ ∀ls f. PROD (MAP f ls) = FOLDL (λa e. a * f e) 1 ls

⊢ PROD [] = 1

⊢ ∀l. EVERY_POSITIVE l ⇒ 0 < PROD l

⊢ ∀l. POSITIVE l ⇒ 0 < PROD l

⊢ ∀L. PROD L = PROD_ACC L 1

⊢ ∀n. PROD [n] = n

⊢ ∀x l. PROD (SNOC x l) = PROD l * x

⊢ ∀m n. PROD (GENLIST (λj. n ** 2 ** j) m) = n ** tops 2 m

⊢ ∀ls. PROD ls = 1 ⇔ ∀x. MEM x ls ⇒ x = 1

⊢ ∀ls. PROD ls = if ls = [] then 1 else HD ls * PROD (TL ls)

⊢ ∀a b n.
    SUM (GENLIST a n) + SUM (GENLIST b n) = SUM (GENLIST (λk. a k + b k) n)

⊢ ∀h t. SUM (h::t) = h + SUM t

⊢ ∀n x. SUM (GENLIST (λj. x) n) = n * x

⊢ ∀f n. SUM (GENLIST f (SUC n)) = f 0 + SUM (GENLIST (f ∘ SUC) n)

⊢ ∀f n.
    0 < n ⇒
    SUM (GENLIST f (SUC n)) = f 0 + SUM (GENLIST (f ∘ SUC) (PRE n)) + f n

⊢ ∀f n. SUM (GENLIST f (SUC n)) = SUM (GENLIST f n) + f n

⊢ ∀m n. SUM (GENLIST (λj. n * 2 ** j) m) = n * tops 2 m

⊢ ∀l. SUM l = 0 ⇔ EVERY (λx. x = 0) l

⊢ ∀f n. SUM (GENLIST f n) = ∑ f (count n)

⊢ ∀a b n. SUM (GENLIST a n ⧺ GENLIST b n) = SUM (GENLIST (λk. a k + b k) n)

⊢ ∀m n. SUM (GENLIST (K m) n) = m * n

⊢ ∀n. 0 < n ⇒
      ∀f. SUM (GENLIST ((λk. f k) ∘ SUC) (PRE n)) MOD n =
          SUM (GENLIST ((λk. f k MOD n) ∘ SUC) (PRE n)) MOD n

⊢ ∀f n. SUM (GENLIST (λj. f (n − j)) n) = SUM (MAP f [1 .. n])

⊢ ∀f n. ∑ f (count n) = SUM (MAP f [0 ..< n])

⊢ ∀f n. ∑ f (upto n) = SUM (MAP f [0 .. n])

⊢ ∀l1 l2.
    LENGTH l1 = LENGTH l2 ∧ (∀k. k < LENGTH l1 ⇒ l1❲k❳ ≤ l2❲k❳) ⇒
    SUM l1 ≤ SUM l2

⊢ ∀s m n. SUM s * (m + n) = SUM (MAP ($* m) s) + SUM (MAP ($* n) s)

⊢ ∀l n. n < LENGTH l ⇒ l❲n❳ ≤ SUM l

⊢ ∀l x. MEM x l ⇒ x ≤ SUM l

⊢ ∀l m n. m < n ∧ n < LENGTH l ⇒ l❲m❳ + l❲n❳ ≤ SUM l

⊢ ∀ls. MIN_LIST ls * LENGTH ls ≤ SUM ls

⊢ ∀lx ly c. SUM (MAP2 (λx y. c) lx ly) = c * LENGTH (MAP2 (λx y. c) lx ly)

⊢ ∀f. MONO2 f ⇒
      ∀lx ly.
        SUM (MAP2 f lx ly) ≤
        f (MAX_LIST lx) (MAX_LIST ly) * LENGTH (MAP2 f lx ly)

⊢ ∀lx ly lz c.
    SUM (MAP3 (λx y z. c) lx ly lz) =
    c * LENGTH (MAP3 (λx y z. c) lx ly lz)

⊢ ∀f. MONO3 f ⇒
      ∀lx ly lz.
        SUM (MAP3 f lx ly lz) ≤
        f (MAX_LIST lx) (MAX_LIST ly) (MAX_LIST lz) *
        LENGTH (MAP3 f lx ly lz)

⊢ ∀ls c. SUM (MAP (K c) ls) = c * LENGTH ls

⊢ ∀ls a b. a ≤ b ⇒ SUM (MAP (K a) ls) ≤ SUM (MAP (K b) ls)

⊢ ∀f g ls. EVERY (λx. f x ≤ g x) ls ⇒ SUM (MAP f ls) ≤ SUM (MAP g ls)

⊢ ∀f g ls.
    EVERY (λx. f x < g x) ls ∧ ls ≠ [] ⇒ SUM (MAP f ls) < SUM (MAP g ls)

⊢ ∀f. MONO f ⇒ ∀ls. SUM (MAP f ls) ≤ f (MAX_LIST ls) * LENGTH ls

⊢ ∀n. 0 < n ⇒ ∀l. SUM l MOD n = SUM (MAP (λx. x MOD n) l) MOD n

⊢ ∀f1 f2. (∀x. f1 x ≤ f2 x) ⇒ ∀ls. SUM (MAP f1 ls) ≤ SUM (MAP f2 ls)

⊢ ∀f1 f2.
    (∀x y. f1 x y ≤ f2 x y) ⇒
    ∀lx ly. SUM (MAP2 f1 lx ly) ≤ SUM (MAP2 f2 lx ly)

⊢ ∀f1 f2.
    (∀x y z. f1 x y z ≤ f2 x y z) ⇒
    ∀lx ly lz. SUM (MAP3 f1 lx ly lz) ≤ SUM (MAP3 f2 lx ly lz)

⊢ ∀s k. k * SUM s = SUM (MAP ($* k) s)

⊢ SUM [] = 0

⊢ ∀s m n. (m + n) * SUM s = SUM (MAP ($* m) s) + SUM (MAP ($* n) s)

⊢ ∀n. SUM [n] = n

⊢ ∀ls. SUM ls ≤ MAX_LIST ls * LENGTH ls

⊢ ∀f s t. FINITE t ∧ over f s t ⇒ (SURJ f s t ⇔ CARD (IMAGE f s) = CARD t)

⊢ ∀n. SUM [1 ..< n] = HALF (n * (n − 1))

⊢ ∀n. SUM [1 .. n] = HALF (n * (n + 1))

⊢ ∀n. 0 < n ⇒ 0 arrange n = 0

⊢ ∀n k. n arrange k = (n choose k) * FACT k

⊢ ∀n k. n arrange k = 0 ⇔ n < k

⊢ ∀n k. n arrange k = (n choose k) * perm k

⊢ ∀n k. n arrange k = binomial n k * FACT k

⊢ ∀n k. k ≤ n ⇒ n arrange k = FACT n DIV FACT (n − k)

⊢ ∀n. n arrange 0 = 1

⊢ ∀n. n arrange n = perm n

⊢ ∀n. n arrange n = FACT n

⊢ ∀n. beta 0 n = 0

⊢ ∀n k. 0 < n ∧ 0 < k ⇒ beta n k = leibniz (n − 1) (k − 1)

⊢ ∀m n k. k ≤ m ∧ m ≤ n ⇒ beta n k divides beta m k * binomial n m

⊢ ∀n k. beta n k = 0 ⇔ k = 0 ∨ n < k

⊢ ∀n k. beta (n + 1) (k + 1) = leibniz n k

⊢ beta_horizontal 0 = []

⊢ ∀n. 0 < n ⇒ beta_horizontal n = leibniz_horizontal (n − 1)

⊢ ∀n k. k < n ⇒ (beta_horizontal n)❲k❳ = beta n (k + 1)

⊢ ∀n. beta_horizontal (n + 1) = leibniz_horizontal n

⊢ ∀n. LENGTH (beta_horizontal n) = n

⊢ ∀n k. 0 < k ∧ k ≤ n ⇒ MEM (beta n k) (beta_horizontal n)

⊢ ∀n k. MEM (beta n k) (beta_horizontal n) ⇔ 0 < k ∧ k ≤ n

⊢ ∀n x. MEM x (beta_horizontal n) ⇔ ∃k. 0 < k ∧ k ≤ n ∧ x = beta n k

⊢ ∀n k. n < k ⇒ beta n k = 0

⊢ ∀n. beta n 0 = 0

⊢ ∀n k. 0 < k ∧ k ≤ n ⇒ 0 < beta n k

⊢ ∀n k. k ≤ n ⇒ beta n k = beta n (n − k + 1)

⊢ ∀n. big_lcm (leibniz_col (n + 1)) = big_lcm (leibniz_row n (n + 1))

⊢ ∀f n.
    (∀x. x ∈ count (n + 1) ⇒ 0 < f x) ⇒
    SUM (GENLIST f (n + 1)) ≤ (n + 1) * big_lcm (IMAGE f (count (n + 1)))

⊢ ∀l. big_lcm (set l) = list_lcm l

⊢ ∀s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < x) ⇒ MAX_SET s ≤ big_lcm s

⊢ ∀n. 2 ** n ≤ big_lcm (natural (n + 1))

⊢ ∀n. big_lcm (natural (n + 1)) =
      (n + 1) * big_lcm (IMAGE (binomial n) (count (n + 1)))

⊢ ∀n. big_lcm (natural n) ≤ big_lcm (natural (n + 1))

⊢ ∀n h.
    lcm (leibniz (n + 1) 0) (big_lcm (leibniz_row n h)) =
    big_lcm (leibniz_row (n + 1) (h + 1))

⊢ ∀n k h.
    lcm (leibniz (n + 1) k) (big_lcm (leibniz_seg n k h)) =
    big_lcm (leibniz_seg (n + 1) k (h + 1))

⊢ ∀s t. s =b= t ∧ (FINITE s ∨ FINITE t) ⇒ CARD s = CARD t

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

⊢ ∀s. FINITE s ⇒ s =b= count (CARD s)

⊢ ∀s t. s =b= t ⇒ (s = ∅ ⇔ t = ∅)

⊢ ∀P. (λs t. s =b= t) equiv_on P

⊢ ∀s t. s =b= t ⇒ (FINITE s ⇔ FINITE t)

⊢ ∀s. s =b= s

⊢ ∀s t. s =b= t ⇔ t =b= s

⊢ ∀s t u. s =b= t ∧ t =b= u ⇒ s =b= u

⊢ ∀f s t.
    FINITE s ∧ over f s t ⇒
    (BIJ f s t ⇔ ∀y. y ∈ t ⇒ CARD (preimage f s y) = 1)

⊢ ∀f s t. BIJ f s t ⇔ over f s t ∧ ∀y. y ∈ t ⇒ SING (preimage f s y)

⊢ ∀n. binomial 0 n = if n = 0 then 1 else 0

⊢ ∀n. binomial 1 n = if 1 < n then 0 else 1

⊢ ∀n k.
    binomial n 0 = 1 ∧ binomial 0 (k + 1) = 0 ∧
    binomial (n + 1) (k + 1) = binomial n k + binomial n (k + 1)

⊢ binomial 0 0 = 1 ∧ (∀n. binomial (NUMERAL (BIT1 n)) 0 = 1) ∧
  (∀n. binomial (NUMERAL (BIT2 n)) 0 = 1) ∧
  (∀k. binomial 0 (NUMERAL (BIT1 k)) = 0) ∧
  (∀k. binomial 0 (NUMERAL (BIT2 k)) = 0) ∧
  (∀n k.
     binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT1 k)) =
     binomial (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 k) − 1) +
     binomial (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 k))) ∧
  (∀n k.
     binomial (NUMERAL (BIT2 n)) (NUMERAL (BIT1 k)) =
     binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT1 k) − 1) +
     binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT1 k))) ∧
  (∀n k.
     binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT2 k)) =
     binomial (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 k)) +
     binomial (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT2 k))) ∧
  ∀n k.
    binomial (NUMERAL (BIT2 n)) (NUMERAL (BIT2 k)) =
    binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT1 k)) +
    binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT2 k))

⊢ binomial 0 0 = 1 ∧ (∀n. binomial (SUC n) 0 = 1) ∧
  (∀k. binomial 0 (SUC k) = 0) ∧
  ∀n k. binomial (SUC n) (SUC k) = binomial n k + binomial n (SUC k)

⊢ ∀n k. binomial n k = 0 ⇔ n < k

⊢ ∀n k. k ≤ n ⇒ binomial n k = FACT n DIV (FACT k * FACT (n − k))

⊢ ∀n k. binomial (n + k) k * (FACT n * FACT k) = FACT (n + k)

⊢ ∀n k. k ≤ n ⇒ FACT n = binomial n k * (FACT (n − k) * FACT k)

⊢ ∀n k. k ≤ n ⇒ binomial n k = FACT n DIV (FACT k * FACT (n − k))

⊢ binomial_horizontal 0 = [1]

⊢ ∀n k. k ≤ n ⇒ (binomial_horizontal n)❲k❳ = binomial n k

⊢ ∀n. LENGTH (binomial_horizontal n) = n + 1

⊢ ∀n. MAX_LIST (binomial_horizontal n) = binomial n (HALF n)

⊢ ∀n k. k < n + 1 ⇒ MEM (binomial n k) (binomial_horizontal n)

⊢ ∀n k. MEM (binomial n k) (binomial_horizontal n) ⇔ k ≤ n

⊢ ∀n x. MEM x (binomial_horizontal n) ⇔ ∃k. k ≤ n ∧ x = binomial n k

⊢ ∀n. EVERY_POSITIVE (binomial_horizontal n)

⊢ ∀n x. MEM x (binomial_horizontal n) ⇒ 0 < x

⊢ ∀n. SUM (binomial_horizontal n) = 2 ** n

⊢ ∀f. f = binomial ⇔
      ∀n k.
        f n 0 = 1 ∧ f 0 (k + 1) = 0 ∧
        f (n + 1) (k + 1) = f n k + f n (k + 1)

⊢ ∀P. P 0 0 ∧ (∀n. P (SUC n) 0) ∧ (∀k. P 0 (SUC k)) ∧
      (∀n k. P n k ∧ P n (SUC k) ⇒ P (SUC n) (SUC k)) ⇒
      ∀v v1. P v v1

⊢ ∀n x y.
    (λk. binomial (SUC n) k * x ** (SUC n − k) * y ** k) ∘ SUC =
    (λk. binomial (SUC n) (SUC k) * x ** (n − k) * y ** SUC k)

⊢ ∀n k. k ≤ n ⇒ FACT k * FACT (n − k) divides FACT n

⊢ ∀n k. n < k ⇒ binomial n k = 0

⊢ ∀n k. binomial n k ≤ binomial n (HALF n)

⊢ Stirling ⇒
  ∀n. 0 < n ∧ EVEN n ⇒
      binomial n (HALF n) = 2 ** (n + 1) DIV SQRT (TWICE pi * n)

⊢ ∀n. binomial n (HALF n) ≤ 4 ** HALF n

⊢ ∀n. 0 < n ⇒
      ∀k. binomial n k MOD n = 0 ⇔
          ∀x y. binomial n k * x ** (n − k) * y ** k MOD n = 0

⊢ ∀n. 0 < n ⇒
      ((∀k. 0 < k ∧ k < n ⇒ binomial n k MOD n = 0) ⇔
       ∀x y.
         SUM
           (GENLIST
              ((λk. binomial n k * x ** (n − k) * y ** k MOD n) ∘ SUC)
              (PRE n)) =
         0)

⊢ ∀n k. k < HALF n ⇒ binomial n k < binomial n (k + 1)

⊢ ∀n. binomial n 0 = 1

⊢ ∀n. binomial n 1 = n

⊢ ∀n k. k ≤ n ⇒ binomial n k = FACT n DIV FACT k DIV FACT (n − k)

⊢ ∀n. binomial n n = 1

⊢ ∀n k. k ≤ n ⇒ 0 < binomial n k

⊢ ∀m n k.
    k ≤ m ∧ m ≤ n ⇒
    binomial m k * binomial n m = binomial n k * binomial (n − k) (m − k)

⊢ ∀n. 0 < n ⇒
      ((∀k. 0 < k ∧ k < n ⇒ binomial n k MOD n = 0) ⇔
       ∀h. h < PRE n ⇒ binomial n (SUC h) MOD n = 0)

⊢ ∀n. 0 < n ⇒
      ((∀k. 0 < k ∧ k < n ⇒
            ∀x y. binomial n k * x ** (n − k) * y ** k MOD n = 0) ⇔
       ∀h. h < PRE n ⇒
           ∀x y.
             binomial n (SUC h) * x ** (n − SUC h) * y ** SUC h MOD n = 0)

⊢ ∀n k. binomial (SUC n) (SUC k) = binomial n k + binomial n (SUC k)

⊢ ∀n. 0 < n ⇒ ∀k. binomial n (k + 1) = (n − k) * binomial n k DIV (k + 1)

⊢ ∀n. 0 < n ⇒ ∀k. beta n (k + 1) = (n − k) * binomial n k

⊢ ∀n. MAX_SET (IMAGE (binomial n) (count (n + 1))) = binomial n (HALF n)

⊢ ∀n. SUM (GENLIST (binomial n) (SUC n)) = 2 ** n

⊢ ∀n. SUM (binomial_horizontal n) = 2 ** n

⊢ ∀n k. k ≤ n ⇒ binomial n k = binomial n (n − k)

⊢ ∀n x y.
    (λk. x * k) ∘ (λk. binomial n k * x ** (n − k) * y ** k) =
    (λk. binomial n k * x ** SUC (n − k) * y ** k)

⊢ ∀n x y.
    (λk. y * k) ∘ (λk. binomial n k * x ** (n − k) * y ** k) =
    (λk. binomial n k * x ** (n − k) * y ** SUC k)

⊢ ∀n x y.
    (x + y) ** n =
    SUM (GENLIST (λk. binomial n k * x ** (n − k) * y ** k) (SUC n))

⊢ ∀n x y.
    (x + y) ** n =
    SUM (GENLIST (λk. binomial n k * x ** (n − k) * y ** k) (n + 1))

⊢ ∀p. prime p ⇒ ∀x y. (x + y) ** p MOD p = (x ** p + y ** p) MOD p

⊢ ∀n. 0 < n ⇒ ∀k. binomial (n − 1) k = (n − k) * binomial n k DIV n

⊢ ∀n. 0 < n ⇒ ∀k. n * binomial (n − 1) k = (n − k) * binomial n k

⊢ ∀n. 0 choose n = if n = 0 then 1 else 0

⊢ ∀n. 1 choose n = if 1 < n then 0 else 1

⊢ ∀n k.
    n choose 0 = 1 ∧ 0 choose (k + 1) = 0 ∧
    (n + 1) choose (k + 1) = n choose k + n choose (k + 1)

⊢ ∀n k. n choose k = 0 ⇔ n < k

⊢ ∀n k. n choose k = binomial n k

⊢ ∀n. n choose 0 = 1

⊢ ∀n. n choose 1 = n

⊢ ∀n. n choose n = 1

⊢ ∀n k. (n + 1) choose (k + 1) = n choose k + n choose (k + 1)

⊢ ∀n. SUM (MAP ($choose n) [0 .. n]) = 2 ** n

⊢ ∀n. ∑ ($choose n) (upto n) = 2 ** n

⊢ ∀n. partition (λs t. s =b= t) (POW (count n)) =
      IMAGE (sub_count n) (upto n)

⊢ DATATYPE (record triple a b c)

⊢ ∀n. 1 < n ∧ (∀k. 0 < k ∧ k < n ⇒ n divides binomial n k) ⇒ prime n

⊢ ∀s. feq set equiv_on s

⊢ ∀f s t.
    FINITE s ∧ SURJ f s t ⇒
    (INJ f s t ⇔ ∀e. e ∈ IMAGE (preimage f s) t ⇒ CARD e = 1)

⊢ ∀p m n. prime p ∧ m divides n ∧ ¬(p * m divides n) ⇒ gcd (p * m) n = m

⊢ ∀t n. 1 < t ⇒ SUM (MAP (λj. t ** j) [0 ..< n]) = tops t n DIV (t − 1)

⊢ ∀t n.
    1 < t ⇒ SUM (MAP (λj. t ** j) [0 .. n]) = tops t (n + 1) DIV (t − 1)

⊢ ∀ls. ls ≠ [] ⇒ HD (turn ls) = LAST ls

⊢ ∀ls n.
    n < LENGTH ls ⇒
    HD (turn_exp ls n) = ls❲if n = 0 then 0 else LENGTH ls − n❳

⊢ ∀f s t.
    FINITE s ∧ over f s t ⇒
    (INJ f s t ⇔ ∀y. y ∈ t ⇒ CARD (preimage f s y) ≤ 1)

⊢ ∀f s t.
    INJ f s t ⇔
    over f s t ∧ ∀y. y ∈ t ⇒ preimage f s y = ∅ ∨ SING (preimage f s y)

⊢ ∀ls x. x interleave ls = {TAKE k ls ⧺ x::DROP k ls | k | k ≤ LENGTH ls}

⊢ ∀ls x. ¬MEM x ls ⇒ CARD (x interleave ls) = 1 + LENGTH ls

⊢ ∀ls x.
    ¬MEM x ls ⇒
    INJ (λk. TAKE k ls ⧺ x::DROP k ls) (upto (LENGTH ls)) 𝕌(:α list)

⊢ ∀l1 l2 x.
    ¬MEM x l1 ∧ l1 ≠ l2 ⇒ DISJOINT (x interleave l1) (x interleave l2)

⊢ ∀ls x y. ALL_DISTINCT (x::ls) ∧ y ∈ x interleave ls ⇒ ALL_DISTINCT y

⊢ ∀ls x y.
    ALL_DISTINCT ls ∧ ¬MEM x ls ∧ y ∈ x interleave ls ⇒ ALL_DISTINCT y

⊢ ∀ls x y.
    y ∈ x interleave ls ⇔ ∃k. k ≤ LENGTH ls ∧ y = TAKE k ls ⧺ x::DROP k ls

⊢ ∀n x y. ¬MEM n x ∧ ¬MEM n y ⇒ (n interleave x = n interleave y ⇔ x = y)

⊢ ∀ls x. FINITE (x interleave ls)

⊢ ∀ls x. x::ls ∈ x interleave ls

⊢ ∀ls x y. y ∈ x interleave ls ⇒ LENGTH y = 1 + LENGTH ls

⊢ ∀x. x interleave [] = {[x]}

⊢ ∀ls x. x interleave ls ≠ ∅

⊢ ∀ls h.
    ALL_DISTINCT ls ∧ MEM h ls ⇒
    ∃t. ALL_DISTINCT t ∧ ls ∈ h interleave t ∧ set t = set ls DELETE h

⊢ ∀ls n.
    ALL_DISTINCT ls ∧ set ls = upto n ⇒
    ∃t. ALL_DISTINCT t ∧ ls ∈ n interleave t ∧ set t = count n

⊢ ∀ls x y. y ∈ x interleave ls ⇒ set y = set (x::ls)

⊢ ∀ls x y. y ∈ x interleave ls ⇒ set y = x INSERT set ls

⊢ ∀n. 2 ** n ≤ lcm_run (n + 1)

⊢ ∀n. (n + 1) * binomial n (HALF n) ≤ big_lcm (natural (n + 1))

⊢ Stirling ∧ (∀n c. n DIV SQRT (c * (n − 1)) = SQRT (n DIV c)) ⇒
  ∀n. ODD n ⇒ SQRT (n DIV TWICE pi) * 2 ** n ≤ big_lcm (natural n)

⊢ ∀n. (n + 1) * binomial n (HALF n) ≤ lcm_run (n + 1)

⊢ Stirling ∧ (∀n c. n DIV SQRT (c * (n − 1)) = SQRT (n DIV c)) ⇒
  ∀n. ODD n ⇒ SQRT (n DIV TWICE pi) * 2 ** n ≤ lcm_run n

⊢ ∀p m n.
    prime p ∧ m divides n ∧ ¬(p * m divides n) ⇒ lcm (p * m) n = p * n

⊢ lcm_run 0 = 1

⊢ lcm_run 1 = 1

⊢ ∀n. lcm_run n = lcm_run (n − 1 + 1)

⊢ ∀n k. 0 < k ∧ k ≤ n ⇒ beta n k divides lcm_run n

⊢ ∀m n. n ≤ TWICE m ∧ m ≤ n ⇒ lcm_run n ≤ lcm_run m * binomial n m

⊢ ∀n. lcm_run n = FOLDL lcm 1 [1 .. n]

⊢ ∀n. lcm_run n = FOLDR lcm 1 [1 .. n]

⊢ ∀n. 0 < n ⇒ lcm_run n = list_lcm (beta_horizontal n)

⊢ ∀m n. n ≤ TWICE m ∧ m ≤ n ⇒ lcm_run n divides lcm_run m * binomial n m

⊢ ∀m n. n ≤ TWICE m ∧ m ≤ n ⇒ lcm_run n divides binomial n m * lcm_run m

⊢ ∀n. n + 1 divides lcm_run (n + 1) ∧ lcm_run n divides lcm_run (n + 1)

⊢ ∀n. EVEN n ⇒ HALF (n − 2) * HALF (HALF (2 ** n)) ≤ lcm_run n

⊢ ∀n. EVEN n ∧ 8 ≤ n ⇒ 2 ** n ≤ lcm_run n

⊢ ∀n k. k ≤ n ⇒ leibniz n k divides lcm_run (n + 1)

⊢ ∀n. 2 ** n ≤ lcm_run (n + 1)

⊢ ∀n. 7 ≤ n ⇒ 2 ** n ≤ lcm_run n

⊢ ∀n. 2 ** n ≤ lcm_run n ⇔ n = 0 ∨ n = 5 ∨ 7 ≤ n

⊢ ∀n. n * 4 ** n ≤ lcm_run (TWICE (n + 1))

⊢ ∀n. EVEN n ⇒ (2 ** n ≤ lcm_run n ⇔ n = 0 ∨ 8 ≤ n)

⊢ ∀n. 2 ** (n − 1) ≤ lcm_run n

⊢ ∀n. n * 4 ** n ≤ lcm_run (TWICE n + 1)

⊢ ∀n. ODD n ⇒ (2 ** n ≤ lcm_run n ⇔ 5 ≤ n)

⊢ ∀n. HALF (n + 1) ≤ lcm_run n

⊢ ∀n. lcm_run n ≤ lcm_run (n + 1)

⊢ ∀n. 0 < n ⇒ n * leibniz (TWICE n) n divides lcm_run (TWICE n + 1)

⊢ ∀n. ODD n ⇒ HALF n * HALF (2 ** n) ≤ lcm_run n

⊢ ∀n. ODD n ∧ 5 ≤ n ⇒ 2 ** n ≤ lcm_run n

⊢ ∀n. 0 < lcm_run n

⊢ lcm_run 2 = 2 ∧ lcm_run 3 = 6 ∧ lcm_run 4 = 12 ∧ lcm_run 5 = 60 ∧
  lcm_run 6 = 60 ∧ lcm_run 7 = 420 ∧ lcm_run 8 = 840 ∧ lcm_run 9 = 2520

⊢ ∀n. lcm_run (n + 1) = lcm (n + 1) (lcm_run n)

⊢ ∀n. lcm_run n ≤ 4 ** n

⊢ lcm_upto 0 = 1

⊢ lcm_upto 1 = 1

⊢ ∀n. lcm_upto (SUC n) = lcm (SUC n) (lcm_upto n)

⊢ lcm_upto 0 = 1 ∧ ∀n. lcm_upto (n + 1) = lcm (n + 1) (lcm_upto n)

⊢ lcm_upto 0 = 1 ∧
  (∀n. lcm_upto (NUMERAL (BIT1 n)) =
       lcm (NUMERAL (BIT1 n)) (lcm_upto (NUMERAL (BIT1 n) − 1))) ∧
  ∀n. lcm_upto (NUMERAL (BIT2 n)) =
      lcm (NUMERAL (BIT2 n)) (lcm_upto (NUMERAL (BIT1 n)))

⊢ ∀n. n + 1 divides lcm_upto (n + 1) ∧ lcm_upto n divides lcm_upto (n + 1)

⊢ ∀n. lcm_upto n = lcm_run n

⊢ ∀n k. k ≤ n ⇒ leibniz n k divides lcm_upto (n + 1)

⊢ ∀n. 2 ** n ≤ lcm_upto (n + 1)

⊢ ∀n. 7 ≤ n ⇒ 2 ** n ≤ lcm_upto n

⊢ ∀n. n * 4 ** n ≤ lcm_upto (TWICE (n + 1))

⊢ ∀n. n * 4 ** n ≤ lcm_upto (TWICE n + 1)

⊢ ∀n. lcm_upto n ≤ lcm_upto (n + 1)

⊢ ∀n. 0 < lcm_upto (n + 1)

⊢ lcm_upto 2 = 2 ∧ lcm_upto 3 = 6 ∧ lcm_upto 4 = 12 ∧ lcm_upto 5 = 60 ∧
  lcm_upto 6 = 60 ∧ lcm_upto 7 = 420 ∧ lcm_upto 8 = 840 ∧
  lcm_upto 9 = 2520 ∧ lcm_upto 10 = 2520

⊢ ∀n. leibniz 0 n = if n = 0 then 1 else 0

⊢ ∀n. leibniz n = (λj. (n + 1) * j) ∘ binomial n

⊢ ∀m n k.
    k ≤ m ∧ m ≤ n ⇒
    leibniz n k * binomial (n − k) (m − k) =
    leibniz m k * binomial (n + 1) (m + 1)

⊢ ∀a b. leibniz_col_arm a b 0 = []

⊢ ∀a b. leibniz_col_arm a b 1 = [leibniz a b]

⊢ ∀a b n.
    leibniz_col_arm (a + 1) b (n + 1) =
    leibniz (a + 1) b::leibniz_col_arm a b n

⊢ ∀n k. k < n ⇒ ∀a b. (leibniz_col_arm a b n)❲k❳ = leibniz (a − k) b

⊢ ∀a b n. LENGTH (leibniz_col_arm a b n) = n

⊢ ∀n. leibniz_col_arm n 0 (n + 1) = leibniz_up n

⊢ ∀a b n.
    b ≤ a ∧ n ≤ a + 1 − b ⇒
    leibniz_col_arm a b n wriggle leibniz_seg_arm a b n

⊢ ∀h. leibniz_col h = {leibniz j 0 | j ∈ count h}

⊢ ∀n. leibniz_col n = natural n

⊢ ∀n k. leibniz n k = (λj. (n + 1) * j) (binomial n k)

⊢ ∀m n k.
    k ≤ m ∧ m ≤ n ⇒
    leibniz n k divides leibniz m k * binomial (n + 1) (m + 1)

⊢ ∀n k. leibniz n k = 0 ⇔ n < k

⊢ ∀n k. leibniz n k = (n + 1 − k) * binomial (n + 1) k

⊢ ∀n k. k ≤ n ⇒ leibniz n k = (n + 1) * FACT n DIV (FACT k * FACT (n − k))

⊢ leibniz_horizontal 0 = [1]

⊢ ∀n. leibniz_horizontal n = MAP (λj. (n + 1) * j) (binomial_horizontal n)

⊢ ∀n. SUM (leibniz_horizontal n) DIV LENGTH (leibniz_horizontal n) =
      SUM (binomial_horizontal n)

⊢ ∀n. SUM (leibniz_horizontal n) DIV LENGTH (leibniz_horizontal n) = 2 ** n

⊢ ∀n k. k ≤ n ⇒ leibniz n k divides list_lcm (leibniz_horizontal n)

⊢ ∀n k. k ≤ n ⇒ (leibniz_horizontal n)❲k❳ = leibniz n k

⊢ ∀n k. k ≤ n ⇒ (leibniz_horizontal n)❲k❳ = leibniz n k

⊢ ∀n. TAKE 1 (leibniz_horizontal (n + 1)) = [n + 2]

⊢ ∀n. list_lcm (leibniz_horizontal n) =
      (n + 1) * list_lcm (binomial_horizontal n)

⊢ ∀n. 2 ** n ≤ list_lcm (leibniz_horizontal n)

⊢ ∀n. LENGTH (leibniz_horizontal n) = n + 1

⊢ ∀n k. k ≤ n ⇒ MEM (leibniz n k) (leibniz_horizontal n)

⊢ ∀n k. MEM (leibniz n k) (leibniz_horizontal n) ⇔ k ≤ n

⊢ ∀n x. MEM x (leibniz_horizontal n) ⇔ ∃k. k ≤ n ∧ x = leibniz n k

⊢ ∀m n x.
    n ≤ TWICE m + 1 ∧ m ≤ n ∧ MEM x (leibniz_horizontal n) ⇒
    x divides list_lcm (leibniz_horizontal m) * binomial (n + 1) (m + 1)

⊢ ∀n. EVERY_POSITIVE (leibniz_horizontal n)

⊢ ∀n x. MEM x (leibniz_horizontal n) ⇒ 0 < x

⊢ ∀n. SUM (leibniz_horizontal n) = (n + 1) * SUM (binomial_horizontal n)

⊢ ∀n. SUM (leibniz_horizontal n) = (n + 1) * 2 ** n

⊢ ∀n. [leibniz (n + 1) 0] ⧺ leibniz_horizontal n wriggle
      leibniz_horizontal (n + 1)

⊢ ∀n k.
    k ≤ n + 1 ⇒
    TAKE (k + 1) (leibniz_horizontal (n + 1)) ⧺
    DROP k (leibniz_horizontal n) wriggle leibniz_horizontal (n + 1)

⊢ ∀n k.
    k ≤ n ⇒
    TAKE (k + 1) (leibniz_horizontal (n + 1)) ⧺
    DROP k (leibniz_horizontal n) zigzag
    TAKE (k + 2) (leibniz_horizontal (n + 1)) ⧺
    DROP (k + 1) (leibniz_horizontal n)

⊢ ∀n. 0 < n ⇒
      ∀k. lcm (leibniz n k) (leibniz (n − 1) k) =
          lcm (leibniz n k) (leibniz n (k + 1))

⊢ ∀a b n.
    b ≤ a ∧ n ≤ a + 1 − b ⇒
    list_lcm (leibniz_col_arm a b n) = list_lcm (leibniz_seg_arm a b n)

⊢ ∀n. lcm_run (n + 1) = list_lcm (leibniz_horizontal n)

⊢ ∀n k. n < k ⇒ leibniz n k = 0

⊢ ∀n. 4 ** n ≤ leibniz (TWICE n) n

⊢ ∀n k. k < HALF n ⇒ leibniz n k < leibniz n (k + 1)

⊢ ∀n. leibniz n 0 = n + 1

⊢ ∀n k.
    0 < k ∧ k ≤ n ⇒
    leibniz n k =
    leibniz n (k − 1) * leibniz (n − 1) (k − 1) DIV
    (leibniz n (k − 1) − leibniz (n − 1) (k − 1))

⊢ ∀n. leibniz n n = n + 1

⊢ ∀n k. k ≤ n ⇒ 0 < leibniz n k

⊢ ∀n. 0 < n ⇒
      ∀k. leibniz n k * leibniz (n − 1) k =
          leibniz n (k + 1) * (leibniz n k − leibniz (n − 1) k)

⊢ ∀n. 0 < n ⇒
      ∀k. k < n ⇒
          leibniz n (k + 1) =
          leibniz n k * leibniz (n − 1) k DIV
          (leibniz n k − leibniz (n − 1) k)

⊢ ∀n. 0 < n ⇒ ∀k. leibniz n (k + 1) = (n − k) * leibniz n k DIV (k + 1)

⊢ ∀n k. leibniz n (k + 1) = (n − k) * binomial (n + 1) (k + 1)

⊢ ∀n k. (k + 1) * tc = (n + 1 − k) * tb

⊢ ∀n. 0 < n ⇒ ∀k. (k + 1) * leibniz n (k + 1) = (n − k) * leibniz n k

⊢ ∀n h. leibniz_row n h = {leibniz n j | j ∈ count h}

⊢ ∀a b. leibniz_seg_arm a b 0 = []

⊢ ∀a b. leibniz_seg_arm a b 1 = [leibniz a b]

⊢ ∀n k. k < n ⇒ ∀a b. (leibniz_seg_arm a b n)❲k❳ = leibniz a (b + k)

⊢ ∀a b n. TAKE 1 (leibniz_seg_arm a b (n + 1)) = [leibniz a b]

⊢ ∀a b n. LENGTH (leibniz_seg_arm a b n) = n

⊢ ∀n. leibniz_seg_arm n 0 (n + 1) = leibniz_horizontal n

⊢ ∀a b n.
    [leibniz (a + 1) b] ⧺ leibniz_seg_arm a b n wriggle
    leibniz_seg_arm (a + 1) b (n + 1)

⊢ ∀n k.
    k < n + 1 ⇒
    ∀a b.
      TAKE (k + 1) (leibniz_seg_arm (a + 1) b (n + 1)) ⧺
      DROP k (leibniz_seg_arm a b n) wriggle
      leibniz_seg_arm (a + 1) b (n + 1)

⊢ ∀n k.
    k < n ⇒
    ∀a b.
      TAKE (k + 1) (leibniz_seg_arm (a + 1) b (n + 1)) ⧺
      DROP k (leibniz_seg_arm a b n) zigzag
      TAKE (k + 2) (leibniz_seg_arm (a + 1) b (n + 1)) ⧺
      DROP (k + 1) (leibniz_seg_arm a b n)

⊢ ∀n k h. leibniz_seg n k h = {leibniz n (k + j) | j ∈ count h}

⊢ ∀n k. k ≤ n ⇒ leibniz n k = leibniz n (n − k)

⊢ leibniz_up 1 zigzag leibniz_horizontal 1

⊢ ∀n k. lcm tb ta = lcm tb tc

⊢ ∀n k.
    ta = leibniz n k ∧ tb = leibniz (n + 1) k ∧
    tc = leibniz (n + 1) (k + 1)

⊢ ∀n' k. ta * tb = tc * (tb − ta)

⊢ ∀n. 0 < n ⇒ ∀k. leibniz (n − 1) k = (n − k) * leibniz n k DIV (n + 1)

⊢ leibniz_up 0 = [1]

⊢ ∀n. 0 < n ⇒ ∀k. leibniz (n − 1) k = (n − k) * binomial n k

⊢ ∀n. leibniz_up (n + 1) = n + 2::leibniz_up n

⊢ ∀n k. (n + 2) * ta = (n + 1 − k) * tb

⊢ ∀n. 0 < n ⇒ ∀k. (n + 1) * leibniz (n − 1) k = (n − k) * leibniz n k

⊢ ∀n. list_lcm (leibniz_up n) = list_lcm (leibniz_horizontal n)

⊢ ∀n. LENGTH (leibniz_up n) = n + 1

⊢ ∀n x. 0 < x ∧ x ≤ n + 1 ⇔ MEM x (leibniz_up n)

⊢ ∀n. EVERY_POSITIVE (leibniz_up n)

⊢ ∀n. leibniz_up n wriggle leibniz_horizontal n

⊢ ∀n. leibniz_up n wriggle leibniz_horizontal n

⊢ leibniz_vertical 0 = [1]

⊢ ∀n. leibniz_vertical n = GENLIST (λi. 1 + i) (n + 1)

⊢ ∀n k. k ≤ n ⇒ leibniz n k divides lcm_run (n + 1)

⊢ ∀n. 2 ** n ≤ lcm_run (n + 1)

⊢ ∀n. LENGTH (leibniz_vertical n) = n + 1

⊢ ∀n x. 0 < x ∧ x ≤ n + 1 ⇔ MEM x (leibniz_vertical n)

⊢ ∀n. leibniz_vertical n ≠ []

⊢ ∀n. EVERY_POSITIVE (leibniz_vertical n)

⊢ ∀n x. MEM x (leibniz_vertical n) ⇒ 0 < x

⊢ ∀n. leibniz_vertical (n + 1) = SNOC (n + 2) (leibniz_vertical n)

⊢ ∀p1. p1 wriggle p1

⊢ ∀p1 p2. p1 wriggle p2 ⇒ ∀x. [x] ⧺ p1 wriggle [x] ⧺ p2

⊢ ∀p1 p2 p3. p1 wriggle p2 ∧ p2 wriggle p3 ⇒ p1 wriggle p3

⊢ ∀p1 p2. p1 zigzag p2 ⇒ ∀x. [x] ⧺ p1 zigzag [x] ⧺ p2

⊢ ∀p1 p2. p1 zigzag p2 ⇒ p1 wriggle p2

⊢ ∀m n m' n'. m' ≤ n' ∧ n' < LENGTH [m .. n] ⇒ [m .. n]❲m'❳ ≤ [m .. n]❲n'❳

⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ PROD [m .. n] = PROD [1 .. n] DIV PROD [1 .. m − 1]

⊢ ∀m n. 0 < m ⇒ 0 < PROD [m .. n]

⊢ ∀m n m' n'.
    m' ≤ n' ∧ n' < LENGTH [m ..< n] ⇒ [m ..< n]❲m'❳ ≤ [m ..< n]❲n'❳

⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ PROD [m ..< n] = PROD [1 ..< n] DIV PROD [1 ..< m]

⊢ ∀m n. 0 < m ⇒ 0 < PROD [m ..< n]

⊢ ∀n. 0 < n ⇒ list_count 0 n = ∅

⊢ ∀n k.
    list_count n k =
    {ls | ALL_DISTINCT ls ∧ set ls ⊆ count n ∧ CARD (set ls) = k}

⊢ ∀n k.
    0 < k ⇒
    list_count n k =
    IMAGE (λls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE
    []

⊢ ∀ls n k.
    ls ∈ list_count n k ⇔
    ALL_DISTINCT ls ∧ set ls ⊆ count n ∧ LENGTH ls = k

⊢ ∀ls n k.
    ls ∈ list_count n k ⇔
    ALL_DISTINCT ls ∧ set ls ⊆ count n ∧ CARD (set ls) = k

⊢ ∀ls n k. ls ∈ list_count n k ⇒ perm_set (set ls) ≠ ∅

⊢ ∀ls n k. ls ∈ list_count n k ⇒ CARD (set ls) = k

⊢ ∀n k. list_count n k = ∅ ⇔ n < k

⊢ ∀n k.
    list_count n k =
    if k = 0 then {[]}
    else
      IMAGE (λls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE
      []

⊢ ∀n k. FINITE (list_count n k)

⊢ ∀n. list_count n 0 = {[]}

⊢ ∀n. list_count n n = perm_count n

⊢ ∀ls n k.
    ls ∈ list_count n k ⇒
    equiv_class (feq set) (list_count n k) ls = perm_set (set ls)

⊢ ∀ls n k.
    ls ∈ list_count n k ⇒
    CARD (equiv_class (feq set) (list_count n k) ls) = perm k

⊢ ∀n k.
    BIJ (set ∘ CHOICE) (partition (feq set) (list_count n k))
      (sub_count n k)

⊢ ∀s n k.
    s ∈ partition (feq set) (list_count n k) ⇒
    (set ∘ CHOICE) s ∈ sub_count n k

⊢ ∀n k.
    INJ (set ∘ CHOICE) (partition (feq set) (list_count n k))
      (sub_count n k)

⊢ ∀n k.
    SURJ (set ∘ CHOICE) (partition (feq set) (list_count n k))
      (sub_count n k)

⊢ ∀n k e. e ∈ partition (feq set) (list_count n k) ⇒ CARD e = perm k

⊢ ∀n k. list_count n k ⊆ necklace k n

⊢ ∀x l. MEM x l ⇒ list_lcm (x::l) = list_lcm l

⊢ ∀l1 l2. list_lcm (l1 ⧺ l2) = lcm (list_lcm l1) (list_lcm l2)

⊢ ∀l1 l2 l3.
    list_lcm (l1 ⧺ l2 ⧺ l3) =
    list_lcm [list_lcm l1; list_lcm l2; list_lcm l3]

⊢ ∀ls. list_lcm ls = FOLDL lcm 1 ls

⊢ ∀ls. list_lcm ls = FOLDR lcm 1 ls

⊢ ∀h t. list_lcm (h::t) = lcm h (list_lcm t)

⊢ ∀l x y. MEM x l ∧ MEM y l ⇒ lcm x y divides list_lcm l

⊢ ∀l1 l2. set l1 = set l2 ⇒ list_lcm l1 = list_lcm l2

⊢ ∀l. POSITIVE l ⇒ MAX_LIST l ≤ list_lcm l

⊢ ∀x l. MEM x l ⇒ x divides list_lcm l

⊢ ∀l m. (∀x. MEM x l ⇒ x divides m) ⇒ list_lcm l divides m

⊢ ∀l. EVERY_POSITIVE l ⇒ SUM l ≤ LENGTH l * list_lcm l

⊢ ∀l. POSITIVE l ⇒ SUM l ≤ LENGTH l * list_lcm l

⊢ ∀l x y. POSITIVE l ∧ MEM x l ∧ MEM y l ⇒ lcm x y ≤ list_lcm l

⊢ ∀n l. list_lcm (MAP (λk. n * k) l) = if l = [] then 1 else n * list_lcm l

⊢ list_lcm [] = 1

⊢ ∀l. l ≠ [] ∧ EVERY_POSITIVE l ⇒ SUM l DIV LENGTH l ≤ list_lcm l

⊢ ∀l. l ≠ [] ∧ POSITIVE l ⇒ SUM l DIV LENGTH l ≤ list_lcm l

⊢ ∀l. list_lcm (nub l) = list_lcm l

⊢ ∀l1 l2. set l1 = set l2 ⇒ list_lcm (nub l1) = list_lcm (nub l2)

⊢ ∀l. EVERY_POSITIVE l ⇒ 0 < list_lcm l

⊢ ∀l. POSITIVE l ⇒ 0 < list_lcm l

⊢ ∀p l. prime p ∧ p divides list_lcm l ⇒ p divides PROD_SET (set l)

⊢ ∀p l. prime p ∧ p divides list_lcm l ⇒ ∃x. MEM x l ∧ p divides x

⊢ ∀l. list_lcm (REVERSE l) = list_lcm l

⊢ ∀x. list_lcm [x] = x

⊢ ∀x l. list_lcm (SNOC x l) = lcm x (list_lcm l)

⊢ ∀n. lcm_run (n + 1) = lcm (n + 1) (lcm_run n)

⊢ ∀l m. 0 < m ∧ (∀x. MEM x l ⇒ x divides m) ⇒ list_lcm l ≤ m

⊢ ∀p1 p2. p1 wriggle p2 ⇒ list_lcm p1 = list_lcm p2

⊢ ∀p1 p2. p1 zigzag p2 ⇒ list_lcm p1 = list_lcm p2

⊢ ∀ls. EVERY_POSITIVE ls ∧ LENGTH ls = SUM ls ⇒ EVERY (λx. x = 1) ls

⊢ ∀ls. EVERY_POSITIVE ls ⇒ LENGTH ls ≤ SUM ls

⊢ ∀p l. prime p ∧ p divides PROD_SET (set l) ⇒ ∃x. MEM x l ∧ p divides x

⊢ ∀a. monocoloured 0 a = {[]}

⊢ ∀a. CARD (monocoloured 0 a) = 1

⊢ ∀a. monocoloured 1 a = necklace 1 a

⊢ ∀n a. 0 < n ⇒ CARD (monocoloured n a) = a

⊢ ∀n a. CARD (monocoloured n a) = if n = 0 then 1 else a

⊢ ∀n a ls.
    ls ∈ monocoloured n a ⇔ ls ∈ necklace n a ∧ (ls ≠ [] ⇒ SING (set ls))

⊢ ∀n. 0 < n ⇒ monocoloured n 0 = ∅

⊢ ∀n a.
    monocoloured n a =
    if n = 0 then {[]} else IMAGE (λc. GENLIST (K c) n) (count a)

⊢ ∀n a. FINITE (monocoloured n a)

⊢ ∀n. monocoloured n 1 = necklace n 1

⊢ ∀n a ls. ls ∈ monocoloured n a ⇒ ls ∈ necklace n a

⊢ ∀n a. monocoloured n a ⊆ necklace n a

⊢ ∀n a.
    0 < n ⇒
    monocoloured (SUC n) a = IMAGE (λls. HD ls::ls) (monocoloured n a)

⊢ ∀n a. DISJOINT (multicoloured n a) (monocoloured n a)

⊢ ∀n a. necklace n a = multicoloured n a ∪ monocoloured n a

⊢ ∀a. multicoloured 0 a = ∅

⊢ ∀a. multicoloured 1 a = ∅

⊢ ∀n a. 0 < n ⇒ CARD (multicoloured n a) = a ** n − a

⊢ ∀n a. CARD (multicoloured n a) = if n = 0 then 0 else a ** n − a

⊢ ∀n a ls.
    ls ∈ multicoloured n a ⇔ ls ∈ necklace n a ∧ ls ≠ [] ∧ ¬SING (set ls)

⊢ ∀n. multicoloured n 0 = ∅ ∧ multicoloured n 1 = ∅

⊢ ∀n a. FINITE (multicoloured n a)

⊢ ∀n. multicoloured n 0 = ∅

⊢ ∀n. multicoloured n 1 = ∅

⊢ ∀n a ls. ls ∈ multicoloured n a ⇒ ls ∈ necklace n a

⊢ ∀n a. 1 < n ∧ 1 < a ⇒ multicoloured n a ≠ ∅

⊢ ∀n a ls. ls ∈ multicoloured n a ⇒ ls ∉ monocoloured n a

⊢ ∀n a ls.
    ls ∈ necklace n a ⇒ (ls ∈ multicoloured n a ⇔ ls ∉ monocoloured n a)

⊢ ∀n a ls.
    ls ∈ necklace n a ⇒ ls ∈ multicoloured n a ∨ ls ∈ monocoloured n a

⊢ ∀n a. multicoloured n a ⊆ necklace n a

⊢ ∀a. necklace 0 a = {[]}

⊢ ∀a. necklace 1 a = {[e] | e ∈ count a}

⊢ ∀a. necklace 1 a = monocoloured 1 a

⊢ ∀n a. CARD (necklace n a) = a ** n

⊢ ∀n a ls. ls ∈ necklace n a ⇒ set ls ⊆ count a

⊢ ∀n a ls. ls ∈ necklace n a ⇔ LENGTH ls = n ∧ set ls ⊆ count a

⊢ ∀n. 0 < n ⇒ necklace n 0 = ∅

⊢ ∀n a.
    necklace n a =
    if n = 0 then {[]}
    else IMAGE (λ(c,ls). c::ls) (count a × necklace (n − 1) a)

⊢ ∀n a. FINITE (necklace n a)

⊢ ∀n a ls. ls ∈ necklace n a ⇒ LENGTH ls = n

⊢ ∀n a ls. 0 < n ∧ ls ∈ necklace n a ⇒ ls ≠ []

⊢ ∀n a ls. ls ∈ necklace n a ⇒ LENGTH ls = n ∧ set ls ⊆ count a

⊢ ∀n a.
    necklace (SUC n) a = IMAGE (λ(c,ls). c::ls) (count a × necklace n a)

⊢ ∀l. ALL_DISTINCT (nub l)

⊢ ∀x l. nub (x::l) = if MEM x l then nub l else x::nub l

⊢ nub [] = []

⊢ ∀x. nub [x] = [x]

⊢ ∀f s t. BIJ f s t ⇒ over f s t

⊢ ∀f s t. INJ f s t ⇒ over f s t

⊢ ∀f s t. SURJ f s t ⇒ over f s t

⊢ ∀s m.
    FINITE s ∧ PAIRWISE_COPRIME s ∧ (∀x. x ∈ s ⇒ x divides m) ⇒
    PROD_SET s divides m

⊢ ∀s. FINITE s ∧ PAIRWISE_COPRIME s ⇒ set_lcm s = PROD_SET s

⊢ perm 0 = 1

⊢ perm 1 = 1

⊢ perm 0 = 1 ∧ ∀n. perm (n + 1) = (n + 1) * perm n

⊢ perm_count 0 = {[]}

⊢ perm_count 1 = {[0]}

⊢ ∀ls n. ls ∈ perm_count n ⇔ ALL_DISTINCT ls ∧ set ls = count n

⊢ ∀ls n. ls ∈ perm_count n ⇒ LENGTH ls = n

⊢ ∀ls n. ls ∈ perm_count n ⇒ ¬MEM n ls

⊢ ∀n. perm_count n =
      if n = 0 then {[]}
      else BIGUNION (IMAGE ($interleave (n − 1)) (perm_count (n − 1)))

⊢ ∀n. FINITE (perm_count n)

⊢ ∀n e. e ∈ IMAGE ($interleave n) (perm_count n) ⇒ CARD e = n + 1

⊢ ∀n e s t.
    s ∈ IMAGE ($interleave n) (perm_count n) ∧
    t ∈ IMAGE ($interleave n) (perm_count n) ∧ s ≠ t ⇒
    DISJOINT s t

⊢ ∀n e. e ∈ IMAGE ($interleave n) (perm_count n) ⇒ FINITE e

⊢ ∀n. INJ ($interleave n) (perm_count n) 𝕌(:num list -> bool)

⊢ ∀n. perm_count n ⊆ necklace n n

⊢ ∀n. perm_count (SUC n) = BIGUNION (IMAGE ($interleave n) (perm_count n))

⊢ ∀n. perm_count (n + 1) = BIGUNION (IMAGE ($interleave n) (perm_count n))

⊢ ∀n. perm n = FACT n

⊢ ∀s. FINITE s ⇒ perm_set s =b= perm_count (CARD s)

⊢ ∀s. FINITE s ⇒ CARD (perm_set s) = perm (CARD s)

⊢ ∀s. FINITE s ⇒ CARD (perm_set s) = FACT (CARD s)

⊢ ∀ls s. ls ∈ perm_set s ⇔ ALL_DISTINCT ls ∧ set ls = s

⊢ perm_set ∅ = {[]}

⊢ ∀s. perm_set s = {[]} ⇔ s = ∅

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

⊢ ∀s. FINITE s ⇒ SET_TO_LIST s ∈ perm_set s

⊢ ∀ls. perm_set (set ls) ≠ ∅

⊢ ∀f s n. BIJ f s (count n) ⇒ BIJ (MAP f) (perm_set s) (perm_count n)

⊢ ∀ls f s n. ls ∈ perm_set s ∧ BIJ f s (count n) ⇒ MAP f ls ∈ perm_count n

⊢ ∀f s n. BIJ f s (count n) ⇒ INJ (MAP f) (perm_set s) (perm_count n)

⊢ ∀f s n. BIJ f s (count n) ⇒ SURJ (MAP f) (perm_set s) (perm_count n)

⊢ ∀s. FINITE s ⇒ perm_set s ≠ ∅

⊢ ∀n. perm_set (count n) = perm_count n

⊢ ∀x. perm_set {x} = {[x]}

⊢ ∀n. perm (SUC n) = SUC n * perm n

⊢ ∀n. perm (n + 1) = (n + 1) * perm n

⊢ ∀t n. tops t n = (t − 1) * SUM (MAP (λj. t ** j) [0 ..< n])

⊢ ∀n. prime n ⇒ 1 < n ∧ ∀k. 0 < k ∧ k < n ⇒ n divides binomial n k

⊢ ∀n k. prime n ∧ 0 < k ∧ k < n ⇒ n divides binomial n k

⊢ ∀n p.
    1 < n ∧ p < n ∧ prime p ∧ p divides n ⇒
    ¬(p divides FACT (n − 1) DIV FACT (n − p))

⊢ ∀n. prime n ⇔ 1 < n ∧ ∀k. 0 < k ∧ k < n ⇒ n divides binomial n k

⊢ ∀n. prime n ⇔ 1 < n ∧ ∀k. 0 < k ∧ k < n ⇒ binomial n k MOD n = 0

⊢ ∀n. PROD [1 .. n] = FACT n

⊢ ∀l. rotate 0 l = l

⊢ ∀n m l. n + m ≤ LENGTH l ⇒ rotate n (rotate m l) = rotate (n + m) l

⊢ ∀l. rotate (LENGTH l) l = l

⊢ ∀k l. k < LENGTH l ⇒ rotate (LENGTH l − k) (rotate k l) = l

⊢ ∀n. rotate n [] = []

⊢ ∀k l. k < LENGTH l ⇒ rotate k (rotate (LENGTH l − k) l) = l

⊢ ∀l n. LENGTH (rotate n l) = LENGTH l

⊢ ∀l n. set (rotate n l) = set l

⊢ ∀l n. n < LENGTH l ⇒ rotate n l = l❲n❳::(DROP (SUC n) l ⧺ TAKE n l)

⊢ ∀l n. n < LENGTH l ⇒ rotate (SUC n) l = rotate 1 (rotate n l)

⊢ set_lcm ∅ = 1

⊢ ∀s. FINITE s ⇒ big_lcm s = set_lcm s

⊢ ∀l. set_lcm (set l) = list_lcm l

⊢ ∀s. FINITE s ⇒ ∀x. set_lcm (x INSERT s) = lcm x (set_lcm s)

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

⊢ ∀s m. FINITE s ∧ (∀x. x ∈ s ⇒ x divides m) ⇒ set_lcm s divides m

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ set_lcm s = lcm (CHOICE s) (set_lcm (REST s))

⊢ ∀x. set_lcm {x} = x

⊢ ∀n. sub_count 0 n = if n = 0 then {∅} else ∅

⊢ ∀n k.
    sub_count n 0 = {∅} ∧ sub_count 0 (k + 1) = ∅ ∧
    sub_count (n + 1) (k + 1) =
    IMAGE (λs. n INSERT s) (sub_count n k) ∪ sub_count n (k + 1)

⊢ ∀n m. INJ (sub_count n) (upto n) 𝕌(:(num -> bool) -> bool)

⊢ ∀n k.
    DISJOINT (IMAGE (λs. n INSERT s) (sub_count n k)) (sub_count n (k + 1))

⊢ ∀n k s. s ∈ sub_count n k ⇔ s ⊆ count n ∧ CARD s = k

⊢ ∀n k s. s ∈ sub_count n k ⇒ FINITE s

⊢ ∀n k s. s ∈ sub_count n k ⇒ n ∉ s

⊢ ∀n k. sub_count n k = ∅ ⇔ n < k

⊢ ∀n k.
    sub_count n k =
    if k = 0 then {∅}
    else if n = 0 then ∅
    else
      IMAGE (λs. n − 1 INSERT s) (sub_count (n − 1) (k − 1)) ∪
      sub_count (n − 1) k

⊢ ∀n s.
    s ⊆ count n ⇒
    sub_count n (CARD s) = equiv_class (λs t. s =b= t) (POW (count n)) s

⊢ ∀n k. FINITE (sub_count n k)

⊢ ∀n k s. s ∈ sub_count n k ⇒ n INSERT s ∈ sub_count (n + 1) (k + 1)

⊢ ∀n k. CARD (IMAGE (λs. n INSERT s) (sub_count n k)) = n choose k

⊢ ∀n. sub_count n 0 = {∅}

⊢ ∀n. sub_count n 1 = {{j} | j < n}

⊢ ∀n. sub_count n n = {count n}

⊢ ∀n k. sub_count n k ⊆ POW (count n)

⊢ ∀n k.
    sub_count (n + 1) (k + 1) =
    IMAGE (λs. n INSERT s) (sub_count n k) ∪ sub_count n (k + 1)

⊢ ∀P k s. s ∈ sub_sets P k ⇔ s ⊆ P ∧ CARD s = k

⊢ ∀s t.
    FINITE t ∧ s ⊆ t ⇒
    sub_sets t (CARD s) = equiv_class (λs t. s =b= t) (POW t) s

⊢ ∀n k. sub_sets (count n) k = sub_count n k

⊢ ∀n. TWICE (SUM [1 .. n]) = n * (n + 1)

⊢ ∀n. SUM [1 .. n] = tri n

⊢ ∀n. SUM [1 .. n] = HALF (n * (n + 1))

⊢ ∀f s t.
    FINITE s ∧ over f s t ⇒
    (SURJ f s t ⇔ ∀y. y ∈ t ⇒ CARD (preimage f s y) ≠ 0)

⊢ ∀f s t. SURJ f s t ⇔ over f s t ∧ ∀y. y ∈ t ⇒ preimage f s y ≠ ∅

⊢ ∀ls. ls ≠ [] ⇒ TL (turn ls) = FRONT ls

⊢ ∀a0 a1 a2 a0' a1' a2'.
    triple a0 a1 a2 = triple a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'

⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (triple a0 a1 a2) = f a0 a1 a2

⊢ (∀n n0 n1. (triple n n0 n1).a = n) ∧
  (∀n n0 n1. (triple n n0 n1).b = n0) ∧ ∀n n0 n1. (triple n n0 n1).c = n1

⊢ (∀t f. (t with b updated_by f).a = t.a) ∧
  (∀t f. (t with c updated_by f).a = t.a) ∧
  (∀t f. (t with a updated_by f).b = t.b) ∧
  (∀t f. (t with c updated_by f).b = t.b) ∧
  (∀t f. (t with a updated_by f).c = t.c) ∧
  (∀t f. (t with b updated_by f).c = t.c) ∧
  (∀t f. (t with a updated_by f).a = f t.a) ∧
  (∀t f. (t with b updated_by f).b = f t.b) ∧
  ∀t f. (t with c updated_by f).c = f t.c

⊢ ∀M M' f.
    M = M' ∧ (∀a0 a1 a2. M' = triple a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
    triple_CASE M f = triple_CASE M' f'

⊢ triple_CASE x f = v ⇔ ∃n n0 n1. x = triple n n0 n1 ∧ f n n0 n1 = v

⊢ ∀t1 t2. t1 = t2 ⇔ t1.a = t2.a ∧ t1.b = t2.b ∧ t1.c = t2.c

⊢ (∀f n n0 n1. triple n n0 n1 with a updated_by f = triple (f n) n0 n1) ∧
  (∀f n n0 n1. triple n n0 n1 with b updated_by f = triple n (f n0) n1) ∧
  ∀f n n0 n1. triple n n0 n1 with c updated_by f = triple n n0 (f n1)

⊢ (∀t g f.
     t with <|b updated_by f; a updated_by g|> =
     t with <|a updated_by g; b updated_by f|>) ∧
  (∀t g f.
     t with <|c updated_by f; a updated_by g|> =
     t with <|a updated_by g; c updated_by f|>) ∧
  ∀t g f.
    t with <|c updated_by f; b updated_by g|> =
    t with <|b updated_by g; c updated_by f|>

⊢ ((∀g f. b_fupd f ∘ a_fupd g = a_fupd g ∘ b_fupd f) ∧
   ∀h g f. b_fupd f ∘ a_fupd g ∘ h = a_fupd g ∘ b_fupd f ∘ h) ∧
  ((∀g f. c_fupd f ∘ a_fupd g = a_fupd g ∘ c_fupd f) ∧
   ∀h g f. c_fupd f ∘ a_fupd g ∘ h = a_fupd g ∘ c_fupd f ∘ h) ∧
  (∀g f. c_fupd f ∘ b_fupd g = b_fupd g ∘ c_fupd f) ∧
  ∀h g f. c_fupd f ∘ b_fupd g ∘ h = b_fupd g ∘ c_fupd f ∘ h

⊢ (∀t g f.
     t with <|a updated_by f; a updated_by g|> = t with a updated_by f ∘ g) ∧
  (∀t g f.
     t with <|b updated_by f; b updated_by g|> = t with b updated_by f ∘ g) ∧
  ∀t g f.
    t with <|c updated_by f; c updated_by g|> = t with c updated_by f ∘ g

⊢ ((∀g f. a_fupd f ∘ a_fupd g = a_fupd (f ∘ g)) ∧
   ∀h g f. a_fupd f ∘ a_fupd g ∘ h = a_fupd (f ∘ g) ∘ h) ∧
  ((∀g f. b_fupd f ∘ b_fupd g = b_fupd (f ∘ g)) ∧
   ∀h g f. b_fupd f ∘ b_fupd g ∘ h = b_fupd (f ∘ g) ∘ h) ∧
  (∀g f. c_fupd f ∘ c_fupd g = c_fupd (f ∘ g)) ∧
  ∀h g f. c_fupd f ∘ c_fupd g ∘ h = c_fupd (f ∘ g) ∘ h

⊢ ∀P. (∀n n0 n1. P (triple n n0 n1)) ⇒ ∀t. P t

⊢ ∀n11 n01 n1 n12 n02 n2.
    <|a := n11; b := n01; c := n1|> = <|a := n12; b := n02; c := n2|> ⇔
    n11 = n12 ∧ n01 = n02 ∧ n1 = n2

⊢ ∀t. ∃n1 n0 n. t = <|a := n1; b := n0; c := n|>

⊢ ∀tt. ∃n n0 n1. tt = triple n n0 n1

⊢ ∀t n1 n0 n.
    t with <|a := n1; b := n0; c := n|> = <|a := n1; b := n0; c := n|>

⊢ ∀p. turn p = [] ⇔ p = []

⊢ ∀l. turn_exp l 0 = l

⊢ ∀l. turn_exp l 1 = turn l

⊢ ∀l. turn_exp l 2 = turn (turn l)

⊢ ∀l n. turn_exp l (SUC n) = turn_exp (turn l) n

⊢ ∀l n. LENGTH (turn_exp l n) = LENGTH l

⊢ ∀l n. turn_exp l (SUC n) = turn (turn_exp l n)

⊢ ∀l. LENGTH (turn l) = LENGTH l

⊢ turn [] = []

⊢ ∀l. l ≠ [] ⇒ turn l = LAST l::FRONT l

⊢ ∀ls x. turn (SNOC x ls) = x::ls