AF001A

prime_factor_lists_permutation_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Exact G005: every two arbitrary unordered prime factorizations of the same positive natural admit an actual coded matching bijection, with equal lengths and explicit boundedness, injectivity, and surjectivity.

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 b c l d e m. (((~(n = 0) /\ ((exists ff_u_fsat_root_source_product ff_v_fsat_root_source_product. ((((exists ff_h_fsat_root_source_product_start. ff_h_fsat_root_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_root_source_product)) /\ exists ff_q_fsat_root_source_product_start. ff_u_fsat_root_source_product = ff_q_fsat_root_source_product_start * S ((S (0)) * ff_v_fsat_root_source_product) + (1))) /\ ((((exists ff_h_fsat_root_source_product_terminal. ff_h_fsat_root_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_root_source_product)) /\ exists ff_q_fsat_root_source_product_terminal. ff_u_fsat_root_source_product = ff_q_fsat_root_source_product_terminal * S ((S (l)) * ff_v_fsat_root_source_product) + (n))) /\ forall ff_i_fsat_root_source_product. (exists ff_lt_fsat_root_source_product_bound. ff_lt_fsat_root_source_product_bound + S ff_i_fsat_root_source_product = l) -> exists ff_p_fsat_root_source_product ff_r_fsat_root_source_product ff_s_fsat_root_source_product. ((((exists ff_h_fsat_root_source_product_factor. ff_h_fsat_root_source_product_factor + S (ff_p_fsat_root_source_product) = S ((S (ff_i_fsat_root_source_product)) * c)) /\ exists ff_q_fsat_root_source_product_factor. b = ff_q_fsat_root_source_product_factor * S ((S (ff_i_fsat_root_source_product)) * c) + (ff_p_fsat_root_source_product))) /\ ((((exists ff_h_fsat_root_source_product_partial. ff_h_fsat_root_source_product_partial + S (ff_r_fsat_root_source_product) = S ((S (ff_i_fsat_root_source_product)) * ff_v_fsat_root_source_product)) /\ exists ff_q_fsat_root_source_product_partial. ff_u_fsat_root_source_product = ff_q_fsat_root_source_product_partial * S ((S (ff_i_fsat_root_source_product)) * ff_v_fsat_root_source_product) + (ff_r_fsat_root_source_product))) /\ ((((exists ff_h_fsat_root_source_product_successor. ff_h_fsat_root_source_product_successor + S (ff_s_fsat_root_source_product) = S ((S (S ff_i_fsat_root_source_product)) * ff_v_fsat_root_source_product)) /\ exists ff_q_fsat_root_source_product_successor. ff_u_fsat_root_source_product = ff_q_fsat_root_source_product_successor * S ((S (S ff_i_fsat_root_source_product)) * ff_v_fsat_root_source_product) + (ff_s_fsat_root_source_product))) /\ ff_s_fsat_root_source_product = ff_r_fsat_root_source_product * ff_p_fsat_root_source_product)))))) /\ (forall ftsf_index_fsat_root_source_primes. (exists ftsf_gap_fsat_root_source_primes_bound. ftsf_gap_fsat_root_source_primes_bound + S ftsf_index_fsat_root_source_primes = (l)) -> exists ftsf_factor_fsat_root_source_primes. ((((exists ff_h_ftsf_fsat_root_source_primes_entry. ff_h_ftsf_fsat_root_source_primes_entry + S (ftsf_factor_fsat_root_source_primes) = S ((S (ftsf_index_fsat_root_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_root_source_primes_entry. b = ff_q_ftsf_fsat_root_source_primes_entry * S ((S (ftsf_index_fsat_root_source_primes)) * c) + (ftsf_factor_fsat_root_source_primes))) /\ ((~(ftsf_factor_fsat_root_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_root_source_primes_prime frm_prime_right_ftsf_fsat_root_source_primes_prime. ftsf_factor_fsat_root_source_primes = frm_prime_left_ftsf_fsat_root_source_primes_prime * frm_prime_right_ftsf_fsat_root_source_primes_prime -> frm_prime_left_ftsf_fsat_root_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_root_source_primes_prime = 1))))))) /\ ((~(n = 0) /\ ((exists ff_u_fsat_root_target_product ff_v_fsat_root_target_product. ((((exists ff_h_fsat_root_target_product_start. ff_h_fsat_root_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_root_target_product)) /\ exists ff_q_fsat_root_target_product_start. ff_u_fsat_root_target_product = ff_q_fsat_root_target_product_start * S ((S (0)) * ff_v_fsat_root_target_product) + (1))) /\ ((((exists ff_h_fsat_root_target_product_terminal. ff_h_fsat_root_target_product_terminal + S (n) = S ((S (m)) * ff_v_fsat_root_target_product)) /\ exists ff_q_fsat_root_target_product_terminal. ff_u_fsat_root_target_product = ff_q_fsat_root_target_product_terminal * S ((S (m)) * ff_v_fsat_root_target_product) + (n))) /\ forall ff_i_fsat_root_target_product. (exists ff_lt_fsat_root_target_product_bound. ff_lt_fsat_root_target_product_bound + S ff_i_fsat_root_target_product = m) -> exists ff_p_fsat_root_target_product ff_r_fsat_root_target_product ff_s_fsat_root_target_product. ((((exists ff_h_fsat_root_target_product_factor. ff_h_fsat_root_target_product_factor + S (ff_p_fsat_root_target_product) = S ((S (ff_i_fsat_root_target_product)) * e)) /\ exists ff_q_fsat_root_target_product_factor. d = ff_q_fsat_root_target_product_factor * S ((S (ff_i_fsat_root_target_product)) * e) + (ff_p_fsat_root_target_product))) /\ ((((exists ff_h_fsat_root_target_product_partial. ff_h_fsat_root_target_product_partial + S (ff_r_fsat_root_target_product) = S ((S (ff_i_fsat_root_target_product)) * ff_v_fsat_root_target_product)) /\ exists ff_q_fsat_root_target_product_partial. ff_u_fsat_root_target_product = ff_q_fsat_root_target_product_partial * S ((S (ff_i_fsat_root_target_product)) * ff_v_fsat_root_target_product) + (ff_r_fsat_root_target_product))) /\ ((((exists ff_h_fsat_root_target_product_successor. ff_h_fsat_root_target_product_successor + S (ff_s_fsat_root_target_product) = S ((S (S ff_i_fsat_root_target_product)) * ff_v_fsat_root_target_product)) /\ exists ff_q_fsat_root_target_product_successor. ff_u_fsat_root_target_product = ff_q_fsat_root_target_product_successor * S ((S (S ff_i_fsat_root_target_product)) * ff_v_fsat_root_target_product) + (ff_s_fsat_root_target_product))) /\ ff_s_fsat_root_target_product = ff_r_fsat_root_target_product * ff_p_fsat_root_target_product)))))) /\ (forall ftsf_index_fsat_root_target_primes. (exists ftsf_gap_fsat_root_target_primes_bound. ftsf_gap_fsat_root_target_primes_bound + S ftsf_index_fsat_root_target_primes = (m)) -> exists ftsf_factor_fsat_root_target_primes. ((((exists ff_h_ftsf_fsat_root_target_primes_entry. ff_h_ftsf_fsat_root_target_primes_entry + S (ftsf_factor_fsat_root_target_primes) = S ((S (ftsf_index_fsat_root_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_root_target_primes_entry. d = ff_q_ftsf_fsat_root_target_primes_entry * S ((S (ftsf_index_fsat_root_target_primes)) * e) + (ftsf_factor_fsat_root_target_primes))) /\ ((~(ftsf_factor_fsat_root_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_root_target_primes_prime frm_prime_right_ftsf_fsat_root_target_primes_prime. ftsf_factor_fsat_root_target_primes = frm_prime_left_ftsf_fsat_root_target_primes_prime * frm_prime_right_ftsf_fsat_root_target_primes_prime -> frm_prime_left_ftsf_fsat_root_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_root_target_primes_prime = 1)))))))) -> exists u v. (((l = m) /\ (((((forall pfp_i_root_permutationpermutationbounded. (exists pfp_gap_root_permutationpermutationboundedindex. pfp_gap_root_permutationpermutationboundedindex + S (pfp_i_root_permutationpermutationbounded) = (l)) -> exists pfp_a_root_permutationpermutationbounded. (((exists ff_h_pfp_root_permutationpermutationboundedentry. ff_h_pfp_root_permutationpermutationboundedentry + S (pfp_a_root_permutationpermutationbounded) = S ((S (pfp_i_root_permutationpermutationbounded)) * v)) /\ exists ff_q_pfp_root_permutationpermutationboundedentry. u = ff_q_pfp_root_permutationpermutationboundedentry * S ((S (pfp_i_root_permutationpermutationbounded)) * v) + (pfp_a_root_permutationpermutationbounded))) /\ (exists pfp_gap_root_permutationpermutationboundedvalue. pfp_gap_root_permutationpermutationboundedvalue + S (pfp_a_root_permutationpermutationbounded) = (l))) /\ (((forall pfp_i_root_permutationpermutationinjective pfp_j_root_permutationpermutationinjective pfp_a_root_permutationpermutationinjective. (exists pfp_gap_root_permutationpermutationinjectivefirst. pfp_gap_root_permutationpermutationinjectivefirst + S (pfp_i_root_permutationpermutationinjective) = (l)) -> (exists pfp_gap_root_permutationpermutationinjectivesecond. pfp_gap_root_permutationpermutationinjectivesecond + S (pfp_j_root_permutationpermutationinjective) = (l)) -> (((exists ff_h_pfp_root_permutationpermutationinjectiveleft. ff_h_pfp_root_permutationpermutationinjectiveleft + S (pfp_a_root_permutationpermutationinjective) = S ((S (pfp_i_root_permutationpermutationinjective)) * v)) /\ exists ff_q_pfp_root_permutationpermutationinjectiveleft. u = ff_q_pfp_root_permutationpermutationinjectiveleft * S ((S (pfp_i_root_permutationpermutationinjective)) * v) + (pfp_a_root_permutationpermutationinjective))) -> (((exists ff_h_pfp_root_permutationpermutationinjectiveright. ff_h_pfp_root_permutationpermutationinjectiveright + S (pfp_a_root_permutationpermutationinjective) = S ((S (pfp_j_root_permutationpermutationinjective)) * v)) /\ exists ff_q_pfp_root_permutationpermutationinjectiveright. u = ff_q_pfp_root_permutationpermutationinjectiveright * S ((S (pfp_j_root_permutationpermutationinjective)) * v) + (pfp_a_root_permutationpermutationinjective))) -> pfp_i_root_permutationpermutationinjective = pfp_j_root_permutationpermutationinjective) /\ (forall pfp_a_root_permutationpermutationsurjective. (exists pfp_gap_root_permutationpermutationsurjectivevalue. pfp_gap_root_permutationpermutationsurjectivevalue + S (pfp_a_root_permutationpermutationsurjective) = (l)) -> exists pfp_i_root_permutationpermutationsurjective. (exists pfp_gap_root_permutationpermutationsurjectiveindex. pfp_gap_root_permutationpermutationsurjectiveindex + S (pfp_i_root_permutationpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_root_permutationpermutationsurjectiveentry. ff_h_pfp_root_permutationpermutationsurjectiveentry + S (pfp_a_root_permutationpermutationsurjective) = S ((S (pfp_i_root_permutationpermutationsurjective)) * v)) /\ exists ff_q_pfp_root_permutationpermutationsurjectiveentry. u = ff_q_pfp_root_permutationpermutationsurjectiveentry * S ((S (pfp_i_root_permutationpermutationsurjective)) * v) + (pfp_a_root_permutationpermutationsurjective)))))))) /\ (forall pfp_i_root_permutationmatching pfp_j_root_permutationmatching pfp_a_root_permutationmatching. (exists pfp_gap_root_permutationmatchingbound. pfp_gap_root_permutationmatchingbound + S (pfp_i_root_permutationmatching) = (l)) -> (((exists ff_h_pfp_root_permutationmatchingmap. ff_h_pfp_root_permutationmatchingmap + S (pfp_j_root_permutationmatching) = S ((S (pfp_i_root_permutationmatching)) * v)) /\ exists ff_q_pfp_root_permutationmatchingmap. u = ff_q_pfp_root_permutationmatchingmap * S ((S (pfp_i_root_permutationmatching)) * v) + (pfp_j_root_permutationmatching))) -> (((exists ff_h_pfp_root_permutationmatchingsource. ff_h_pfp_root_permutationmatchingsource + S (pfp_a_root_permutationmatching) = S ((S (pfp_i_root_permutationmatching)) * c)) /\ exists ff_q_pfp_root_permutationmatchingsource. b = ff_q_pfp_root_permutationmatchingsource * S ((S (pfp_i_root_permutationmatching)) * c) + (pfp_a_root_permutationmatching))) -> (((exists ff_h_pfp_root_permutationmatchingtarget. ff_h_pfp_root_permutationmatchingtarget + S (pfp_a_root_permutationmatching) = S ((S (pfp_j_root_permutationmatching)) * e)) /\ exists ff_q_pfp_root_permutationmatchingtarget. d = ff_q_pfp_root_permutationmatchingtarget * S ((S (pfp_j_root_permutationmatching)) * e) + (pfp_a_root_permutationmatching))))))))

Constructive proof overview

Generated structural guide

Exact G005: every two arbitrary unordered prime factorizations of the same positive natural admit an actual coded matching bijection, with equal lengths and explicit boundedness, injectivity, and surjectivity.

The unchanged tactic script uses 1 declared prerequisite and contains 28 exact native proof lines.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

AF0019 prime_factor_lists_matching_by_length

Direct dependents

AF001B prime_factorization_exists_unique_up_to_permutation

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

28 script commands · 8 reading checkpoints · 1 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.

Named ingredients (1)
prime factor lists matching by length

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–8

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro l
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro m
  8. L8
    intro hf
02Separate the logical casesL9–9

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

  1. L9
    cases hf
03Establish hresultL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime factor lists matching by length.

  1. L10
    have hresult : l = m ∧ (∃ x. ∃ y. PermutationPrefix(x,y,l) ∧ FactorListMatching(b,c,d,e,x,y,l))Definitions: PermutationPrefixFactorListMatching
  2. L11
    specialize prime_factor_lists_matching_by_length (l)
  3. L12
    specialize prime_factor_lists_matching_by_length (n)
  4. L13
    specialize prime_factor_lists_matching_by_length (b)
  5. L14
    specialize prime_factor_lists_matching_by_length (c)
  6. L15
    specialize prime_factor_lists_matching_by_length (m)
  7. L16
    specialize prime_factor_lists_matching_by_length (d)
  8. L17
    specialize prime_factor_lists_matching_by_length (e)
  9. L18
    apply prime_factor_lists_matching_by_length
  10. L19
    exact hf_left
04Use earlier factsL20–20

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

  1. L20
    exact hf_right
05Separate the logical casesL21–23

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

  1. L21
    cases hresult
  2. L22
    cases hresult_right
  3. L23
    cases hresult_right_witness
06Construct an explicit witnessL24–25

Supply the displayed value, then prove that it has the required property.

  1. L24
    exists x
  2. L25
    exists x1
07Separate the logical casesL26–26

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

  1. L26
    split
08Use earlier factsL27–28

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

  1. L27
    exact hresult_left
  2. L28
    exact hresult_right_witness_witness

Library-wide reading audit

Original exact command ledger · 28 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro d
  6. 0006intro e
  7. 0007intro m
  8. 0008intro hf
  9. 0009cases hf
  10. 0010have hresult : ((l = m) /\ (exists pfp_u_root_induction pfp_v_root_induction. (((((forall pfp_i_root_inductionmatchingpermutationbounded. (exists pfp_gap_root_inductionmatchingpermutationboundedindex. pfp_gap_root_inductionmatchingpermutationboundedindex + S (pfp_i_root_inductionmatchingpermutationbounded) = (l)) -> exists pfp_a_root_inductionmatchingpermutationbounded. (((exists ff_h_pfp_root_inductionmatchingpermutationboundedentry. ff_h_pfp_root_inductionmatchingpermutationboundedentry + S (pfp_a_root_inductionmatchingpermutationbounded) = S ((S (pfp_i_root_inductionmatchingpermutationbounded)) * pfp_v_root_induction)) /\ exists ff_q_pfp_root_inductionmatchingpermutationboundedentry. pfp_u_root_induction = ff_q_pfp_root_inductionmatchingpermutationboundedentry * S ((S (pfp_i_root_inductionmatchingpermutationbounded)) * pfp_v_root_induction) + (pfp_a_root_inductionmatchingpermutationbounded))) /\ (exists pfp_gap_root_inductionmatchingpermutationboundedvalue. pfp_gap_root_inductionmatchingpermutationboundedvalue + S (pfp_a_root_inductionmatchingpermutationbounded) = (l))) /\ (((forall pfp_i_root_inductionmatchingpermutationinjective pfp_j_root_inductionmatchingpermutationinjective pfp_a_root_inductionmatchingpermutationinjective. (exists pfp_gap_root_inductionmatchingpermutationinjectivefirst. pfp_gap_root_inductionmatchingpermutationinjectivefirst + S (pfp_i_root_inductionmatchingpermutationinjective) = (l)) -> (exists pfp_gap_root_inductionmatchingpermutationinjectivesecond. pfp_gap_root_inductionmatchingpermutationinjectivesecond + S (pfp_j_root_inductionmatchingpermutationinjective) = (l)) -> (((exists ff_h_pfp_root_inductionmatchingpermutationinjectiveleft. ff_h_pfp_root_inductionmatchingpermutationinjectiveleft + S (pfp_a_root_inductionmatchingpermutationinjective) = S ((S (pfp_i_root_inductionmatchingpermutationinjective)) * pfp_v_root_induction)) /\ exists ff_q_pfp_root_inductionmatchingpermutationinjectiveleft. pfp_u_root_induction = ff_q_pfp_root_inductionmatchingpermutationinjectiveleft * S ((S (pfp_i_root_inductionmatchingpermutationinjective)) * pfp_v_root_induction) + (pfp_a_root_inductionmatchingpermutationinjective))) -> (((exists ff_h_pfp_root_inductionmatchingpermutationinjectiveright. ff_h_pfp_root_inductionmatchingpermutationinjectiveright + S (pfp_a_root_inductionmatchingpermutationinjective) = S ((S (pfp_j_root_inductionmatchingpermutationinjective)) * pfp_v_root_induction)) /\ exists ff_q_pfp_root_inductionmatchingpermutationinjectiveright. pfp_u_root_induction = ff_q_pfp_root_inductionmatchingpermutationinjectiveright * S ((S (pfp_j_root_inductionmatchingpermutationinjective)) * pfp_v_root_induction) + (pfp_a_root_inductionmatchingpermutationinjective))) -> pfp_i_root_inductionmatchingpermutationinjective = pfp_j_root_inductionmatchingpermutationinjective) /\ (forall pfp_a_root_inductionmatchingpermutationsurjective. (exists pfp_gap_root_inductionmatchingpermutationsurjectivevalue. pfp_gap_root_inductionmatchingpermutationsurjectivevalue + S (pfp_a_root_inductionmatchingpermutationsurjective) = (l)) -> exists pfp_i_root_inductionmatchingpermutationsurjective. (exists pfp_gap_root_inductionmatchingpermutationsurjectiveindex. pfp_gap_root_inductionmatchingpermutationsurjectiveindex + S (pfp_i_root_inductionmatchingpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_root_inductionmatchingpermutationsurjectiveentry. ff_h_pfp_root_inductionmatchingpermutationsurjectiveentry + S (pfp_a_root_inductionmatchingpermutationsurjective) = S ((S (pfp_i_root_inductionmatchingpermutationsurjective)) * pfp_v_root_induction)) /\ exists ff_q_pfp_root_inductionmatchingpermutationsurjectiveentry. pfp_u_root_induction = ff_q_pfp_root_inductionmatchingpermutationsurjectiveentry * S ((S (pfp_i_root_inductionmatchingpermutationsurjective)) * pfp_v_root_induction) + (pfp_a_root_inductionmatchingpermutationsurjective)))))))) /\ (forall pfp_i_root_inductionmatchingmatching pfp_j_root_inductionmatchingmatching pfp_a_root_inductionmatchingmatching. (exists pfp_gap_root_inductionmatchingmatchingbound. pfp_gap_root_inductionmatchingmatchingbound + S (pfp_i_root_inductionmatchingmatching) = (l)) -> (((exists ff_h_pfp_root_inductionmatchingmatchingmap. ff_h_pfp_root_inductionmatchingmatchingmap + S (pfp_j_root_inductionmatchingmatching) = S ((S (pfp_i_root_inductionmatchingmatching)) * pfp_v_root_induction)) /\ exists ff_q_pfp_root_inductionmatchingmatchingmap. pfp_u_root_induction = ff_q_pfp_root_inductionmatchingmatchingmap * S ((S (pfp_i_root_inductionmatchingmatching)) * pfp_v_root_induction) + (pfp_j_root_inductionmatchingmatching))) -> (((exists ff_h_pfp_root_inductionmatchingmatchingsource. ff_h_pfp_root_inductionmatchingmatchingsource + S (pfp_a_root_inductionmatchingmatching) = S ((S (pfp_i_root_inductionmatchingmatching)) * c)) /\ exists ff_q_pfp_root_inductionmatchingmatchingsource. b = ff_q_pfp_root_inductionmatchingmatchingsource * S ((S (pfp_i_root_inductionmatchingmatching)) * c) + (pfp_a_root_inductionmatchingmatching))) -> (((exists ff_h_pfp_root_inductionmatchingmatchingtarget. ff_h_pfp_root_inductionmatchingmatchingtarget + S (pfp_a_root_inductionmatchingmatching) = S ((S (pfp_j_root_inductionmatchingmatching)) * e)) /\ exists ff_q_pfp_root_inductionmatchingmatchingtarget. d = ff_q_pfp_root_inductionmatchingmatchingtarget * S ((S (pfp_j_root_inductionmatchingmatching)) * e) + (pfp_a_root_inductionmatchingmatching))))))))
  11. 0011specialize prime_factor_lists_matching_by_length (l)
  12. 0012specialize prime_factor_lists_matching_by_length (n)
  13. 0013specialize prime_factor_lists_matching_by_length (b)
  14. 0014specialize prime_factor_lists_matching_by_length (c)
  15. 0015specialize prime_factor_lists_matching_by_length (m)
  16. 0016specialize prime_factor_lists_matching_by_length (d)
  17. 0017specialize prime_factor_lists_matching_by_length (e)
  18. 0018apply prime_factor_lists_matching_by_length
  19. 0019exact hf_left
  20. 0020exact hf_right
  21. 0021cases hresult
  22. 0022cases hresult_right
  23. 0023cases hresult_right_witness
  24. 0024exists x
  25. 0025exists x1
  26. 0026split
  27. 0027exact hresult_left
  28. 0028exact hresult_right_witness_witness