beta_range_two_product_is_factorial_succ

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

1. 0001intro l
2. 0002induction l
3. 0003intro b
4. 0004intro c
5. 0005intro P
6. 0006intro hrange
7. 0007intro hproduct
8. 0008have hpone : P = 1
9. 0009specialize beta_product_zero b
10. 0010specialize beta_product_zero c
11. 0011specialize beta_product_zero P
12. 0012apply beta_product_zero
13. 0013exact hproduct
14. 0014have hfactorial : exists F. (exists wer_factor_code_wer_factorial_one_F wer_factor_scale_wer_factorial_one_F. ((forall wer_range_index_wer_factorial_one_F_range. (exists wer_range_gap_wer_factorial_one_F_range. wer_range_gap_wer_factorial_one_F_range + S wer_range_index_wer_factorial_one_F_range = 1) -> (((exists ff_h_wer_factorial_one_F_range_decoded. ff_h_wer_factorial_one_F_range_decoded + S (1 + wer_range_index_wer_factorial_one_F_range) = S ((S (wer_range_index_wer_factorial_one_F_range)) * wer_factor_scale_wer_factorial_one_F)) /\ exists ff_q_wer_factorial_one_F_range_decoded. wer_factor_code_wer_factorial_one_F = ff_q_wer_factorial_one_F_range_decoded * S ((S (wer_range_index_wer_factorial_one_F_range)) * wer_factor_scale_wer_factorial_one_F) + (1 + wer_range_index_wer_factorial_one_F_range)))) /\ (exists ff_u_wer_factorial_one_F_product ff_v_wer_factorial_one_F_product. ((((exists ff_h_wer_factorial_one_F_product_start. ff_h_wer_factorial_one_F_product_start + S (1) = S ((S (0)) * ff_v_wer_factorial_one_F_product)) /\ exists ff_q_wer_factorial_one_F_product_start. ff_u_wer_factorial_one_F_product = ff_q_wer_factorial_one_F_product_start * S ((S (0)) * ff_v_wer_factorial_one_F_product) + (1))) /\ ((((exists ff_h_wer_factorial_one_F_product_terminal. ff_h_wer_factorial_one_F_product_terminal + S (F) = S ((S (1)) * ff_v_wer_factorial_one_F_product)) /\ exists ff_q_wer_factorial_one_F_product_terminal. ff_u_wer_factorial_one_F_product = ff_q_wer_factorial_one_F_product_terminal * S ((S (1)) * ff_v_wer_factorial_one_F_product) + (F))) /\ forall ff_i_wer_factorial_one_F_product. (exists ff_lt_wer_factorial_one_F_product_bound. ff_lt_wer_factorial_one_F_product_bound + S ff_i_wer_factorial_one_F_product = 1) -> exists ff_p_wer_factorial_one_F_product ff_r_wer_factorial_one_F_product ff_s_wer_factorial_one_F_product. ((((exists ff_h_wer_factorial_one_F_product_factor. ff_h_wer_factorial_one_F_product_factor + S (ff_p_wer_factorial_one_F_product) = S ((S (ff_i_wer_factorial_one_F_product)) * wer_factor_scale_wer_factorial_one_F)) /\ exists ff_q_wer_factorial_one_F_product_factor. wer_factor_code_wer_factorial_one_F = ff_q_wer_factorial_one_F_product_factor * S ((S (ff_i_wer_factorial_one_F_product)) * wer_factor_scale_wer_factorial_one_F) + (ff_p_wer_factorial_one_F_product))) /\ ((((exists ff_h_wer_factorial_one_F_product_partial. ff_h_wer_factorial_one_F_product_partial + S (ff_r_wer_factorial_one_F_product) = S ((S (ff_i_wer_factorial_one_F_product)) * ff_v_wer_factorial_one_F_product)) /\ exists ff_q_wer_factorial_one_F_product_partial. ff_u_wer_factorial_one_F_product = ff_q_wer_factorial_one_F_product_partial * S ((S (ff_i_wer_factorial_one_F_product)) * ff_v_wer_factorial_one_F_product) + (ff_r_wer_factorial_one_F_product))) /\ ((((exists ff_h_wer_factorial_one_F_product_successor. ff_h_wer_factorial_one_F_product_successor + S (ff_s_wer_factorial_one_F_product) = S ((S (S ff_i_wer_factorial_one_F_product)) * ff_v_wer_factorial_one_F_product)) /\ exists ff_q_wer_factorial_one_F_product_successor. ff_u_wer_factorial_one_F_product = ff_q_wer_factorial_one_F_product_successor * S ((S (S ff_i_wer_factorial_one_F_product)) * ff_v_wer_factorial_one_F_product) + (ff_s_wer_factorial_one_F_product))) /\ ff_s_wer_factorial_one_F_product = ff_r_wer_factorial_one_F_product * ff_p_wer_factorial_one_F_product))))))))
15. 0015specialize factorial_exists 1
16. 0016exact factorial_exists
17. 0017cases hfactorial
18. 0018have hfone : x = 1
19. 0019specialize factorial_one_value 1
20. 0020specialize factorial_one_value x
21. 0021apply factorial_one_value
22. 0022refl
23. 0023exact hfactorial_witness
24. 0024have hpx : P = x
25. 0025trans 1
26. 0026exact hpone
27. 0027symm
28. 0028exact hfone
29. 0029rewrite hpx
30. 0030rewrite hpx
31. 0031exact hfactorial_witness
32. 0032intro b
33. 0033intro c
34. 0034intro P
35. 0035intro hrange
36. 0036intro hproduct
37. 0037have hrange_prefix : forall wtp_range_index_wer_step_prefix_range. (exists wtp_range_gap_wer_step_prefix_range. wtp_range_gap_wer_step_prefix_range + S wtp_range_index_wer_step_prefix_range = l) -> (((exists ff_h_wer_step_prefix_range_decoded. ff_h_wer_step_prefix_range_decoded + S (2 + wtp_range_index_wer_step_prefix_range) = S ((S (wtp_range_index_wer_step_prefix_range)) * c)) /\ exists ff_q_wer_step_prefix_range_decoded. b = ff_q_wer_step_prefix_range_decoded * S ((S (wtp_range_index_wer_step_prefix_range)) * c) + (2 + wtp_range_index_wer_step_prefix_range)))
38. 0038intro i
39. 0039intro hi
40. 0040specialize hrange i
41. 0041apply hrange
42. 0042specialize le_succ (S i)
43. 0043specialize le_succ l
44. 0044apply le_succ
45. 0045exact hi
46. 0046have hdecomp : exists x x1. ((((exists ff_h_wer_step_factor. ff_h_wer_step_factor + S (x) = S ((S (l)) * c)) /\ exists ff_q_wer_step_factor. b = ff_q_wer_step_factor * S ((S (l)) * c) + (x))) /\ ((exists ff_u_wer_step_prefix_product ff_v_wer_step_prefix_product. ((((exists ff_h_wer_step_prefix_product_start. ff_h_wer_step_prefix_product_start + S (1) = S ((S (0)) * ff_v_wer_step_prefix_product)) /\ exists ff_q_wer_step_prefix_product_start. ff_u_wer_step_prefix_product = ff_q_wer_step_prefix_product_start * S ((S (0)) * ff_v_wer_step_prefix_product) + (1))) /\ ((((exists ff_h_wer_step_prefix_product_terminal. ff_h_wer_step_prefix_product_terminal + S (x1) = S ((S (l)) * ff_v_wer_step_prefix_product)) /\ exists ff_q_wer_step_prefix_product_terminal. ff_u_wer_step_prefix_product = ff_q_wer_step_prefix_product_terminal * S ((S (l)) * ff_v_wer_step_prefix_product) + (x1))) /\ forall ff_i_wer_step_prefix_product. (exists ff_lt_wer_step_prefix_product_bound. ff_lt_wer_step_prefix_product_bound + S ff_i_wer_step_prefix_product = l) -> exists ff_p_wer_step_prefix_product ff_r_wer_step_prefix_product ff_s_wer_step_prefix_product. ((((exists ff_h_wer_step_prefix_product_factor. ff_h_wer_step_prefix_product_factor + S (ff_p_wer_step_prefix_product) = S ((S (ff_i_wer_step_prefix_product)) * c)) /\ exists ff_q_wer_step_prefix_product_factor. b = ff_q_wer_step_prefix_product_factor * S ((S (ff_i_wer_step_prefix_product)) * c) + (ff_p_wer_step_prefix_product))) /\ ((((exists ff_h_wer_step_prefix_product_partial. ff_h_wer_step_prefix_product_partial + S (ff_r_wer_step_prefix_product) = S ((S (ff_i_wer_step_prefix_product)) * ff_v_wer_step_prefix_product)) /\ exists ff_q_wer_step_prefix_product_partial. ff_u_wer_step_prefix_product = ff_q_wer_step_prefix_product_partial * S ((S (ff_i_wer_step_prefix_product)) * ff_v_wer_step_prefix_product) + (ff_r_wer_step_prefix_product))) /\ ((((exists ff_h_wer_step_prefix_product_successor. ff_h_wer_step_prefix_product_successor + S (ff_s_wer_step_prefix_product) = S ((S (S ff_i_wer_step_prefix_product)) * ff_v_wer_step_prefix_product)) /\ exists ff_q_wer_step_prefix_product_successor. ff_u_wer_step_prefix_product = ff_q_wer_step_prefix_product_successor * S ((S (S ff_i_wer_step_prefix_product)) * ff_v_wer_step_prefix_product) + (ff_s_wer_step_prefix_product))) /\ ff_s_wer_step_prefix_product = ff_r_wer_step_prefix_product * ff_p_wer_step_prefix_product)))))) /\ P = x1 * x))
47. 0047specialize beta_product_succ_decompose b
48. 0048specialize beta_product_succ_decompose c
49. 0049specialize beta_product_succ_decompose l
50. 0050specialize beta_product_succ_decompose P
51. 0051apply beta_product_succ_decompose
52. 0052exact hproduct
53. 0053cases hdecomp
54. 0054cases hdecomp_witness
55. 0055cases hdecomp_witness_witness
56. 0056cases hdecomp_witness_witness_right
57. 0057have hprefix_factorial : exists wer_factor_code_wer_step_prefix_factorial wer_factor_scale_wer_step_prefix_factorial. ((forall wer_range_index_wer_step_prefix_factorial_range. (exists wer_range_gap_wer_step_prefix_factorial_range. wer_range_gap_wer_step_prefix_factorial_range + S wer_range_index_wer_step_prefix_factorial_range = S l) -> (((exists ff_h_wer_step_prefix_factorial_range_decoded. ff_h_wer_step_prefix_factorial_range_decoded + S (1 + wer_range_index_wer_step_prefix_factorial_range) = S ((S (wer_range_index_wer_step_prefix_factorial_range)) * wer_factor_scale_wer_step_prefix_factorial)) /\ exists ff_q_wer_step_prefix_factorial_range_decoded. wer_factor_code_wer_step_prefix_factorial = ff_q_wer_step_prefix_factorial_range_decoded * S ((S (wer_range_index_wer_step_prefix_factorial_range)) * wer_factor_scale_wer_step_prefix_factorial) + (1 + wer_range_index_wer_step_prefix_factorial_range)))) /\ (exists ff_u_wer_step_prefix_factorial_product ff_v_wer_step_prefix_factorial_product. ((((exists ff_h_wer_step_prefix_factorial_product_start. ff_h_wer_step_prefix_factorial_product_start + S (1) = S ((S (0)) * ff_v_wer_step_prefix_factorial_product)) /\ exists ff_q_wer_step_prefix_factorial_product_start. ff_u_wer_step_prefix_factorial_product = ff_q_wer_step_prefix_factorial_product_start * S ((S (0)) * ff_v_wer_step_prefix_factorial_product) + (1))) /\ ((((exists ff_h_wer_step_prefix_factorial_product_terminal. ff_h_wer_step_prefix_factorial_product_terminal + S (x1) = S ((S (S l)) * ff_v_wer_step_prefix_factorial_product)) /\ exists ff_q_wer_step_prefix_factorial_product_terminal. ff_u_wer_step_prefix_factorial_product = ff_q_wer_step_prefix_factorial_product_terminal * S ((S (S l)) * ff_v_wer_step_prefix_factorial_product) + (x1))) /\ forall ff_i_wer_step_prefix_factorial_product. (exists ff_lt_wer_step_prefix_factorial_product_bound. ff_lt_wer_step_prefix_factorial_product_bound + S ff_i_wer_step_prefix_factorial_product = S l) -> exists ff_p_wer_step_prefix_factorial_product ff_r_wer_step_prefix_factorial_product ff_s_wer_step_prefix_factorial_product. ((((exists ff_h_wer_step_prefix_factorial_product_factor. ff_h_wer_step_prefix_factorial_product_factor + S (ff_p_wer_step_prefix_factorial_product) = S ((S (ff_i_wer_step_prefix_factorial_product)) * wer_factor_scale_wer_step_prefix_factorial)) /\ exists ff_q_wer_step_prefix_factorial_product_factor. wer_factor_code_wer_step_prefix_factorial = ff_q_wer_step_prefix_factorial_product_factor * S ((S (ff_i_wer_step_prefix_factorial_product)) * wer_factor_scale_wer_step_prefix_factorial) + (ff_p_wer_step_prefix_factorial_product))) /\ ((((exists ff_h_wer_step_prefix_factorial_product_partial. ff_h_wer_step_prefix_factorial_product_partial + S (ff_r_wer_step_prefix_factorial_product) = S ((S (ff_i_wer_step_prefix_factorial_product)) * ff_v_wer_step_prefix_factorial_product)) /\ exists ff_q_wer_step_prefix_factorial_product_partial. ff_u_wer_step_prefix_factorial_product = ff_q_wer_step_prefix_factorial_product_partial * S ((S (ff_i_wer_step_prefix_factorial_product)) * ff_v_wer_step_prefix_factorial_product) + (ff_r_wer_step_prefix_factorial_product))) /\ ((((exists ff_h_wer_step_prefix_factorial_product_successor. ff_h_wer_step_prefix_factorial_product_successor + S (ff_s_wer_step_prefix_factorial_product) = S ((S (S ff_i_wer_step_prefix_factorial_product)) * ff_v_wer_step_prefix_factorial_product)) /\ exists ff_q_wer_step_prefix_factorial_product_successor. ff_u_wer_step_prefix_factorial_product = ff_q_wer_step_prefix_factorial_product_successor * S ((S (S ff_i_wer_step_prefix_factorial_product)) * ff_v_wer_step_prefix_factorial_product) + (ff_s_wer_step_prefix_factorial_product))) /\ ff_s_wer_step_prefix_factorial_product = ff_r_wer_step_prefix_factorial_product * ff_p_wer_step_prefix_factorial_product)))))))
58. 0058specialize IH b
59. 0059specialize IH c
60. 0060specialize IH x1
61. 0061apply IH
62. 0062exact hrange_prefix
63. 0063exact hdecomp_witness_witness_right_left
64. 0064have hfactor_value : x = S (S l)
65. 0065have hfactor_raw : x = 2 + l
66. 0066specialize beta_range_entry_eq b
67. 0067specialize beta_range_entry_eq c
68. 0068specialize beta_range_entry_eq 2
69. 0069specialize beta_range_entry_eq (S l)
70. 0070specialize beta_range_entry_eq l
71. 0071specialize beta_range_entry_eq x
72. 0072apply beta_range_entry_eq
73. 0073exact hrange
74. 0074specialize le_refl (S l)
75. 0075exact le_refl
76. 0076exact hdecomp_witness_witness_left
77. 0077trans 2 + l
78. 0078exact hfactor_raw
79. 0079simp [add_succ_left, zero_add]
80. 0080have hfull_factorial : exists F. (exists wer_factor_code_wer_step_full_factorial_F wer_factor_scale_wer_step_full_factorial_F. ((forall wer_range_index_wer_step_full_factorial_F_range. (exists wer_range_gap_wer_step_full_factorial_F_range. wer_range_gap_wer_step_full_factorial_F_range + S wer_range_index_wer_step_full_factorial_F_range = S (S l)) -> (((exists ff_h_wer_step_full_factorial_F_range_decoded. ff_h_wer_step_full_factorial_F_range_decoded + S (1 + wer_range_index_wer_step_full_factorial_F_range) = S ((S (wer_range_index_wer_step_full_factorial_F_range)) * wer_factor_scale_wer_step_full_factorial_F)) /\ exists ff_q_wer_step_full_factorial_F_range_decoded. wer_factor_code_wer_step_full_factorial_F = ff_q_wer_step_full_factorial_F_range_decoded * S ((S (wer_range_index_wer_step_full_factorial_F_range)) * wer_factor_scale_wer_step_full_factorial_F) + (1 + wer_range_index_wer_step_full_factorial_F_range)))) /\ (exists ff_u_wer_step_full_factorial_F_product ff_v_wer_step_full_factorial_F_product. ((((exists ff_h_wer_step_full_factorial_F_product_start. ff_h_wer_step_full_factorial_F_product_start + S (1) = S ((S (0)) * ff_v_wer_step_full_factorial_F_product)) /\ exists ff_q_wer_step_full_factorial_F_product_start. ff_u_wer_step_full_factorial_F_product = ff_q_wer_step_full_factorial_F_product_start * S ((S (0)) * ff_v_wer_step_full_factorial_F_product) + (1))) /\ ((((exists ff_h_wer_step_full_factorial_F_product_terminal. ff_h_wer_step_full_factorial_F_product_terminal + S (F) = S ((S (S (S l))) * ff_v_wer_step_full_factorial_F_product)) /\ exists ff_q_wer_step_full_factorial_F_product_terminal. ff_u_wer_step_full_factorial_F_product = ff_q_wer_step_full_factorial_F_product_terminal * S ((S (S (S l))) * ff_v_wer_step_full_factorial_F_product) + (F))) /\ forall ff_i_wer_step_full_factorial_F_product. (exists ff_lt_wer_step_full_factorial_F_product_bound. ff_lt_wer_step_full_factorial_F_product_bound + S ff_i_wer_step_full_factorial_F_product = S (S l)) -> exists ff_p_wer_step_full_factorial_F_product ff_r_wer_step_full_factorial_F_product ff_s_wer_step_full_factorial_F_product. ((((exists ff_h_wer_step_full_factorial_F_product_factor. ff_h_wer_step_full_factorial_F_product_factor + S (ff_p_wer_step_full_factorial_F_product) = S ((S (ff_i_wer_step_full_factorial_F_product)) * wer_factor_scale_wer_step_full_factorial_F)) /\ exists ff_q_wer_step_full_factorial_F_product_factor. wer_factor_code_wer_step_full_factorial_F = ff_q_wer_step_full_factorial_F_product_factor * S ((S (ff_i_wer_step_full_factorial_F_product)) * wer_factor_scale_wer_step_full_factorial_F) + (ff_p_wer_step_full_factorial_F_product))) /\ ((((exists ff_h_wer_step_full_factorial_F_product_partial. ff_h_wer_step_full_factorial_F_product_partial + S (ff_r_wer_step_full_factorial_F_product) = S ((S (ff_i_wer_step_full_factorial_F_product)) * ff_v_wer_step_full_factorial_F_product)) /\ exists ff_q_wer_step_full_factorial_F_product_partial. ff_u_wer_step_full_factorial_F_product = ff_q_wer_step_full_factorial_F_product_partial * S ((S (ff_i_wer_step_full_factorial_F_product)) * ff_v_wer_step_full_factorial_F_product) + (ff_r_wer_step_full_factorial_F_product))) /\ ((((exists ff_h_wer_step_full_factorial_F_product_successor. ff_h_wer_step_full_factorial_F_product_successor + S (ff_s_wer_step_full_factorial_F_product) = S ((S (S ff_i_wer_step_full_factorial_F_product)) * ff_v_wer_step_full_factorial_F_product)) /\ exists ff_q_wer_step_full_factorial_F_product_successor. ff_u_wer_step_full_factorial_F_product = ff_q_wer_step_full_factorial_F_product_successor * S ((S (S ff_i_wer_step_full_factorial_F_product)) * ff_v_wer_step_full_factorial_F_product) + (ff_s_wer_step_full_factorial_F_product))) /\ ff_s_wer_step_full_factorial_F_product = ff_r_wer_step_full_factorial_F_product * ff_p_wer_step_full_factorial_F_product))))))))
81. 0081specialize factorial_exists (S (S l))
82. 0082exact factorial_exists
83. 0083cases hfull_factorial
84. 0084have hfactorial_decomp : exists x3. ((exists wer_factor_code_wer_step_previous_factorial wer_factor_scale_wer_step_previous_factorial. ((forall wer_range_index_wer_step_previous_factorial_range. (exists wer_range_gap_wer_step_previous_factorial_range. wer_range_gap_wer_step_previous_factorial_range + S wer_range_index_wer_step_previous_factorial_range = S l) -> (((exists ff_h_wer_step_previous_factorial_range_decoded. ff_h_wer_step_previous_factorial_range_decoded + S (1 + wer_range_index_wer_step_previous_factorial_range) = S ((S (wer_range_index_wer_step_previous_factorial_range)) * wer_factor_scale_wer_step_previous_factorial)) /\ exists ff_q_wer_step_previous_factorial_range_decoded. wer_factor_code_wer_step_previous_factorial = ff_q_wer_step_previous_factorial_range_decoded * S ((S (wer_range_index_wer_step_previous_factorial_range)) * wer_factor_scale_wer_step_previous_factorial) + (1 + wer_range_index_wer_step_previous_factorial_range)))) /\ (exists ff_u_wer_step_previous_factorial_product ff_v_wer_step_previous_factorial_product. ((((exists ff_h_wer_step_previous_factorial_product_start. ff_h_wer_step_previous_factorial_product_start + S (1) = S ((S (0)) * ff_v_wer_step_previous_factorial_product)) /\ exists ff_q_wer_step_previous_factorial_product_start. ff_u_wer_step_previous_factorial_product = ff_q_wer_step_previous_factorial_product_start * S ((S (0)) * ff_v_wer_step_previous_factorial_product) + (1))) /\ ((((exists ff_h_wer_step_previous_factorial_product_terminal. ff_h_wer_step_previous_factorial_product_terminal + S (x3) = S ((S (S l)) * ff_v_wer_step_previous_factorial_product)) /\ exists ff_q_wer_step_previous_factorial_product_terminal. ff_u_wer_step_previous_factorial_product = ff_q_wer_step_previous_factorial_product_terminal * S ((S (S l)) * ff_v_wer_step_previous_factorial_product) + (x3))) /\ forall ff_i_wer_step_previous_factorial_product. (exists ff_lt_wer_step_previous_factorial_product_bound. ff_lt_wer_step_previous_factorial_product_bound + S ff_i_wer_step_previous_factorial_product = S l) -> exists ff_p_wer_step_previous_factorial_product ff_r_wer_step_previous_factorial_product ff_s_wer_step_previous_factorial_product. ((((exists ff_h_wer_step_previous_factorial_product_factor. ff_h_wer_step_previous_factorial_product_factor + S (ff_p_wer_step_previous_factorial_product) = S ((S (ff_i_wer_step_previous_factorial_product)) * wer_factor_scale_wer_step_previous_factorial)) /\ exists ff_q_wer_step_previous_factorial_product_factor. wer_factor_code_wer_step_previous_factorial = ff_q_wer_step_previous_factorial_product_factor * S ((S (ff_i_wer_step_previous_factorial_product)) * wer_factor_scale_wer_step_previous_factorial) + (ff_p_wer_step_previous_factorial_product))) /\ ((((exists ff_h_wer_step_previous_factorial_product_partial. ff_h_wer_step_previous_factorial_product_partial + S (ff_r_wer_step_previous_factorial_product) = S ((S (ff_i_wer_step_previous_factorial_product)) * ff_v_wer_step_previous_factorial_product)) /\ exists ff_q_wer_step_previous_factorial_product_partial. ff_u_wer_step_previous_factorial_product = ff_q_wer_step_previous_factorial_product_partial * S ((S (ff_i_wer_step_previous_factorial_product)) * ff_v_wer_step_previous_factorial_product) + (ff_r_wer_step_previous_factorial_product))) /\ ((((exists ff_h_wer_step_previous_factorial_product_successor. ff_h_wer_step_previous_factorial_product_successor + S (ff_s_wer_step_previous_factorial_product) = S ((S (S ff_i_wer_step_previous_factorial_product)) * ff_v_wer_step_previous_factorial_product)) /\ exists ff_q_wer_step_previous_factorial_product_successor. ff_u_wer_step_previous_factorial_product = ff_q_wer_step_previous_factorial_product_successor * S ((S (S ff_i_wer_step_previous_factorial_product)) * ff_v_wer_step_previous_factorial_product) + (ff_s_wer_step_previous_factorial_product))) /\ ff_s_wer_step_previous_factorial_product = ff_r_wer_step_previous_factorial_product * ff_p_wer_step_previous_factorial_product)))))))) /\ x2 = x3 * S (S l))
85. 0085specialize factorial_succ_decompose (S l)
86. 0086specialize factorial_succ_decompose (S (S l))
87. 0087specialize factorial_succ_decompose x2
88. 0088apply factorial_succ_decompose
89. 0089refl
90. 0090exact hfull_factorial_witness
91. 0091cases hfactorial_decomp
92. 0092cases hfactorial_decomp_witness
93. 0093have hprefix_eq : x1 = x3
94. 0094specialize factorial_functional (S l)
95. 0095specialize factorial_functional x1
96. 0096specialize factorial_functional x3
97. 0097apply factorial_functional
98. 0098exact hprefix_factorial
99. 0099exact hfactorial_decomp_witness_left
100. 0100have hproduct_eq : P = x2
101. 0101trans x1 * x
102. 0102exact hdecomp_witness_witness_right_right
103. 0103trans x1 * S (S l)
104. 0104apply mul_congr
105. 0105refl
106. 0106exact hfactor_value
107. 0107trans x3 * S (S l)
108. 0108apply mul_congr
109. 0109exact hprefix_eq
110. 0110refl
111. 0111symm
112. 0112exact hfactorial_decomp_witness_right
113. 0113rewrite hproduct_eq
114. 0114rewrite hproduct_eq
115. 0115exact hfull_factorial_witness