Thm* q:, n1,n2:, r1:(qn1), r2:(qn2). (qn1)+r1 = (qn2)+r2 n1 = n2 & r1 = r2 geom_unique

Thm* q:, n:, i:, r1:(qn), r2:(qn+i). (qn)+r1 = (qn+i)+r2 False geom_n_unique

Thm* q,n:, i:. (qn)+(qn)(qn+i) geom_speed_lbound

Thm* q,n:. (qn+1) = (qn)+(qn) geom_series_step

Thm* n:, m:, k:(nm). l:n*. ||l|| = m & en(l) = k en_surj

Thm* n:, l:n*. en(l) (n||l||) en_bound

Thm* n:, l:n*. en(l) < (n||l||) en_ubound

Thm* n,m:. f:((mn)(nm)). Bij(mn; (nm); f) fun_enumer

Thm* n,k:. 0 < k (nk) = n(nk-1) exp_step

Thm* n:. (n0) = 1 exp_base

Thm* m:, n:. 0 < (mn) exp_non_zero

Thm* m:. (0m) = 0 exp_zero

Thm* n1,n2,k1,k2:. n1 = n2 k1 = k2 (n1k1) = (n2k2) exp_functionality