1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/logic.bend as L
4	import ../../lib/lemmas/proofs/nat_algebra.bend as A
5	import ../../../src/math/natural.bend as M
6	import ./arith.bend as R
7	import ./lcm.bend as LC
8	import ../../../spec/math/natural.bend as S
9	
10	# factorial, perm and comb against the structural definitions of
11	# spec.bend, following Lean 4 Mathlib (Mathlib/Data/Nat/Factorial/Basic,
12	# Mathlib/Data/Nat/Choose/Basic): Nat.factorial_pos,
13	# Nat.succ_descFactorial_succ, Nat.descFactorial_self,
14	# Nat.factorial_mul_descFactorial, Nat.add_one_mul_choose_eq,
15	# Nat.choose_succ_right_eq, Nat.descFactorial_eq_factorial_mul_choose,
16	# Nat.choose_mul_factorial_mul_factorial, Nat.choose_symm,
17	# Nat.choose_eq_zero_of_lt.
18	
19	# (x a) f == a (x f)
20	def mul_left_comm(+x: Nat, +a: Nat, +f: Nat) -> {Nat.mul(Nat.mul(x, a), f) == Nat.mul(a, Nat.mul(x, f)) : Nat}:
21	  Equal.trans(Nat, Nat.mul(Nat.mul(x, a), f), Nat.mul(Nat.mul(a, x), f), Nat.mul(a, Nat.mul(x, f)), Equal.cong(Nat, Nat, z => Nat.mul(z, f), Nat.mul(x, a), Nat.mul(a, x), A.mul_comm(x, a)), A.mul_assoc(a, x, f))
22	
23	# ---- factorial ----
24	
25	def factorial_go(+n: Nat, +acc: Nat) -> {M.factorial_go(n, acc) == Nat.mul(acc, S.factorial(n)) : Nat}:
26	  match n:
27	    case 0n:
28	      Equal.sym(Nat, Nat.mul(acc, 1n), acc, A.mul_one(acc))
29	    case 1n+ +p:
30	      Equal.trans(Nat, M.factorial_go(p, Nat.mul(1n+p, acc)), Nat.mul(Nat.mul(1n+p, acc), S.factorial(p)), Nat.mul(acc, Nat.mul(1n+p, S.factorial(p))), factorial_go(p, Nat.mul(1n+p, acc)), mul_left_comm(1n+p, acc, S.factorial(p)))
31	
32	# factorial(n) == n!
33	def factorial_ok(+n: Nat) -> {M.factorial(n) == S.factorial(n) : Nat}:
34	  Equal.trans(Nat, M.factorial(n), Nat.mul(1n, S.factorial(n)), S.factorial(n), factorial_go(n, 1n), LC.one_mul(S.factorial(n)))
35	
36	def pos_mul(+p: Nat, +f: Nat, +h: {Nat.is_lt(0n, f) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.mul(1n+p, f)) == True{} : Bool}:
37	  match f:
38	    case 0n:
39	      Empty.absurd({Nat.is_lt(0n, Nat.mul(1n+p, 0n)) == True{} : Bool}, L.false_true(h))
40	    case 1n+fp:
41	      {==}
42	
43	# 0 < n!   (Mathlib Nat.factorial_pos)
44	def factorial_pos(+n: Nat) -> {Nat.is_lt(0n, S.factorial(n)) == True{} : Bool}:
45	  match n:
46	    case 0n:
47	      {==}
48	    case 1n+ +p:
49	      pos_mul(p, S.factorial(p), factorial_pos(p))
50	
51	# ---- descending factorial: perm ----
52	
53	# (1+m).desc(1+j) == (1+m) * m.desc(j)   (Mathlib Nat.succ_descFactorial_succ)
54	def desc_succ(+m: Nat, +j: Nat) -> {S.desc(1n+m, 1n+j) == Nat.mul(1n+m, S.desc(m, j)) : Nat}:
55	  match j:
56	    case 0n:
57	      {==}
58	    case 1n+ +i:
59	      %Equal.sym(Nat, S.desc(1n+m, 1n+i), Nat.mul(1n+m, S.desc(m, i)), desc_succ(m, i)) : {Nat.mul(Nat.sub(m, i), _) == Nat.mul(1n+m, Nat.mul(Nat.sub(m, i), S.desc(m, i))) : Nat}
60	      LC.swap_cw(Nat.sub(m, i), 1n+m, S.desc(m, i))
61	
62	# m * (m - 1).desc(j) == m.desc(1+j), the order perm multiplies in
63	def desc_front(+m: Nat, +j: Nat) -> {Nat.mul(m, S.desc(Nat.sub(m, 1n), j)) == S.desc(m, 1n+j) : Nat}:
64	  match m:
65	    case 0n:
66	      Equal.sym(Nat, Nat.mul(Nat.sub(0n, j), S.desc(0n, j)), 0n, Equal.cong(Nat, Nat, z => Nat.mul(z, S.desc(0n, j)), Nat.sub(0n, j), 0n, R.zsub(j)))
67	    case 1n+ +mp:
68	      %Equal.sym(Nat, Nat.sub(1n+mp, 1n), mp, N.sub_zero(mp)) : {Nat.mul(1n+mp, S.desc(_, j)) == S.desc(1n+mp, 1n+j) : Nat}
69	      Equal.sym(Nat, S.desc(1n+mp, 1n+j), Nat.mul(1n+mp, S.desc(mp, j)), desc_succ(mp, j))
70	
71	def perm_go(+k: Nat, +m: Nat, +acc: Nat) -> {M.perm_go(k, m, acc) == Nat.mul(acc, S.desc(m, k)) : Nat}:
72	  match k:
73	    case 0n:
74	      Equal.sym(Nat, Nat.mul(acc, 1n), acc, A.mul_one(acc))
75	    case 1n+ +j:
76	      Equal.trans(Nat, M.perm_go(j, Nat.sub(m, 1n), Nat.mul(acc, m)), Nat.mul(Nat.mul(acc, m), S.desc(Nat.sub(m, 1n), j)), Nat.mul(acc, S.desc(m, 1n+j)), perm_go(j, Nat.sub(m, 1n), Nat.mul(acc, m)),
77	        Equal.trans(Nat, Nat.mul(Nat.mul(acc, m), S.desc(Nat.sub(m, 1n), j)), Nat.mul(acc, Nat.mul(m, S.desc(Nat.sub(m, 1n), j))), Nat.mul(acc, S.desc(m, 1n+j)), A.mul_assoc(acc, m, S.desc(Nat.sub(m, 1n), j)),
78	          Equal.cong(Nat, Nat, z => Nat.mul(acc, z), Nat.mul(m, S.desc(Nat.sub(m, 1n), j)), S.desc(m, 1n+j), desc_front(m, j))))
79	
80	# perm(n, k) == n.descFactorial(k)
81	def perm_ok(+n: Nat, +k: Nat) -> {M.perm(n, k) == S.desc(n, k) : Nat}:
82	  Equal.trans(Nat, M.perm(n, k), Nat.mul(1n, S.desc(n, k)), S.desc(n, k), perm_go(k, n, 1n), LC.one_mul(S.desc(n, k)))
83	
84	# n.desc(n) == n!   (Mathlib Nat.descFactorial_self)
85	def desc_self(+n: Nat) -> {S.desc(n, n) == S.factorial(n) : Nat}:
86	  match n:
87	    case 0n:
88	      {==}
89	    case 1n+ +p:
90	      Equal.trans(Nat, S.desc(1n+p, 1n+p), Nat.mul(1n+p, S.desc(p, p)), S.factorial(1n+p), desc_succ(p, p), Equal.cong(Nat, Nat, z => Nat.mul(1n+p, z), S.desc(p, p), S.factorial(p), desc_self(p)))
91	
92	# j < n gives n - j == 1 + (n - (1 + j))
93	def sub_lt_succ(+n: Nat, +j: Nat, +h: {Nat.is_lt(j, n) == True{} : Bool}) -> {Nat.sub(n, j) == 1n+Nat.sub(n, 1n+j) : Nat}:
94	  match n j:
95	    case 0n j0:
96	      Empty.absurd({Nat.sub(0n, j0) == 1n+Nat.sub(0n, 1n+j0) : Nat}, N.lt_zero_absurd(j0, h))
97	    case 1n+ +np 0n:
98	      Equal.sym(Nat, 1n+Nat.sub(np, 0n), 1n+np, N.succ_cong(Nat.sub(np, 0n), np, N.sub_zero(np)))
99	    case 1n+ +np 1n+ +jp:
100	      sub_lt_succ(np, jp, h)
101	
102	# (n - k)! * n.desc(k) == n!   (Mathlib Nat.factorial_mul_descFactorial)
103	def factorial_mul_desc(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.mul(S.factorial(Nat.sub(n, k)), S.desc(n, k)) == S.factorial(n) : Nat}:
104	  match k:
105	    case 0n:
106	      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.mul(S.factorial(_), 1n) == S.factorial(n) : Nat}
107	      A.mul_one(S.factorial(n))
108	    case 1n+ +j:
109	      +t = Nat.sub(n, 1n+j)
110	      +hj = N.succ_le_lt(j, n, h)
111	      +ih = factorial_mul_desc(n, j, N.lt_le(j, n, hj))
112	      +es = sub_lt_succ(n, j, hj)
113	      # t! * ((n - j) * n.desc(j)) == ((n - j) * t!) * n.desc(j) == (n - j)! * n.desc(j)
114	      %Equal.sym(Nat, Nat.mul(S.factorial(t), Nat.mul(Nat.sub(n, j), S.desc(n, j))), Nat.mul(Nat.mul(Nat.sub(n, j), S.factorial(t)), S.desc(n, j)), Equal.sym(Nat, Nat.mul(Nat.mul(Nat.sub(n, j), S.factorial(t)), S.desc(n, j)), Nat.mul(S.factorial(t), Nat.mul(Nat.sub(n, j), S.desc(n, j))), mul_left_comm(Nat.sub(n, j), S.factorial(t), S.desc(n, j)))) : {_ == S.factorial(n) : Nat}
115	      %Equal.sym(Nat, Nat.sub(n, j), 1n+t, es) : {Nat.mul(Nat.mul(_, S.factorial(t)), S.desc(n, j)) == S.factorial(n) : Nat}
116	      %Equal.sym(Nat, Nat.mul(1n+t, S.factorial(t)), S.factorial(Nat.sub(n, j)), Equal.trans(Nat, Nat.mul(1n+t, S.factorial(t)), S.factorial(1n+t), S.factorial(Nat.sub(n, j)), {==}, Equal.cong(Nat, Nat, z => S.factorial(z), 1n+t, Nat.sub(n, j), Equal.sym(Nat, Nat.sub(n, j), 1n+t, es)))) : {Nat.mul(_, S.desc(n, j)) == S.factorial(n) : Nat}
117	      ih
118	
119	# ---- binomial coefficients ----
120	
121	def choose_zero_right(+n: Nat) -> {S.choose(n, 0n) == 1n : Nat}:
122	  match n:
123	    case 0n:
124	      {==}
125	    case 1n+m:
126	      {==}
127	
128	# C(n, 1) == n
129	def choose_one_right(+n: Nat) -> {S.choose(n, 1n) == n : Nat}:
130	  match n:
131	    case 0n:
132	      {==}
133	    case 1n+ +m:
134	      %Equal.sym(Nat, S.choose(m, 0n), 1n, choose_zero_right(m)) : {Nat.add(_, S.choose(m, 1n)) == 1n+m : Nat}
135	      N.succ_cong(S.choose(m, 1n), m, choose_one_right(m))
136	
137	# (n + 1) C(n, k) == C(n + 1, k + 1) (k + 1)   (Mathlib Nat.add_one_mul_choose_eq)
138	def succ_mul_choose(+n: Nat, +k: Nat) -> {Nat.mul(1n+n, S.choose(n, k)) == Nat.mul(S.choose(1n+n, 1n+k), 1n+k) : Nat}:
139	  match n k:
140	    case 0n 0n:
141	      {==}
142	    case 0n 1n+j:
143	      {==}
144	    case 1n+ +m 0n:
145	      %Equal.sym(Nat, S.choose(1n+m, 0n), 1n, choose_zero_right(1n+m)) : {Nat.mul(2n+m, _) == Nat.mul(Nat.add(S.choose(1n+m, 0n), S.choose(1n+m, 1n)), 1n) : Nat}
146	      %Equal.sym(Nat, S.choose(1n+m, 0n), 1n, choose_zero_right(1n+m)) : {Nat.mul(2n+m, 1n) == Nat.mul(Nat.add(_, S.choose(1n+m, 1n)), 1n) : Nat}
147	      %Equal.sym(Nat, S.choose(1n+m, 1n), 1n+m, choose_one_right(1n+m)) : {Nat.mul(2n+m, 1n) == Nat.mul(Nat.add(1n, _), 1n) : Nat}
148	      {==}
149	    case 1n+ +m 1n+ +j:
150	      +x = S.choose(1n+m, 1n+j)
151	      +y = S.choose(1n+m, 2n+j)
152	      +c0 = S.choose(m, j)
153	      +c1 = S.choose(m, 1n+j)
154	      # (x + y)(2 + j) == x + x(1 + j) + y(2 + j) == x + (1+m) c0 + (1+m) c1 == x + (1+m) x
155	      %Equal.sym(Nat, Nat.mul(Nat.add(x, y), 2n+j), Nat.add(Nat.mul(x, 2n+j), Nat.mul(y, 2n+j)), A.mul_add_right(x, y, 2n+j)) : {Nat.mul(2n+m, x) == _ : Nat}
156	      %Equal.sym(Nat, Nat.mul(x, 2n+j), Nat.add(x, Nat.mul(x, 1n+j)), A.mul_succ(x, 1n+j)) : {Nat.mul(2n+m, x) == Nat.add(_, Nat.mul(y, 2n+j)) : Nat}
157	      %Equal.sym(Nat, Nat.mul(x, 1n+j), Nat.mul(1n+m, c0), Equal.sym(Nat, Nat.mul(1n+m, c0), Nat.mul(x, 1n+j), succ_mul_choose(m, j))) : {Nat.mul(2n+m, x) == Nat.add(Nat.add(x, _), Nat.mul(y, 2n+j)) : Nat}
158	      %Equal.sym(Nat, Nat.mul(y, 2n+j), Nat.mul(1n+m, c1), Equal.sym(Nat, Nat.mul(1n+m, c1), Nat.mul(y, 2n+j), succ_mul_choose(m, 1n+j))) : {Nat.mul(2n+m, x) == Nat.add(Nat.add(x, Nat.mul(1n+m, c0)), _) : Nat}
159	      %Equal.sym(Nat, Nat.add(Nat.add(x, Nat.mul(1n+m, c0)), Nat.mul(1n+m, c1)), Nat.add(x, Nat.add(Nat.mul(1n+m, c0), Nat.mul(1n+m, c1))), A.add_assoc(x, Nat.mul(1n+m, c0), Nat.mul(1n+m, c1))) : {Nat.mul(2n+m, x) == _ : Nat}
160	      %Equal.sym(Nat, Nat.add(Nat.mul(1n+m, c0), Nat.mul(1n+m, c1)), Nat.mul(1n+m, Nat.add(c0, c1)), Equal.sym(Nat, Nat.mul(1n+m, Nat.add(c0, c1)), Nat.add(Nat.mul(1n+m, c0), Nat.mul(1n+m, c1)), A.mul_add_left(1n+m, c0, c1))) : {Nat.mul(2n+m, x) == Nat.add(x, _) : Nat}
161	      {==}
162	
163	# a (x - y) == a x - a y
164	def mul_sub_left(+a: Nat, +x: Nat, +y: Nat) -> {Nat.mul(a, Nat.sub(x, y)) == Nat.sub(Nat.mul(a, x), Nat.mul(a, y)) : Nat}:
165	  %Equal.sym(Nat, Nat.mul(a, Nat.sub(x, y)), Nat.mul(Nat.sub(x, y), a), A.mul_comm(a, Nat.sub(x, y))) : {_ == Nat.sub(Nat.mul(a, x), Nat.mul(a, y)) : Nat}
166	  %Equal.sym(Nat, Nat.mul(a, x), Nat.mul(x, a), A.mul_comm(a, x)) : {Nat.mul(Nat.sub(x, y), a) == Nat.sub(_, Nat.mul(a, y)) : Nat}
167	  %Equal.sym(Nat, Nat.mul(a, y), Nat.mul(y, a), A.mul_comm(a, y)) : {Nat.mul(Nat.sub(x, y), a) == Nat.sub(Nat.mul(x, a), _) : Nat}
168	  R.mul_sub(x, y, a)
169	
170	# C(n, k + 1) (k + 1) == C(n, k) (n - k)   (Mathlib Nat.choose_succ_right_eq)
171	def choose_succ_right(+n: Nat, +k: Nat) -> {Nat.mul(S.choose(n, 1n+k), 1n+k) == Nat.mul(S.choose(n, k), Nat.sub(n, k)) : Nat}:
172	  +c = S.choose(n, k)
173	  +d = S.choose(n, 1n+k)
174	  # (1 + n) c == c (1 + k) + d (1 + k)
175	  +e = Equal.trans(Nat, Nat.mul(1n+n, c), Nat.mul(Nat.add(c, d), 1n+k), Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), succ_mul_choose(n, k), A.mul_add_right(c, d, 1n+k))
176	  %Equal.sym(Nat, Nat.mul(c, Nat.sub(n, k)), Nat.sub(Nat.mul(c, 1n+n), Nat.mul(c, 1n+k)), mul_sub_left(c, 1n+n, 1n+k)) : {Nat.mul(d, 1n+k) == _ : Nat}
177	  %Equal.sym(Nat, Nat.mul(c, 1n+n), Nat.mul(1n+n, c), A.mul_comm(c, 1n+n)) : {Nat.mul(d, 1n+k) == Nat.sub(_, Nat.mul(c, 1n+k)) : Nat}
178	  %Equal.sym(Nat, Nat.mul(1n+n, c), Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), e) : {Nat.mul(d, 1n+k) == Nat.sub(_, Nat.mul(c, 1n+k)) : Nat}
179	  Equal.sym(Nat, Nat.sub(Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), Nat.mul(c, 1n+k)), Nat.mul(d, 1n+k), N.add_sub_cancel(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)))
180	
181	# C(n, k) k! == n.desc(k)   (Mathlib Nat.descFactorial_eq_factorial_mul_choose)
182	def choose_mul_factorial(+n: Nat, +k: Nat) -> {Nat.mul(S.choose(n, k), S.factorial(k)) == S.desc(n, k) : Nat}:
183	  match k:
184	    case 0n:
185	      %Equal.sym(Nat, S.choose(n, 0n), 1n, choose_zero_right(n)) : {Nat.mul(_, 1n) == 1n : Nat}
186	      {==}
187	    case 1n+ +j:
188	      # C(n, 1+j) ((1+j) j!) == (C(n, 1+j) (1+j)) j! == (C(n, j) (n - j)) j! == (n - j) (C(n, j) j!)
189	      %Equal.sym(Nat, Nat.mul(S.choose(n, 1n+j), Nat.mul(1n+j, S.factorial(j))), Nat.mul(Nat.mul(S.choose(n, 1n+j), 1n+j), S.factorial(j)), Equal.sym(Nat, Nat.mul(Nat.mul(S.choose(n, 1n+j), 1n+j), S.factorial(j)), Nat.mul(S.choose(n, 1n+j), Nat.mul(1n+j, S.factorial(j))), A.mul_assoc(S.choose(n, 1n+j), 1n+j, S.factorial(j)))) : {_ == S.desc(n, 1n+j) : Nat}
190	      %Equal.sym(Nat, Nat.mul(S.choose(n, 1n+j), 1n+j), Nat.mul(S.choose(n, j), Nat.sub(n, j)), choose_succ_right(n, j)) : {Nat.mul(_, S.factorial(j)) == S.desc(n, 1n+j) : Nat}
191	      %Equal.sym(Nat, Nat.mul(Nat.mul(S.choose(n, j), Nat.sub(n, j)), S.factorial(j)), Nat.mul(Nat.sub(n, j), Nat.mul(S.choose(n, j), S.factorial(j))), Equal.trans(Nat, Nat.mul(Nat.mul(S.choose(n, j), Nat.sub(n, j)), S.factorial(j)), Nat.mul(Nat.mul(Nat.sub(n, j), S.choose(n, j)), S.factorial(j)), Nat.mul(Nat.sub(n, j), Nat.mul(S.choose(n, j), S.factorial(j))), Equal.cong(Nat, Nat, z => Nat.mul(z, S.factorial(j)), Nat.mul(S.choose(n, j), Nat.sub(n, j)), Nat.mul(Nat.sub(n, j), S.choose(n, j)), A.mul_comm(S.choose(n, j), Nat.sub(n, j))), A.mul_assoc(Nat.sub(n, j), S.choose(n, j), S.factorial(j)))) : {_ == S.desc(n, 1n+j) : Nat}
192	      Equal.cong(Nat, Nat, z => Nat.mul(Nat.sub(n, j), z), Nat.mul(S.choose(n, j), S.factorial(j)), S.desc(n, j), choose_mul_factorial(n, j))
193	
194	# n < k gives C(n, k) == 0   (Mathlib Nat.choose_eq_zero_of_lt)
195	def choose_eq_zero(+n: Nat, +k: Nat, +h: {Nat.is_lt(n, k) == True{} : Bool}) -> {S.choose(n, k) == 0n : Nat}:
196	  match n k:
197	    case n0 0n:
198	      Empty.absurd({S.choose(n0, 0n) == 0n : Nat}, N.lt_zero_absurd(n0, h))
199	    case 0n 1n+j:
200	      {==}
201	    case 1n+ +m 1n+ +j:
202	      %Equal.sym(Nat, S.choose(m, j), 0n, choose_eq_zero(m, j, h)) : {Nat.add(_, S.choose(m, 1n+j)) == 0n : Nat}
203	      choose_eq_zero(m, 1n+j, N.lt_trans(m, j, 1n+j, h, N.lt_succ(j)))
204	
205	def pos_pos(+a: Nat, +b: Nat, +ha: {Nat.is_lt(0n, a) == True{} : Bool}, +hb: {Nat.is_lt(0n, b) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.mul(a, b)) == True{} : Bool}:
206	  match a:
207	    case 0n:
208	      Empty.absurd({Nat.is_lt(0n, Nat.mul(0n, b)) == True{} : Bool}, L.false_true(ha))
209	    case 1n+ +ap:
210	      pos_mul(ap, b, hb)
211	
212	# C(n, k) (k! (n - k)!) == n!   (Mathlib Nat.choose_mul_factorial_mul_factorial)
213	def choose_mul_facts(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.mul(S.choose(n, k), Nat.mul(S.factorial(k), S.factorial(Nat.sub(n, k)))) == S.factorial(n) : Nat}:
214	  %Equal.sym(Nat, Nat.mul(S.choose(n, k), Nat.mul(S.factorial(k), S.factorial(Nat.sub(n, k)))), Nat.mul(Nat.mul(S.choose(n, k), S.factorial(k)), S.factorial(Nat.sub(n, k))), Equal.sym(Nat, Nat.mul(Nat.mul(S.choose(n, k), S.factorial(k)), S.factorial(Nat.sub(n, k))), Nat.mul(S.choose(n, k), Nat.mul(S.factorial(k), S.factorial(Nat.sub(n, k)))), A.mul_assoc(S.choose(n, k), S.factorial(k), S.factorial(Nat.sub(n, k))))) : {_ == S.factorial(n) : Nat}
215	  %Equal.sym(Nat, Nat.mul(S.choose(n, k), S.factorial(k)), S.desc(n, k), choose_mul_factorial(n, k)) : {Nat.mul(_, S.factorial(Nat.sub(n, k))) == S.factorial(n) : Nat}
216	  %Equal.sym(Nat, Nat.mul(S.desc(n, k), S.factorial(Nat.sub(n, k))), Nat.mul(S.factorial(Nat.sub(n, k)), S.desc(n, k)), A.mul_comm(S.desc(n, k), S.factorial(Nat.sub(n, k)))) : {_ == S.factorial(n) : Nat}
217	  factorial_mul_desc(n, k, h)
218	
219	# n - (n - k) == k for k <= n
220	def sub_sub_self(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.sub(n, Nat.sub(n, k)) == k : Nat}:
221	  +e = N.sub_add(n, k, h)
222	  %Equal.sym(Nat, n, Nat.add(k, Nat.sub(n, k)), Equal.sym(Nat, Nat.add(k, Nat.sub(n, k)), n, e)) : {Nat.sub(_, Nat.sub(n, k)) == k : Nat}
223	  %Equal.sym(Nat, Nat.add(k, Nat.sub(n, k)), Nat.add(Nat.sub(n, k), k), A.add_comm(k, Nat.sub(n, k))) : {Nat.sub(_, Nat.sub(n, k)) == k : Nat}
224	  N.add_sub_cancel(Nat.sub(n, k), k)
225	
226	def sub_le_self(+n: Nat, +k: Nat) -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}:
227	  match n k:
228	    case 0n k0:
229	      %Equal.sym(Nat, Nat.sub(0n, k0), 0n, R.zsub(k0)) : {Nat.is_le(_, 0n) == True{} : Bool}
230	      {==}
231	    case 1n+ +np 0n:
232	      N.le_refl(1n+np)
233	    case 1n+ +np 1n+ +kp:
234	      N.le_trans(Nat.sub(np, kp), np, 1n+np, sub_le_self(np, kp), N.le_succ(np))
235	
236	# C(n, n - k) == C(n, k)   (Mathlib Nat.choose_symm)
237	def choose_symm(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {S.choose(n, Nat.sub(n, k)) == S.choose(n, k) : Nat}:
238	  +kk = Nat.sub(n, k)
239	  +fk = S.factorial(k)
240	  +fkk = S.factorial(kk)
241	  +e1 = choose_mul_facts(n, kk, sub_le_self(n, k))
242	  +e1b = Equal.trans(Nat, Nat.mul(S.choose(n, kk), Nat.mul(fkk, fk)), Nat.mul(S.choose(n, kk), Nat.mul(fkk, S.factorial(Nat.sub(n, kk)))), S.factorial(n),
243	    Equal.cong(Nat, Nat, z => Nat.mul(S.choose(n, kk), Nat.mul(fkk, S.factorial(z))), k, Nat.sub(n, kk), Equal.sym(Nat, Nat.sub(n, kk), k, sub_sub_self(n, k, h))), e1)
244	  +e2 = Equal.trans(Nat, Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), Nat.mul(S.choose(n, k), Nat.mul(fk, fkk)), S.factorial(n),
245	    Equal.cong(Nat, Nat, z => Nat.mul(S.choose(n, k), z), Nat.mul(fkk, fk), Nat.mul(fk, fkk), A.mul_comm(fkk, fk)), choose_mul_facts(n, k, h))
246	  LC.cancel_pos(S.choose(n, kk), S.choose(n, k), Nat.mul(fkk, fk), pos_pos(fkk, fk, factorial_pos(kk), factorial_pos(k)), Equal.trans(Nat, Nat.mul(S.choose(n, kk), Nat.mul(fkk, fk)), S.factorial(n), Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), e1b, Equal.sym(Nat, Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), S.factorial(n), e2)))
247	
248	# ---- comb ----
249	
250	# every r_i is C(n, i), so each division is exact
251	def comb_go(+j: Nat, +n: Nat, +i: Nat) -> {M.comb_go(j, n, i, S.choose(n, i)) == S.choose(n, Nat.add(i, j)) : Nat}:
252	  match j:
253	    case 0n:
254	      Equal.cong(Nat, Nat, z => S.choose(n, z), i, Nat.add(i, 0n), Equal.sym(Nat, Nat.add(i, 0n), i, A.add_zero(i)))
255	    case 1n+ +jp:
256	      %Equal.sym(Nat, Nat.mul(S.choose(n, i), Nat.sub(n, i)), Nat.add(Nat.mul(S.choose(n, 1n+i), 1n+i), 0n), Equal.trans(Nat, Nat.mul(S.choose(n, i), Nat.sub(n, i)), Nat.mul(S.choose(n, 1n+i), 1n+i), Nat.add(Nat.mul(S.choose(n, 1n+i), 1n+i), 0n), Equal.sym(Nat, Nat.mul(S.choose(n, 1n+i), 1n+i), Nat.mul(S.choose(n, i), Nat.sub(n, i)), choose_succ_right(n, i)), Equal.sym(Nat, Nat.add(Nat.mul(S.choose(n, 1n+i), 1n+i), 0n), Nat.mul(S.choose(n, 1n+i), 1n+i), A.add_zero(Nat.mul(S.choose(n, 1n+i), 1n+i))))) : {M.comb_go(jp, n, 1n+i, Nat.div(_, 1n+i)) == S.choose(n, Nat.add(i, 1n+jp)) : Nat}
257	      %Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(S.choose(n, 1n+i), 1n+i), 0n), 1n+i), S.choose(n, 1n+i), R.div_of(S.choose(n, 1n+i), i, 0n, {==})) : {M.comb_go(jp, n, 1n+i, _) == S.choose(n, Nat.add(i, 1n+jp)) : Nat}
258	      %Equal.sym(Nat, Nat.add(i, 1n+jp), 1n+Nat.add(i, jp), A.add_succ(i, jp)) : {M.comb_go(jp, n, 1n+i, S.choose(n, 1n+i)) == S.choose(n, _) : Nat}
259	      comb_go(jp, n, 1n+i)
260	
261	def comb_min(+n: Nat, +k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(k, Nat.sub(n, k)) == b : Bool}) -> {S.choose(n, Nat.min(k, Nat.sub(n, k))) == S.choose(n, k) : Nat}:
262	  match b:
263	    case True{}:
264	      Equal.cong(Nat, Nat, z => S.choose(n, z), Nat.min(k, Nat.sub(n, k)), k, N.min_left(k, Nat.sub(n, k), hb))
265	    case False{}:
266	      Equal.trans(Nat, S.choose(n, Nat.min(k, Nat.sub(n, k))), S.choose(n, Nat.sub(n, k)), S.choose(n, k), Equal.cong(Nat, Nat, z => S.choose(n, z), Nat.min(k, Nat.sub(n, k)), Nat.sub(n, k), N.min_right(k, Nat.sub(n, k), hb)), choose_symm(n, k, hk))
267	
268	def comb_small(+n: Nat, +k: Nat, +b: Bool, +hb: {Nat.is_lt(n, k) == b : Bool}) -> {M.comb_small(n, k, b) == S.choose(n, k) : Nat}:
269	  match b:
270	    case True{}:
271	      Equal.sym(Nat, S.choose(n, k), 0n, choose_eq_zero(n, k, hb))
272	    case False{}:
273	      +m = Nat.min(k, Nat.sub(n, k))
274	      %Equal.sym(Nat, 1n, S.choose(n, 0n), Equal.sym(Nat, S.choose(n, 0n), 1n, choose_zero_right(n))) : {M.comb_go(m, n, 0n, _) == S.choose(n, k) : Nat}
275	      Equal.trans(Nat, M.comb_go(m, n, 0n, S.choose(n, 0n)), S.choose(n, m), S.choose(n, k), comb_go(m, n, 0n), comb_min(n, k, N.not_lt_le(n, k, hb), Nat.is_lt(k, Nat.sub(n, k)), {==}))
276	
277	# comb(n, k) == C(n, k)
278	def comb_ok(+n: Nat, +k: Nat) -> {M.comb(n, k) == S.choose(n, k) : Nat}:
279	  comb_small(n, k, Nat.is_lt(n, k), {==})