def central

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/combnat.bend:97

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

97def central(+i: Nat) -> {Nat.is_le(C.pow2(i), S.choose(Nat.double(i), i)) == True{} : Bool}:
98  match i:
99    case 0n:
100      {==}
101    case 1n+ +ip:
102      +m = {1n+Nat.double(ip) : Nat}
103      +y = S.choose(m, ip)
104      +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)))))
105      +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)))
106      +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)))
107      +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)
108      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)