Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ n. ∀ k. ∀ j. ∀ p. ∀ C. k + j = n → Prime(p) → Choose(n,k,C) → Dvd(p,C) → Le(p,n)Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
Exact expanded first-order statement
forall n k j p C. k + j = n -> ((~(p = 1) /\ forall frm_prime_left_lucas_bound_prime frm_prime_right_lucas_bound_prime. p = frm_prime_left_lucas_bound_prime * frm_prime_right_lucas_bound_prime -> frm_prime_left_lucas_bound_prime = 1 \/ frm_prime_right_lucas_bound_prime = 1)) -> (((exists bcf_lt_gap_lucas_bound_choose_out_of_range. bcf_lt_gap_lucas_bound_choose_out_of_range + S (n) = k) /\ C = 0) \/ ((exists bcf_le_gap_lucas_bound_choose_in_range. bcf_le_gap_lucas_bound_choose_in_range + (k) = n) /\ (exists bcf_row_code_code_lucas_bound_choose bcf_row_code_scale_lucas_bound_choose bcf_row_scale_code_lucas_bound_choose bcf_row_scale_scale_lucas_bound_choose bcf_row_code_lucas_bound_choose bcf_row_scale_lucas_bound_choose. ((forall bcf_row_index_lucas_bound_choose_table. (exists bcf_lt_gap_lucas_bound_choose_table_row_bound. bcf_lt_gap_lucas_bound_choose_table_row_bound + S (bcf_row_index_lucas_bound_choose_table) = S (n)) -> exists bcf_row_code_lucas_bound_choose_table bcf_row_scale_lucas_bound_choose_table. ((((exists bcf_height_lucas_bound_choose_table_decoded_row_code. bcf_height_lucas_bound_choose_table_decoded_row_code + S (bcf_row_code_lucas_bound_choose_table) = S ((S (bcf_row_index_lucas_bound_choose_table)) * bcf_row_code_scale_lucas_bound_choose)) /\ exists bcf_quotient_lucas_bound_choose_table_decoded_row_code. bcf_row_code_code_lucas_bound_choose = bcf_quotient_lucas_bound_choose_table_decoded_row_code * S ((S (bcf_row_index_lucas_bound_choose_table)) * bcf_row_code_scale_lucas_bound_choose) + (bcf_row_code_lucas_bound_choose_table))) /\ ((((exists bcf_height_lucas_bound_choose_table_decoded_row_scale. bcf_height_lucas_bound_choose_table_decoded_row_scale + S (bcf_row_scale_lucas_bound_choose_table) = S ((S (bcf_row_index_lucas_bound_choose_table)) * bcf_row_scale_scale_lucas_bound_choose)) /\ exists bcf_quotient_lucas_bound_choose_table_decoded_row_scale. bcf_row_scale_code_lucas_bound_choose = bcf_quotient_lucas_bound_choose_table_decoded_row_scale * S ((S (bcf_row_index_lucas_bound_choose_table)) * bcf_row_scale_scale_lucas_bound_choose) + (bcf_row_scale_lucas_bound_choose_table))) /\ ((bcf_row_index_lucas_bound_choose_table = 0 /\ (forall bcf_index_lucas_bound_choose_table_zero_row. (exists bcf_lt_gap_lucas_bound_choose_table_zero_row_bound. bcf_lt_gap_lucas_bound_choose_table_zero_row_bound + S (bcf_index_lucas_bound_choose_table_zero_row) = S (n)) -> exists bcf_value_lucas_bound_choose_table_zero_row. ((((exists bcf_height_lucas_bound_choose_table_zero_row_entry. bcf_height_lucas_bound_choose_table_zero_row_entry + S (bcf_value_lucas_bound_choose_table_zero_row) = S ((S (bcf_index_lucas_bound_choose_table_zero_row)) * bcf_row_scale_lucas_bound_choose_table)) /\ exists bcf_quotient_lucas_bound_choose_table_zero_row_entry. bcf_row_code_lucas_bound_choose_table = bcf_quotient_lucas_bound_choose_table_zero_row_entry * S ((S (bcf_index_lucas_bound_choose_table_zero_row)) * bcf_row_scale_lucas_bound_choose_table) + (bcf_value_lucas_bound_choose_table_zero_row))) /\ ((bcf_index_lucas_bound_choose_table_zero_row = 0 /\ bcf_value_lucas_bound_choose_table_zero_row = 1) \/ exists bcf_predecessor_lucas_bound_choose_table_zero_row. bcf_index_lucas_bound_choose_table_zero_row = S bcf_predecessor_lucas_bound_choose_table_zero_row /\ bcf_value_lucas_bound_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_bound_choose_table bcf_previous_code_lucas_bound_choose_table bcf_previous_scale_lucas_bound_choose_table. bcf_row_index_lucas_bound_choose_table = S bcf_predecessor_lucas_bound_choose_table /\ ((((exists bcf_height_lucas_bound_choose_table_decoded_previous_code. bcf_height_lucas_bound_choose_table_decoded_previous_code + S (bcf_previous_code_lucas_bound_choose_table) = S ((S (bcf_predecessor_lucas_bound_choose_table)) * bcf_row_code_scale_lucas_bound_choose)) /\ exists bcf_quotient_lucas_bound_choose_table_decoded_previous_code. bcf_row_code_code_lucas_bound_choose = bcf_quotient_lucas_bound_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_bound_choose_table)) * bcf_row_code_scale_lucas_bound_choose) + (bcf_previous_code_lucas_bound_choose_table))) /\ ((((exists bcf_height_lucas_bound_choose_table_decoded_previous_scale. bcf_height_lucas_bound_choose_table_decoded_previous_scale + S (bcf_previous_scale_lucas_bound_choose_table) = S ((S (bcf_predecessor_lucas_bound_choose_table)) * bcf_row_scale_scale_lucas_bound_choose)) /\ exists bcf_quotient_lucas_bound_choose_table_decoded_previous_scale. bcf_row_scale_code_lucas_bound_choose = bcf_quotient_lucas_bound_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_bound_choose_table)) * bcf_row_scale_scale_lucas_bound_choose) + (bcf_previous_scale_lucas_bound_choose_table))) /\ (forall bcf_index_lucas_bound_choose_table_row_step. (exists bcf_lt_gap_lucas_bound_choose_table_row_step_bound. bcf_lt_gap_lucas_bound_choose_table_row_step_bound + S (bcf_index_lucas_bound_choose_table_row_step) = S (n)) -> exists bcf_value_lucas_bound_choose_table_row_step. ((((exists bcf_height_lucas_bound_choose_table_row_step_entry. bcf_height_lucas_bound_choose_table_row_step_entry + S (bcf_value_lucas_bound_choose_table_row_step) = S ((S (bcf_index_lucas_bound_choose_table_row_step)) * bcf_row_scale_lucas_bound_choose_table)) /\ exists bcf_quotient_lucas_bound_choose_table_row_step_entry. bcf_row_code_lucas_bound_choose_table = bcf_quotient_lucas_bound_choose_table_row_step_entry * S ((S (bcf_index_lucas_bound_choose_table_row_step)) * bcf_row_scale_lucas_bound_choose_table) + (bcf_value_lucas_bound_choose_table_row_step))) /\ ((bcf_index_lucas_bound_choose_table_row_step = 0 /\ bcf_value_lucas_bound_choose_table_row_step = 1) \/ exists bcf_predecessor_lucas_bound_choose_table_row_step bcf_left_lucas_bound_choose_table_row_step bcf_right_lucas_bound_choose_table_row_step. bcf_index_lucas_bound_choose_table_row_step = S bcf_predecessor_lucas_bound_choose_table_row_step /\ ((((exists bcf_height_lucas_bound_choose_table_row_step_previous_left. bcf_height_lucas_bound_choose_table_row_step_previous_left + S (bcf_left_lucas_bound_choose_table_row_step) = S ((S (bcf_predecessor_lucas_bound_choose_table_row_step)) * bcf_previous_scale_lucas_bound_choose_table)) /\ exists bcf_quotient_lucas_bound_choose_table_row_step_previous_left. bcf_previous_code_lucas_bound_choose_table = bcf_quotient_lucas_bound_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_bound_choose_table_row_step)) * bcf_previous_scale_lucas_bound_choose_table) + (bcf_left_lucas_bound_choose_table_row_step))) /\ ((((exists bcf_height_lucas_bound_choose_table_row_step_previous_right. bcf_height_lucas_bound_choose_table_row_step_previous_right + S (bcf_right_lucas_bound_choose_table_row_step) = S ((S (S (bcf_predecessor_lucas_bound_choose_table_row_step))) * bcf_previous_scale_lucas_bound_choose_table)) /\ exists bcf_quotient_lucas_bound_choose_table_row_step_previous_right. bcf_previous_code_lucas_bound_choose_table = bcf_quotient_lucas_bound_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_bound_choose_table_row_step))) * bcf_previous_scale_lucas_bound_choose_table) + (bcf_right_lucas_bound_choose_table_row_step))) /\ bcf_value_lucas_bound_choose_table_row_step = bcf_left_lucas_bound_choose_table_row_step + bcf_right_lucas_bound_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_bound_choose_decoded_row_code. bcf_height_lucas_bound_choose_decoded_row_code + S (bcf_row_code_lucas_bound_choose) = S ((S (n)) * bcf_row_code_scale_lucas_bound_choose)) /\ exists bcf_quotient_lucas_bound_choose_decoded_row_code. bcf_row_code_code_lucas_bound_choose = bcf_quotient_lucas_bound_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_lucas_bound_choose) + (bcf_row_code_lucas_bound_choose))) /\ ((((exists bcf_height_lucas_bound_choose_decoded_row_scale. bcf_height_lucas_bound_choose_decoded_row_scale + S (bcf_row_scale_lucas_bound_choose) = S ((S (n)) * bcf_row_scale_scale_lucas_bound_choose)) /\ exists bcf_quotient_lucas_bound_choose_decoded_row_scale. bcf_row_scale_code_lucas_bound_choose = bcf_quotient_lucas_bound_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_lucas_bound_choose) + (bcf_row_scale_lucas_bound_choose))) /\ (((exists bcf_height_lucas_bound_choose_decoded_value. bcf_height_lucas_bound_choose_decoded_value + S (C) = S ((S (k)) * bcf_row_scale_lucas_bound_choose)) /\ exists bcf_quotient_lucas_bound_choose_decoded_value. bcf_row_code_lucas_bound_choose = bcf_quotient_lucas_bound_choose_decoded_value * S ((S (k)) * bcf_row_scale_lucas_bound_choose) + (C))))))))) -> (exists ldc_quotient_bound. C = p * ldc_quotient_bound) -> (exists ldc_le_prime_bound. ldc_le_prime_bound + (p) = n)Proof neighborhood
Direct theorem prerequisites
factorial_exists · Stable closed choose_factorial_bridge · Alpha closed multiple_mul_left · Stable closed factorial_prime_le_of_divides · Alpha closed
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
01Fix variables and assumptionsL1–9
02Establish htotalL10–12
Establish this local claim before using it. It is not an additional assumption.
- L10
have htotal : ∃ F. Factorial(n,F)Definitions: Factorial(n,F)Original native command in the exact edition - L11
specialize factorial_exists n - L12
exact factorial_exists
03Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
cases htotal
04Establish hleftL14–16
Establish this local claim before using it. It is not an additional assumption.
- L14
have hleft : ∃ K. Factorial(k,K)Definitions: Factorial(k,K)Original native command in the exact edition - L15
specialize factorial_exists k - L16
exact factorial_exists
05Separate the logical casesL17–17
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L17
cases hleft
06Establish hrightL18–20
Establish this local claim before using it. It is not an additional assumption.
- L18
have hright : ∃ J. Factorial(j,J)Definitions: Factorial(j,J)Original native command in the exact edition - L19
specialize factorial_exists j - L20
exact factorial_exists
07Separate the logical casesL21–21
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L21
cases hright
08Establish hbridgeL22–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose factorial bridge.
- L22
have hbridge : x = (x1 * x2) * C - L23
specialize choose_factorial_bridge n - L24
specialize choose_factorial_bridge k - L25
specialize choose_factorial_bridge j - L26
specialize choose_factorial_bridge C - L27
specialize choose_factorial_bridge x - L28
specialize choose_factorial_bridge x1 - L29
specialize choose_factorial_bridge x2 - L30
apply choose_factorial_bridge - L31
exact hsum
09Use earlier factsL32–35
10Establish hfactorial_dividesL36–45
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple mul left.
- L36
- L37
rewrite hbridge - L38
specialize multiple_mul_left p - L39
specialize multiple_mul_left C - L40
specialize multiple_mul_left (x1 * x2) - L41
apply multiple_mul_left - L42
exact hdivides - L43
specialize factorial_prime_le_of_divides p - L44
specialize factorial_prime_le_of_divides n - L45
specialize factorial_prime_le_of_divides x
Original defined command ledger · 49 lines
- 0001
intro n - 0002
intro k - 0003
intro j - 0004
intro p - 0005
intro C - 0006
intro hsum - 0007
intro hp - 0008
intro hchoose - 0009
intro hdivides - 0010
have htotal : ∃ F. Factorial(n,F)Exact native replay line
have htotal : exists F. (exists ff_b_lucas_bound_total ff_c_lucas_bound_total. ((forall ff_i_lucas_bound_total_range. (exists ff_lt_lucas_bound_total_range_bound. ff_lt_lucas_bound_total_range_bound + S ff_i_lucas_bound_total_range = n) -> (((exists ff_h_lucas_bound_total_range_decoded. ff_h_lucas_bound_total_range_decoded + S (1 + ff_i_lucas_bound_total_range) = S ((S (ff_i_lucas_bound_total_range)) * ff_c_lucas_bound_total)) /\ exists ff_q_lucas_bound_total_range_decoded. ff_b_lucas_bound_total = ff_q_lucas_bound_total_range_decoded * S ((S (ff_i_lucas_bound_total_range)) * ff_c_lucas_bound_total) + (1 + ff_i_lucas_bound_total_range)))) /\ (exists ff_u_lucas_bound_total_product ff_v_lucas_bound_total_product. ((((exists ff_h_lucas_bound_total_product_start. ff_h_lucas_bound_total_product_start + S (1) = S ((S (0)) * ff_v_lucas_bound_total_product)) /\ exists ff_q_lucas_bound_total_product_start. ff_u_lucas_bound_total_product = ff_q_lucas_bound_total_product_start * S ((S (0)) * ff_v_lucas_bound_total_product) + (1))) /\ ((((exists ff_h_lucas_bound_total_product_terminal. ff_h_lucas_bound_total_product_terminal + S (F) = S ((S (n)) * ff_v_lucas_bound_total_product)) /\ exists ff_q_lucas_bound_total_product_terminal. ff_u_lucas_bound_total_product = ff_q_lucas_bound_total_product_terminal * S ((S (n)) * ff_v_lucas_bound_total_product) + (F))) /\ forall ff_i_lucas_bound_total_product. (exists ff_lt_lucas_bound_total_product_bound. ff_lt_lucas_bound_total_product_bound + S ff_i_lucas_bound_total_product = n) -> exists ff_p_lucas_bound_total_product ff_r_lucas_bound_total_product ff_s_lucas_bound_total_product. ((((exists ff_h_lucas_bound_total_product_factor. ff_h_lucas_bound_total_product_factor + S (ff_p_lucas_bound_total_product) = S ((S (ff_i_lucas_bound_total_product)) * ff_c_lucas_bound_total)) /\ exists ff_q_lucas_bound_total_product_factor. ff_b_lucas_bound_total = ff_q_lucas_bound_total_product_factor * S ((S (ff_i_lucas_bound_total_product)) * ff_c_lucas_bound_total) + (ff_p_lucas_bound_total_product))) /\ ((((exists ff_h_lucas_bound_total_product_partial. ff_h_lucas_bound_total_product_partial + S (ff_r_lucas_bound_total_product) = S ((S (ff_i_lucas_bound_total_product)) * ff_v_lucas_bound_total_product)) /\ exists ff_q_lucas_bound_total_product_partial. ff_u_lucas_bound_total_product = ff_q_lucas_bound_total_product_partial * S ((S (ff_i_lucas_bound_total_product)) * ff_v_lucas_bound_total_product) + (ff_r_lucas_bound_total_product))) /\ ((((exists ff_h_lucas_bound_total_product_successor. ff_h_lucas_bound_total_product_successor + S (ff_s_lucas_bound_total_product) = S ((S (S ff_i_lucas_bound_total_product)) * ff_v_lucas_bound_total_product)) /\ exists ff_q_lucas_bound_total_product_successor. ff_u_lucas_bound_total_product = ff_q_lucas_bound_total_product_successor * S ((S (S ff_i_lucas_bound_total_product)) * ff_v_lucas_bound_total_product) + (ff_s_lucas_bound_total_product))) /\ ff_s_lucas_bound_total_product = ff_r_lucas_bound_total_product * ff_p_lucas_bound_total_product)))))))) - 0011
specialize factorial_exists n - 0012
exact factorial_exists - 0013
cases htotal - 0014
have hleft : ∃ K. Factorial(k,K)Exact native replay line
have hleft : exists K. (exists ff_b_lucas_bound_left ff_c_lucas_bound_left. ((forall ff_i_lucas_bound_left_range. (exists ff_lt_lucas_bound_left_range_bound. ff_lt_lucas_bound_left_range_bound + S ff_i_lucas_bound_left_range = k) -> (((exists ff_h_lucas_bound_left_range_decoded. ff_h_lucas_bound_left_range_decoded + S (1 + ff_i_lucas_bound_left_range) = S ((S (ff_i_lucas_bound_left_range)) * ff_c_lucas_bound_left)) /\ exists ff_q_lucas_bound_left_range_decoded. ff_b_lucas_bound_left = ff_q_lucas_bound_left_range_decoded * S ((S (ff_i_lucas_bound_left_range)) * ff_c_lucas_bound_left) + (1 + ff_i_lucas_bound_left_range)))) /\ (exists ff_u_lucas_bound_left_product ff_v_lucas_bound_left_product. ((((exists ff_h_lucas_bound_left_product_start. ff_h_lucas_bound_left_product_start + S (1) = S ((S (0)) * ff_v_lucas_bound_left_product)) /\ exists ff_q_lucas_bound_left_product_start. ff_u_lucas_bound_left_product = ff_q_lucas_bound_left_product_start * S ((S (0)) * ff_v_lucas_bound_left_product) + (1))) /\ ((((exists ff_h_lucas_bound_left_product_terminal. ff_h_lucas_bound_left_product_terminal + S (K) = S ((S (k)) * ff_v_lucas_bound_left_product)) /\ exists ff_q_lucas_bound_left_product_terminal. ff_u_lucas_bound_left_product = ff_q_lucas_bound_left_product_terminal * S ((S (k)) * ff_v_lucas_bound_left_product) + (K))) /\ forall ff_i_lucas_bound_left_product. (exists ff_lt_lucas_bound_left_product_bound. ff_lt_lucas_bound_left_product_bound + S ff_i_lucas_bound_left_product = k) -> exists ff_p_lucas_bound_left_product ff_r_lucas_bound_left_product ff_s_lucas_bound_left_product. ((((exists ff_h_lucas_bound_left_product_factor. ff_h_lucas_bound_left_product_factor + S (ff_p_lucas_bound_left_product) = S ((S (ff_i_lucas_bound_left_product)) * ff_c_lucas_bound_left)) /\ exists ff_q_lucas_bound_left_product_factor. ff_b_lucas_bound_left = ff_q_lucas_bound_left_product_factor * S ((S (ff_i_lucas_bound_left_product)) * ff_c_lucas_bound_left) + (ff_p_lucas_bound_left_product))) /\ ((((exists ff_h_lucas_bound_left_product_partial. ff_h_lucas_bound_left_product_partial + S (ff_r_lucas_bound_left_product) = S ((S (ff_i_lucas_bound_left_product)) * ff_v_lucas_bound_left_product)) /\ exists ff_q_lucas_bound_left_product_partial. ff_u_lucas_bound_left_product = ff_q_lucas_bound_left_product_partial * S ((S (ff_i_lucas_bound_left_product)) * ff_v_lucas_bound_left_product) + (ff_r_lucas_bound_left_product))) /\ ((((exists ff_h_lucas_bound_left_product_successor. ff_h_lucas_bound_left_product_successor + S (ff_s_lucas_bound_left_product) = S ((S (S ff_i_lucas_bound_left_product)) * ff_v_lucas_bound_left_product)) /\ exists ff_q_lucas_bound_left_product_successor. ff_u_lucas_bound_left_product = ff_q_lucas_bound_left_product_successor * S ((S (S ff_i_lucas_bound_left_product)) * ff_v_lucas_bound_left_product) + (ff_s_lucas_bound_left_product))) /\ ff_s_lucas_bound_left_product = ff_r_lucas_bound_left_product * ff_p_lucas_bound_left_product)))))))) - 0015
specialize factorial_exists k - 0016
exact factorial_exists - 0017
cases hleft - 0018
have hright : ∃ J. Factorial(j,J)Exact native replay line
have hright : exists J. (exists ff_b_lucas_bound_right ff_c_lucas_bound_right. ((forall ff_i_lucas_bound_right_range. (exists ff_lt_lucas_bound_right_range_bound. ff_lt_lucas_bound_right_range_bound + S ff_i_lucas_bound_right_range = j) -> (((exists ff_h_lucas_bound_right_range_decoded. ff_h_lucas_bound_right_range_decoded + S (1 + ff_i_lucas_bound_right_range) = S ((S (ff_i_lucas_bound_right_range)) * ff_c_lucas_bound_right)) /\ exists ff_q_lucas_bound_right_range_decoded. ff_b_lucas_bound_right = ff_q_lucas_bound_right_range_decoded * S ((S (ff_i_lucas_bound_right_range)) * ff_c_lucas_bound_right) + (1 + ff_i_lucas_bound_right_range)))) /\ (exists ff_u_lucas_bound_right_product ff_v_lucas_bound_right_product. ((((exists ff_h_lucas_bound_right_product_start. ff_h_lucas_bound_right_product_start + S (1) = S ((S (0)) * ff_v_lucas_bound_right_product)) /\ exists ff_q_lucas_bound_right_product_start. ff_u_lucas_bound_right_product = ff_q_lucas_bound_right_product_start * S ((S (0)) * ff_v_lucas_bound_right_product) + (1))) /\ ((((exists ff_h_lucas_bound_right_product_terminal. ff_h_lucas_bound_right_product_terminal + S (J) = S ((S (j)) * ff_v_lucas_bound_right_product)) /\ exists ff_q_lucas_bound_right_product_terminal. ff_u_lucas_bound_right_product = ff_q_lucas_bound_right_product_terminal * S ((S (j)) * ff_v_lucas_bound_right_product) + (J))) /\ forall ff_i_lucas_bound_right_product. (exists ff_lt_lucas_bound_right_product_bound. ff_lt_lucas_bound_right_product_bound + S ff_i_lucas_bound_right_product = j) -> exists ff_p_lucas_bound_right_product ff_r_lucas_bound_right_product ff_s_lucas_bound_right_product. ((((exists ff_h_lucas_bound_right_product_factor. ff_h_lucas_bound_right_product_factor + S (ff_p_lucas_bound_right_product) = S ((S (ff_i_lucas_bound_right_product)) * ff_c_lucas_bound_right)) /\ exists ff_q_lucas_bound_right_product_factor. ff_b_lucas_bound_right = ff_q_lucas_bound_right_product_factor * S ((S (ff_i_lucas_bound_right_product)) * ff_c_lucas_bound_right) + (ff_p_lucas_bound_right_product))) /\ ((((exists ff_h_lucas_bound_right_product_partial. ff_h_lucas_bound_right_product_partial + S (ff_r_lucas_bound_right_product) = S ((S (ff_i_lucas_bound_right_product)) * ff_v_lucas_bound_right_product)) /\ exists ff_q_lucas_bound_right_product_partial. ff_u_lucas_bound_right_product = ff_q_lucas_bound_right_product_partial * S ((S (ff_i_lucas_bound_right_product)) * ff_v_lucas_bound_right_product) + (ff_r_lucas_bound_right_product))) /\ ((((exists ff_h_lucas_bound_right_product_successor. ff_h_lucas_bound_right_product_successor + S (ff_s_lucas_bound_right_product) = S ((S (S ff_i_lucas_bound_right_product)) * ff_v_lucas_bound_right_product)) /\ exists ff_q_lucas_bound_right_product_successor. ff_u_lucas_bound_right_product = ff_q_lucas_bound_right_product_successor * S ((S (S ff_i_lucas_bound_right_product)) * ff_v_lucas_bound_right_product) + (ff_s_lucas_bound_right_product))) /\ ff_s_lucas_bound_right_product = ff_r_lucas_bound_right_product * ff_p_lucas_bound_right_product)))))))) - 0019
specialize factorial_exists j - 0020
exact factorial_exists - 0021
cases hright - 0022
have hbridge : x = (x1 * x2) * C - 0023
specialize choose_factorial_bridge n - 0024
specialize choose_factorial_bridge k - 0025
specialize choose_factorial_bridge j - 0026
specialize choose_factorial_bridge C - 0027
specialize choose_factorial_bridge x - 0028
specialize choose_factorial_bridge x1 - 0029
specialize choose_factorial_bridge x2 - 0030
apply choose_factorial_bridge - 0031
exact hsum - 0032
exact hchoose - 0033
exact htotal_witness - 0034
exact hleft_witness - 0035
exact hright_witness - 0036
have hfactorial_divides : Dvd(p,x)Exact native replay line
have hfactorial_divides : exists z. x = p * z - 0037
rewrite hbridge - 0038
specialize multiple_mul_left p - 0039
specialize multiple_mul_left C - 0040
specialize multiple_mul_left (x1 * x2) - 0041
apply multiple_mul_left - 0042
exact hdivides - 0043
specialize factorial_prime_le_of_divides p - 0044
specialize factorial_prime_le_of_divides n - 0045
specialize factorial_prime_le_of_divides x - 0046
apply factorial_prime_le_of_divides - 0047
exact hp - 0048
exact htotal_witness - 0049
exact hfactorial_divides