choose_factorial_bridge

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

1. 0001induction n
2. 0002intro k
3. 0003induction j
4. 0004intro c
5. 0005intro F
6. 0006intro K
7. 0007intro J
8. 0008intro hsum
9. 0009intro hchoose
10. 0010intro hF
11. 0011intro hK
12. 0012intro hJ
13. 0013have hk : k = 0
14. 0014trans k + 0
15. 0015symm
16. 0016apply PA3
17. 0017exact hsum
18. 0018have hc_one : c = 1
19. 0019specialize choose_self_of_eq 0
20. 0020specialize choose_self_of_eq k
21. 0021specialize choose_self_of_eq c
22. 0022apply choose_self_of_eq
23. 0023exact hk
24. 0024exact hchoose
25. 0025have hF_one : F = 1
26. 0026specialize factorial_zero 0
27. 0027specialize factorial_zero F
28. 0028apply factorial_zero
29. 0029refl
30. 0030exact hF
31. 0031have hK_one : K = 1
32. 0032specialize factorial_zero k
33. 0033specialize factorial_zero K
34. 0034apply factorial_zero
35. 0035exact hk
36. 0036exact hK
37. 0037have hJ_one : J = 1
38. 0038specialize factorial_zero 0
39. 0039specialize factorial_zero J
40. 0040apply factorial_zero
41. 0041refl
42. 0042exact hJ
43. 0043rewrite hF_one
44. 0044rewrite hK_one
45. 0045rewrite hJ_one
46. 0046rewrite hc_one
47. 0047specialize mul_one 1
48. 0048rewrite mul_one
49. 0049rewrite mul_one
50. 0050refl
51. 0051intro c
52. 0052intro F
53. 0053intro K
54. 0054intro J
55. 0055intro hsum
56. 0056rewrite PA4 at hsum
57. 0057exfalso
58. 0058apply PA1
59. 0059exact hsum
60. 0060intro k
61. 0061induction j
62. 0062intro c
63. 0063intro F
64. 0064intro K
65. 0065intro J
66. 0066intro hsum
67. 0067intro hchoose
68. 0068intro hF
69. 0069intro hK
70. 0070intro hJ
71. 0071have hk : k = S n
72. 0072trans k + 0
73. 0073symm
74. 0074apply PA3
75. 0075exact hsum
76. 0076have hc_one : c = 1
77. 0077specialize choose_self_of_eq (S n)
78. 0078specialize choose_self_of_eq k
79. 0079specialize choose_self_of_eq c
80. 0080apply choose_self_of_eq
81. 0081exact hk
82. 0082exact hchoose
83. 0083have hJ_one : J = 1
84. 0084specialize factorial_zero 0
85. 0085specialize factorial_zero J
86. 0086apply factorial_zero
87. 0087refl
88. 0088exact hJ
89. 0089have hFK : F = K
90. 0090specialize factorial_functional (S n)
91. 0091specialize factorial_functional F
92. 0092specialize factorial_functional K
93. 0093apply factorial_functional
94. 0094exact hF
95. 0095specialize factorial_length_eq_transport k
96. 0096specialize factorial_length_eq_transport (S n)
97. 0097specialize factorial_length_eq_transport K
98. 0098apply factorial_length_eq_transport
99. 0099exact hk
100. 0100exact hK
101. 0101rewrite hFK
102. 0102rewrite hJ_one
103. 0103rewrite hc_one
104. 0104specialize mul_one K
105. 0105rewrite mul_one
106. 0106rewrite mul_one
107. 0107refl
108. 0108intro c
109. 0109intro F
110. 0110intro K
111. 0111intro J
112. 0112intro hsum
113. 0113intro hchoose
114. 0114intro hF
115. 0115intro hK
116. 0116intro hJ
117. 0117have hprevious_sum : k + j = n
118. 0118apply PA2
119. 0119trans k + S j
120. 0120symm
121. 0121apply PA4
122. 0122exact hsum
123. 0123have ha_exists : exists a. (((exists bcf_lt_gap_bcfb_predecessor_choose_out_of_range. bcf_lt_gap_bcfb_predecessor_choose_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcfb_predecessor_choose_in_range. bcf_le_gap_bcfb_predecessor_choose_in_range + (k) = n) /\ (exists bcf_row_code_code_bcfb_predecessor_choose bcf_row_code_scale_bcfb_predecessor_choose bcf_row_scale_code_bcfb_predecessor_choose bcf_row_scale_scale_bcfb_predecessor_choose bcf_row_code_bcfb_predecessor_choose bcf_row_scale_bcfb_predecessor_choose. ((forall bcf_row_index_bcfb_predecessor_choose_table. (exists bcf_lt_gap_bcfb_predecessor_choose_table_row_bound. bcf_lt_gap_bcfb_predecessor_choose_table_row_bound + S (bcf_row_index_bcfb_predecessor_choose_table) = S (n)) -> exists bcf_row_code_bcfb_predecessor_choose_table bcf_row_scale_bcfb_predecessor_choose_table. ((((exists bcf_height_bcfb_predecessor_choose_table_decoded_row_code. bcf_height_bcfb_predecessor_choose_table_decoded_row_code + S (bcf_row_code_bcfb_predecessor_choose_table) = S ((S (bcf_row_index_bcfb_predecessor_choose_table)) * bcf_row_code_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_decoded_row_code. bcf_row_code_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_table_decoded_row_code * S ((S (bcf_row_index_bcfb_predecessor_choose_table)) * bcf_row_code_scale_bcfb_predecessor_choose) + (bcf_row_code_bcfb_predecessor_choose_table))) /\ ((((exists bcf_height_bcfb_predecessor_choose_table_decoded_row_scale. bcf_height_bcfb_predecessor_choose_table_decoded_row_scale + S (bcf_row_scale_bcfb_predecessor_choose_table) = S ((S (bcf_row_index_bcfb_predecessor_choose_table)) * bcf_row_scale_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_decoded_row_scale. bcf_row_scale_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_table_decoded_row_scale * S ((S (bcf_row_index_bcfb_predecessor_choose_table)) * bcf_row_scale_scale_bcfb_predecessor_choose) + (bcf_row_scale_bcfb_predecessor_choose_table))) /\ ((bcf_row_index_bcfb_predecessor_choose_table = 0 /\ (forall bcf_index_bcfb_predecessor_choose_table_zero_row. (exists bcf_lt_gap_bcfb_predecessor_choose_table_zero_row_bound. bcf_lt_gap_bcfb_predecessor_choose_table_zero_row_bound + S (bcf_index_bcfb_predecessor_choose_table_zero_row) = S (n)) -> exists bcf_value_bcfb_predecessor_choose_table_zero_row. ((((exists bcf_height_bcfb_predecessor_choose_table_zero_row_entry. bcf_height_bcfb_predecessor_choose_table_zero_row_entry + S (bcf_value_bcfb_predecessor_choose_table_zero_row) = S ((S (bcf_index_bcfb_predecessor_choose_table_zero_row)) * bcf_row_scale_bcfb_predecessor_choose_table)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_zero_row_entry. bcf_row_code_bcfb_predecessor_choose_table = bcf_quotient_bcfb_predecessor_choose_table_zero_row_entry * S ((S (bcf_index_bcfb_predecessor_choose_table_zero_row)) * bcf_row_scale_bcfb_predecessor_choose_table) + (bcf_value_bcfb_predecessor_choose_table_zero_row))) /\ ((bcf_index_bcfb_predecessor_choose_table_zero_row = 0 /\ bcf_value_bcfb_predecessor_choose_table_zero_row = 1) \/ exists bcf_predecessor_bcfb_predecessor_choose_table_zero_row. bcf_index_bcfb_predecessor_choose_table_zero_row = S bcf_predecessor_bcfb_predecessor_choose_table_zero_row /\ bcf_value_bcfb_predecessor_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bcfb_predecessor_choose_table bcf_previous_code_bcfb_predecessor_choose_table bcf_previous_scale_bcfb_predecessor_choose_table. bcf_row_index_bcfb_predecessor_choose_table = S bcf_predecessor_bcfb_predecessor_choose_table /\ ((((exists bcf_height_bcfb_predecessor_choose_table_decoded_previous_code. bcf_height_bcfb_predecessor_choose_table_decoded_previous_code + S (bcf_previous_code_bcfb_predecessor_choose_table) = S ((S (bcf_predecessor_bcfb_predecessor_choose_table)) * bcf_row_code_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_decoded_previous_code. bcf_row_code_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bcfb_predecessor_choose_table)) * bcf_row_code_scale_bcfb_predecessor_choose) + (bcf_previous_code_bcfb_predecessor_choose_table))) /\ ((((exists bcf_height_bcfb_predecessor_choose_table_decoded_previous_scale. bcf_height_bcfb_predecessor_choose_table_decoded_previous_scale + S (bcf_previous_scale_bcfb_predecessor_choose_table) = S ((S (bcf_predecessor_bcfb_predecessor_choose_table)) * bcf_row_scale_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_decoded_previous_scale. bcf_row_scale_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bcfb_predecessor_choose_table)) * bcf_row_scale_scale_bcfb_predecessor_choose) + (bcf_previous_scale_bcfb_predecessor_choose_table))) /\ (forall bcf_index_bcfb_predecessor_choose_table_row_step. (exists bcf_lt_gap_bcfb_predecessor_choose_table_row_step_bound. bcf_lt_gap_bcfb_predecessor_choose_table_row_step_bound + S (bcf_index_bcfb_predecessor_choose_table_row_step) = S (n)) -> exists bcf_value_bcfb_predecessor_choose_table_row_step. ((((exists bcf_height_bcfb_predecessor_choose_table_row_step_entry. bcf_height_bcfb_predecessor_choose_table_row_step_entry + S (bcf_value_bcfb_predecessor_choose_table_row_step) = S ((S (bcf_index_bcfb_predecessor_choose_table_row_step)) * bcf_row_scale_bcfb_predecessor_choose_table)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_row_step_entry. bcf_row_code_bcfb_predecessor_choose_table = bcf_quotient_bcfb_predecessor_choose_table_row_step_entry * S ((S (bcf_index_bcfb_predecessor_choose_table_row_step)) * bcf_row_scale_bcfb_predecessor_choose_table) + (bcf_value_bcfb_predecessor_choose_table_row_step))) /\ ((bcf_index_bcfb_predecessor_choose_table_row_step = 0 /\ bcf_value_bcfb_predecessor_choose_table_row_step = 1) \/ exists bcf_predecessor_bcfb_predecessor_choose_table_row_step bcf_left_bcfb_predecessor_choose_table_row_step bcf_right_bcfb_predecessor_choose_table_row_step. bcf_index_bcfb_predecessor_choose_table_row_step = S bcf_predecessor_bcfb_predecessor_choose_table_row_step /\ ((((exists bcf_height_bcfb_predecessor_choose_table_row_step_previous_left. bcf_height_bcfb_predecessor_choose_table_row_step_previous_left + S (bcf_left_bcfb_predecessor_choose_table_row_step) = S ((S (bcf_predecessor_bcfb_predecessor_choose_table_row_step)) * bcf_previous_scale_bcfb_predecessor_choose_table)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_row_step_previous_left. bcf_previous_code_bcfb_predecessor_choose_table = bcf_quotient_bcfb_predecessor_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bcfb_predecessor_choose_table_row_step)) * bcf_previous_scale_bcfb_predecessor_choose_table) + (bcf_left_bcfb_predecessor_choose_table_row_step))) /\ ((((exists bcf_height_bcfb_predecessor_choose_table_row_step_previous_right. bcf_height_bcfb_predecessor_choose_table_row_step_previous_right + S (bcf_right_bcfb_predecessor_choose_table_row_step) = S ((S (S (bcf_predecessor_bcfb_predecessor_choose_table_row_step))) * bcf_previous_scale_bcfb_predecessor_choose_table)) /\ exists bcf_quotient_bcfb_predecessor_choose_table_row_step_previous_right. bcf_previous_code_bcfb_predecessor_choose_table = bcf_quotient_bcfb_predecessor_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcfb_predecessor_choose_table_row_step))) * bcf_previous_scale_bcfb_predecessor_choose_table) + (bcf_right_bcfb_predecessor_choose_table_row_step))) /\ bcf_value_bcfb_predecessor_choose_table_row_step = bcf_left_bcfb_predecessor_choose_table_row_step + bcf_right_bcfb_predecessor_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bcfb_predecessor_choose_decoded_row_code. bcf_height_bcfb_predecessor_choose_decoded_row_code + S (bcf_row_code_bcfb_predecessor_choose) = S ((S (n)) * bcf_row_code_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_decoded_row_code. bcf_row_code_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcfb_predecessor_choose) + (bcf_row_code_bcfb_predecessor_choose))) /\ ((((exists bcf_height_bcfb_predecessor_choose_decoded_row_scale. bcf_height_bcfb_predecessor_choose_decoded_row_scale + S (bcf_row_scale_bcfb_predecessor_choose) = S ((S (n)) * bcf_row_scale_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_decoded_row_scale. bcf_row_scale_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcfb_predecessor_choose) + (bcf_row_scale_bcfb_predecessor_choose))) /\ (((exists bcf_height_bcfb_predecessor_choose_decoded_value. bcf_height_bcfb_predecessor_choose_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcfb_predecessor_choose)) /\ exists bcf_quotient_bcfb_predecessor_choose_decoded_value. bcf_row_code_bcfb_predecessor_choose = bcf_quotient_bcfb_predecessor_choose_decoded_value * S ((S (k)) * bcf_row_scale_bcfb_predecessor_choose) + (a)))))))))
124. 0124specialize choose_exists n
125. 0125specialize choose_exists k
126. 0126exact choose_exists
127. 0127cases ha_exists
128. 0128have hweighted : S j * c = S n * x
129. 0129specialize choose_weighted_vertical n
130. 0130specialize choose_weighted_vertical k
131. 0131specialize choose_weighted_vertical j
132. 0132specialize choose_weighted_vertical x
133. 0133specialize choose_weighted_vertical c
134. 0134apply choose_weighted_vertical
135. 0135exact hprevious_sum
136. 0136exact ha_exists_witness
137. 0137exact hchoose
138. 0138have hF_decomp : exists f. (exists ff_b_bcfb_predecessor_total ff_c_bcfb_predecessor_total. ((forall ff_i_bcfb_predecessor_total_range. (exists ff_lt_bcfb_predecessor_total_range_bound. ff_lt_bcfb_predecessor_total_range_bound + S ff_i_bcfb_predecessor_total_range = n) -> (((exists ff_h_bcfb_predecessor_total_range_decoded. ff_h_bcfb_predecessor_total_range_decoded + S (1 + ff_i_bcfb_predecessor_total_range) = S ((S (ff_i_bcfb_predecessor_total_range)) * ff_c_bcfb_predecessor_total)) /\ exists ff_q_bcfb_predecessor_total_range_decoded. ff_b_bcfb_predecessor_total = ff_q_bcfb_predecessor_total_range_decoded * S ((S (ff_i_bcfb_predecessor_total_range)) * ff_c_bcfb_predecessor_total) + (1 + ff_i_bcfb_predecessor_total_range)))) /\ (exists ff_u_bcfb_predecessor_total_product ff_v_bcfb_predecessor_total_product. ((((exists ff_h_bcfb_predecessor_total_product_start. ff_h_bcfb_predecessor_total_product_start + S (1) = S ((S (0)) * ff_v_bcfb_predecessor_total_product)) /\ exists ff_q_bcfb_predecessor_total_product_start. ff_u_bcfb_predecessor_total_product = ff_q_bcfb_predecessor_total_product_start * S ((S (0)) * ff_v_bcfb_predecessor_total_product) + (1))) /\ ((((exists ff_h_bcfb_predecessor_total_product_terminal. ff_h_bcfb_predecessor_total_product_terminal + S (f) = S ((S (n)) * ff_v_bcfb_predecessor_total_product)) /\ exists ff_q_bcfb_predecessor_total_product_terminal. ff_u_bcfb_predecessor_total_product = ff_q_bcfb_predecessor_total_product_terminal * S ((S (n)) * ff_v_bcfb_predecessor_total_product) + (f))) /\ forall ff_i_bcfb_predecessor_total_product. (exists ff_lt_bcfb_predecessor_total_product_bound. ff_lt_bcfb_predecessor_total_product_bound + S ff_i_bcfb_predecessor_total_product = n) -> exists ff_p_bcfb_predecessor_total_product ff_r_bcfb_predecessor_total_product ff_s_bcfb_predecessor_total_product. ((((exists ff_h_bcfb_predecessor_total_product_factor. ff_h_bcfb_predecessor_total_product_factor + S (ff_p_bcfb_predecessor_total_product) = S ((S (ff_i_bcfb_predecessor_total_product)) * ff_c_bcfb_predecessor_total)) /\ exists ff_q_bcfb_predecessor_total_product_factor. ff_b_bcfb_predecessor_total = ff_q_bcfb_predecessor_total_product_factor * S ((S (ff_i_bcfb_predecessor_total_product)) * ff_c_bcfb_predecessor_total) + (ff_p_bcfb_predecessor_total_product))) /\ ((((exists ff_h_bcfb_predecessor_total_product_partial. ff_h_bcfb_predecessor_total_product_partial + S (ff_r_bcfb_predecessor_total_product) = S ((S (ff_i_bcfb_predecessor_total_product)) * ff_v_bcfb_predecessor_total_product)) /\ exists ff_q_bcfb_predecessor_total_product_partial. ff_u_bcfb_predecessor_total_product = ff_q_bcfb_predecessor_total_product_partial * S ((S (ff_i_bcfb_predecessor_total_product)) * ff_v_bcfb_predecessor_total_product) + (ff_r_bcfb_predecessor_total_product))) /\ ((((exists ff_h_bcfb_predecessor_total_product_successor. ff_h_bcfb_predecessor_total_product_successor + S (ff_s_bcfb_predecessor_total_product) = S ((S (S ff_i_bcfb_predecessor_total_product)) * ff_v_bcfb_predecessor_total_product)) /\ exists ff_q_bcfb_predecessor_total_product_successor. ff_u_bcfb_predecessor_total_product = ff_q_bcfb_predecessor_total_product_successor * S ((S (S ff_i_bcfb_predecessor_total_product)) * ff_v_bcfb_predecessor_total_product) + (ff_s_bcfb_predecessor_total_product))) /\ ff_s_bcfb_predecessor_total_product = ff_r_bcfb_predecessor_total_product * ff_p_bcfb_predecessor_total_product)))))))) /\ F = f * S n
139. 0139specialize factorial_succ_decompose n
140. 0140specialize factorial_succ_decompose (S n)
141. 0141specialize factorial_succ_decompose F
142. 0142apply factorial_succ_decompose
143. 0143refl
144. 0144exact hF
145. 0145cases hF_decomp
146. 0146cases hF_decomp_witness
147. 0147have hJ_decomp : exists r. (exists ff_b_bcfb_predecessor_right ff_c_bcfb_predecessor_right. ((forall ff_i_bcfb_predecessor_right_range. (exists ff_lt_bcfb_predecessor_right_range_bound. ff_lt_bcfb_predecessor_right_range_bound + S ff_i_bcfb_predecessor_right_range = j) -> (((exists ff_h_bcfb_predecessor_right_range_decoded. ff_h_bcfb_predecessor_right_range_decoded + S (1 + ff_i_bcfb_predecessor_right_range) = S ((S (ff_i_bcfb_predecessor_right_range)) * ff_c_bcfb_predecessor_right)) /\ exists ff_q_bcfb_predecessor_right_range_decoded. ff_b_bcfb_predecessor_right = ff_q_bcfb_predecessor_right_range_decoded * S ((S (ff_i_bcfb_predecessor_right_range)) * ff_c_bcfb_predecessor_right) + (1 + ff_i_bcfb_predecessor_right_range)))) /\ (exists ff_u_bcfb_predecessor_right_product ff_v_bcfb_predecessor_right_product. ((((exists ff_h_bcfb_predecessor_right_product_start. ff_h_bcfb_predecessor_right_product_start + S (1) = S ((S (0)) * ff_v_bcfb_predecessor_right_product)) /\ exists ff_q_bcfb_predecessor_right_product_start. ff_u_bcfb_predecessor_right_product = ff_q_bcfb_predecessor_right_product_start * S ((S (0)) * ff_v_bcfb_predecessor_right_product) + (1))) /\ ((((exists ff_h_bcfb_predecessor_right_product_terminal. ff_h_bcfb_predecessor_right_product_terminal + S (r) = S ((S (j)) * ff_v_bcfb_predecessor_right_product)) /\ exists ff_q_bcfb_predecessor_right_product_terminal. ff_u_bcfb_predecessor_right_product = ff_q_bcfb_predecessor_right_product_terminal * S ((S (j)) * ff_v_bcfb_predecessor_right_product) + (r))) /\ forall ff_i_bcfb_predecessor_right_product. (exists ff_lt_bcfb_predecessor_right_product_bound. ff_lt_bcfb_predecessor_right_product_bound + S ff_i_bcfb_predecessor_right_product = j) -> exists ff_p_bcfb_predecessor_right_product ff_r_bcfb_predecessor_right_product ff_s_bcfb_predecessor_right_product. ((((exists ff_h_bcfb_predecessor_right_product_factor. ff_h_bcfb_predecessor_right_product_factor + S (ff_p_bcfb_predecessor_right_product) = S ((S (ff_i_bcfb_predecessor_right_product)) * ff_c_bcfb_predecessor_right)) /\ exists ff_q_bcfb_predecessor_right_product_factor. ff_b_bcfb_predecessor_right = ff_q_bcfb_predecessor_right_product_factor * S ((S (ff_i_bcfb_predecessor_right_product)) * ff_c_bcfb_predecessor_right) + (ff_p_bcfb_predecessor_right_product))) /\ ((((exists ff_h_bcfb_predecessor_right_product_partial. ff_h_bcfb_predecessor_right_product_partial + S (ff_r_bcfb_predecessor_right_product) = S ((S (ff_i_bcfb_predecessor_right_product)) * ff_v_bcfb_predecessor_right_product)) /\ exists ff_q_bcfb_predecessor_right_product_partial. ff_u_bcfb_predecessor_right_product = ff_q_bcfb_predecessor_right_product_partial * S ((S (ff_i_bcfb_predecessor_right_product)) * ff_v_bcfb_predecessor_right_product) + (ff_r_bcfb_predecessor_right_product))) /\ ((((exists ff_h_bcfb_predecessor_right_product_successor. ff_h_bcfb_predecessor_right_product_successor + S (ff_s_bcfb_predecessor_right_product) = S ((S (S ff_i_bcfb_predecessor_right_product)) * ff_v_bcfb_predecessor_right_product)) /\ exists ff_q_bcfb_predecessor_right_product_successor. ff_u_bcfb_predecessor_right_product = ff_q_bcfb_predecessor_right_product_successor * S ((S (S ff_i_bcfb_predecessor_right_product)) * ff_v_bcfb_predecessor_right_product) + (ff_s_bcfb_predecessor_right_product))) /\ ff_s_bcfb_predecessor_right_product = ff_r_bcfb_predecessor_right_product * ff_p_bcfb_predecessor_right_product)))))))) /\ J = r * S j
148. 0148specialize factorial_succ_decompose j
149. 0149specialize factorial_succ_decompose (S j)
150. 0150specialize factorial_succ_decompose J
151. 0151apply factorial_succ_decompose
152. 0152refl
153. 0153exact hJ
154. 0154cases hJ_decomp
155. 0155cases hJ_decomp_witness
156. 0156have hbridge : x1 = (K * x2) * x
157. 0157specialize IH k
158. 0158specialize IH j
159. 0159specialize IH x
160. 0160specialize IH x1
161. 0161specialize IH K
162. 0162specialize IH x2
163. 0163apply IH
164. 0164exact hprevious_sum
165. 0165exact ha_exists_witness
166. 0166exact hF_decomp_witness_left
167. 0167exact hK
168. 0168exact hJ_decomp_witness_left
169. 0169specialize factorial_weighted_product_combine (S j)
170. 0170specialize factorial_weighted_product_combine (S n)
171. 0171specialize factorial_weighted_product_combine x
172. 0172specialize factorial_weighted_product_combine c
173. 0173specialize factorial_weighted_product_combine x1
174. 0174specialize factorial_weighted_product_combine K
175. 0175specialize factorial_weighted_product_combine x2
176. 0176specialize factorial_weighted_product_combine F
177. 0177specialize factorial_weighted_product_combine J
178. 0178apply factorial_weighted_product_combine
179. 0179exact hJ_decomp_witness_right
180. 0180exact hF_decomp_witness_right
181. 0181exact hweighted
182. 0182exact hbridge