Combnat.central: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend as Combnat
Lines 97-108 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&start_line=97&end_line=108

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as FA

def central(+i: Nat) -> {Nat.is_le(C.pow2(i), S.choose(Nat.double(i), i)) == True{} : Bool}:
  match i:
    case 0n:
      {==}
    case 1n+ +ip:
      +m = {1n+Nat.double(ip) : Nat}
      +y = S.choose(m, ip)
      +hs = L.subst(Nat, z => {S.choose(m, z) == y : Nat}, Nat.sub(m, ip), 1n+ip, sub_half(ip), FA.choose_symm(m, ip, N.le_trans(ip, Nat.double(ip), m, N.double_self_le(ip), N.le_succ(Nat.double(ip)))))
      +e2 = Equal.trans(Nat, Nat.add(y, S.choose(m, 1n+ip)), Nat.add(y, y), Nat.double(y), Equal.cong(Nat, Nat, t => Nat.add(y, t), S.choose(m, 1n+ip), y, hs), Equal.sym(Nat, Nat.double(y), Nat.add(y, y), NA.double_self(y)))
      +h1 = N.double_le(C.pow2(ip), y, N.le_trans(C.pow2(ip), S.choose(Nat.double(ip), ip), y, central(ip), cn_mono(Nat.double(ip), ip)))
      +h2 = L.subst(Nat, z => {Nat.is_le(Nat.double(C.pow2(ip)), z) == True{} : Bool}, Nat.double(y), Nat.add(y, S.choose(m, 1n+ip)), Equal.sym(Nat, Nat.add(y, S.choose(m, 1n+ip)), Nat.double(y), e2), h1)
      L.subst(Nat, z => {Nat.is_le(Nat.double(C.pow2(ip)), S.choose(z, 1n+ip)) == True{} : Bool}, Nat.add(2n, Nat.double(ip)), Nat.double(1n+ip), Equal.sym(Nat, Nat.double(1n+ip), Nat.add(2n, Nat.double(ip)), N.double_succ(ip)), h2)

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_self
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=double_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=double_self_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=double_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend&name=choose_symm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&name=cn_mono
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/combnat.bend&name=sub_half
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/natural.bend&name=choose