LU0002

lucas_choose_prime_divisor_bound

Dependency-curried candidate body; not Alpha-enrolled; no checked-use authority

Every prime divisor of a relational binomial coefficient is at most its Pascal-row index.

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.

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

Every prime divisor of a relational binomial coefficient is at most its Pascal-row index.

The unchanged tactic script uses 4 declared prerequisites and contains 49 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

factorial_exists Stable theorem; checked-use authorized choose_factorial_bridge Alpha theorem; checked-use authorized multiple_mul_left Stable theorem; checked-use authorized factorial_prime_le_of_divides Alpha theorem; checked-use authorized

Direct dependents

LU0003 lucas_digit_carry_iff_prime_divides

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.

Read the argument

Proof checkpoints

49 script commands · 11 reading checkpoints · 5 local claims

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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–9

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro j
  4. L4
    intro p
  5. L5
    intro C
  6. L6
    intro hsum
  7. L7
    intro hp
  8. L8
    intro hchoose
  9. L9
    intro hdivides
02Establish htotalL10–12

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have htotal : ∃ F. Factorial(n,F)Definitions: Factorial
  2. L11
    specialize factorial_exists n
  3. L12
    exact factorial_exists
03Separate the logical casesL13–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    cases htotal
04Establish hleftL14–16

Establish this local claim before using it. It is not an additional assumption.

  1. L14
    have hleft : ∃ K. Factorial(k,K)Definitions: Factorial
  2. L15
    specialize factorial_exists k
  3. L16
    exact factorial_exists
05Separate the logical casesL17–17

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L17
    cases hleft
06Establish hrightL18–20

Establish this local claim before using it. It is not an additional assumption.

  1. L18
    have hright : ∃ J. Factorial(j,J)Definitions: Factorial
  2. L19
    specialize factorial_exists j
  3. L20
    exact factorial_exists
07Separate the logical casesL21–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. 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.

  1. L22
    have hbridge : x = (x1 * x2) * C
  2. L23
    specialize choose_factorial_bridge n
  3. L24
    specialize choose_factorial_bridge k
  4. L25
    specialize choose_factorial_bridge j
  5. L26
    specialize choose_factorial_bridge C
  6. L27
    specialize choose_factorial_bridge x
  7. L28
    specialize choose_factorial_bridge x1
  8. L29
    specialize choose_factorial_bridge x2
  9. L30
    apply choose_factorial_bridge
  10. L31
    exact hsum
09Use earlier factsL32–35

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    exact hchoose
  2. L33
    exact htotal_witness
  3. L34
    exact hleft_witness
  4. L35
    exact hright_witness
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.

  1. L36
    have hfactorial_divides : exists z. x = p * z
  2. L37
    rewrite hbridge
  3. L38
    specialize multiple_mul_left p
  4. L39
    specialize multiple_mul_left C
  5. L40
    specialize multiple_mul_left (x1 * x2)
  6. L41
    apply multiple_mul_left
  7. L42
    exact hdivides
  8. L43
    specialize factorial_prime_le_of_divides p
  9. L44
    specialize factorial_prime_le_of_divides n
  10. L45
    specialize factorial_prime_le_of_divides x
11Use earlier factsL46–49

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L46
    apply factorial_prime_le_of_divides
  2. L47
    exact hp
  3. L48
    exact htotal_witness
  4. L49
    exact hfactorial_divides

Library-wide reading audit

Original exact command ledger · 49 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro j
  4. 0004intro p
  5. 0005intro C
  6. 0006intro hsum
  7. 0007intro hp
  8. 0008intro hchoose
  9. 0009intro hdivides
  10. 0010have 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))))))))
  11. 0011specialize factorial_exists n
  12. 0012exact factorial_exists
  13. 0013cases htotal
  14. 0014have 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))))))))
  15. 0015specialize factorial_exists k
  16. 0016exact factorial_exists
  17. 0017cases hleft
  18. 0018have 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))))))))
  19. 0019specialize factorial_exists j
  20. 0020exact factorial_exists
  21. 0021cases hright
  22. 0022have hbridge : x = (x1 * x2) * C
  23. 0023specialize choose_factorial_bridge n
  24. 0024specialize choose_factorial_bridge k
  25. 0025specialize choose_factorial_bridge j
  26. 0026specialize choose_factorial_bridge C
  27. 0027specialize choose_factorial_bridge x
  28. 0028specialize choose_factorial_bridge x1
  29. 0029specialize choose_factorial_bridge x2
  30. 0030apply choose_factorial_bridge
  31. 0031exact hsum
  32. 0032exact hchoose
  33. 0033exact htotal_witness
  34. 0034exact hleft_witness
  35. 0035exact hright_witness
  36. 0036have hfactorial_divides : exists z. x = p * z
  37. 0037rewrite hbridge
  38. 0038specialize multiple_mul_left p
  39. 0039specialize multiple_mul_left C
  40. 0040specialize multiple_mul_left (x1 * x2)
  41. 0041apply multiple_mul_left
  42. 0042exact hdivides
  43. 0043specialize factorial_prime_le_of_divides p
  44. 0044specialize factorial_prime_le_of_divides n
  45. 0045specialize factorial_prime_le_of_divides x
  46. 0046apply factorial_prime_le_of_divides
  47. 0047exact hp
  48. 0048exact htotal_witness
  49. 0049exact hfactorial_divides