PQ002D

prime_field_polynomial_trim_exists_unique

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

Construct an actual trim and prove unique removed count, retained length and decoded coefficients against every other actual trim.

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

forall p b c L. (forall fom_index_pfp_unique_input. (exists fom_gap_pfp_unique_input_index_bound. fom_gap_pfp_unique_input_index_bound + S (fom_index_pfp_unique_input) = L) -> exists fom_value_pfp_unique_input. ((((exists fom_beta_height_pfp_unique_input_entry. fom_beta_height_pfp_unique_input_entry + S (fom_value_pfp_unique_input) = S ((S (fom_index_pfp_unique_input)) * c)) /\ exists fom_beta_quotient_pfp_unique_input_entry. b = fom_beta_quotient_pfp_unique_input_entry * S ((S (fom_index_pfp_unique_input)) * c) + (fom_value_pfp_unique_input))) /\ (exists fom_gap_pfp_unique_input_value_bound. fom_gap_pfp_unique_input_value_bound + S (fom_value_pfp_unique_input) = p))) -> exists t d e M. (((((L)=(t)+(M)) /\ (((forall fom_index_pfp_unique_constructedinput. (exists fom_gap_pfp_unique_constructedinput_index_bound. fom_gap_pfp_unique_constructedinput_index_bound + S (fom_index_pfp_unique_constructedinput) = L) -> exists fom_value_pfp_unique_constructedinput. ((((exists fom_beta_height_pfp_unique_constructedinput_entry. fom_beta_height_pfp_unique_constructedinput_entry + S (fom_value_pfp_unique_constructedinput) = S ((S (fom_index_pfp_unique_constructedinput)) * c)) /\ exists fom_beta_quotient_pfp_unique_constructedinput_entry. b = fom_beta_quotient_pfp_unique_constructedinput_entry * S ((S (fom_index_pfp_unique_constructedinput)) * c) + (fom_value_pfp_unique_constructedinput))) /\ (exists fom_gap_pfp_unique_constructedinput_value_bound. fom_gap_pfp_unique_constructedinput_value_bound + S (fom_value_pfp_unique_constructedinput) = p))) /\ (((forall pfp_repeat_index_unique_constructedremoved. (exists pfa_gap_unique_constructedremovedindex. pfa_gap_unique_constructedremovedindex + S (pfp_repeat_index_unique_constructedremoved) = (t)) -> (((exists ff_h_pfp_unique_constructedremovedentry. ff_h_pfp_unique_constructedremovedentry + S (0) = S ((S (pfp_repeat_index_unique_constructedremoved)) * c)) /\ exists ff_q_pfp_unique_constructedremovedentry. b = ff_q_pfp_unique_constructedremovedentry * S ((S (pfp_repeat_index_unique_constructedremoved)) * c) + (0)))) /\ (((forall pftrim_index_unique_constructedsuffix pftrim_value_unique_constructedsuffix. (exists pfa_gap_unique_constructedsuffixbound. pfa_gap_unique_constructedsuffixbound + S (pftrim_index_unique_constructedsuffix) = (M)) -> (((exists ff_h_pfp_unique_constructedsuffixsource. ff_h_pfp_unique_constructedsuffixsource + S (pftrim_value_unique_constructedsuffix) = S ((S ((t)+pftrim_index_unique_constructedsuffix)) * c)) /\ exists ff_q_pfp_unique_constructedsuffixsource. b = ff_q_pfp_unique_constructedsuffixsource * S ((S ((t)+pftrim_index_unique_constructedsuffix)) * c) + (pftrim_value_unique_constructedsuffix))) -> (((exists ff_h_pfp_unique_constructedsuffixoutput. ff_h_pfp_unique_constructedsuffixoutput + S (pftrim_value_unique_constructedsuffix) = S ((S (pftrim_index_unique_constructedsuffix)) * e)) /\ exists ff_q_pfp_unique_constructedsuffixoutput. d = ff_q_pfp_unique_constructedsuffixoutput * S ((S (pftrim_index_unique_constructedsuffix)) * e) + (pftrim_value_unique_constructedsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_unique_constructednormal. ((((exists ff_h_pfp_unique_constructednormalentry. ff_h_pfp_unique_constructednormalentry + S (pftrim_leading_unique_constructednormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_unique_constructednormalentry. d = ff_q_pfp_unique_constructednormalentry * S ((S (0)) * e) + (pftrim_leading_unique_constructednormal))) /\ ((~(pftrim_leading_unique_constructednormal=0))))))))))))))) /\ ((forall u f g N. ((((L)=(u)+(N)) /\ (((forall fom_index_pfp_unique_comparisoninput. (exists fom_gap_pfp_unique_comparisoninput_index_bound. fom_gap_pfp_unique_comparisoninput_index_bound + S (fom_index_pfp_unique_comparisoninput) = L) -> exists fom_value_pfp_unique_comparisoninput. ((((exists fom_beta_height_pfp_unique_comparisoninput_entry. fom_beta_height_pfp_unique_comparisoninput_entry + S (fom_value_pfp_unique_comparisoninput) = S ((S (fom_index_pfp_unique_comparisoninput)) * c)) /\ exists fom_beta_quotient_pfp_unique_comparisoninput_entry. b = fom_beta_quotient_pfp_unique_comparisoninput_entry * S ((S (fom_index_pfp_unique_comparisoninput)) * c) + (fom_value_pfp_unique_comparisoninput))) /\ (exists fom_gap_pfp_unique_comparisoninput_value_bound. fom_gap_pfp_unique_comparisoninput_value_bound + S (fom_value_pfp_unique_comparisoninput) = p))) /\ (((forall pfp_repeat_index_unique_comparisonremoved. (exists pfa_gap_unique_comparisonremovedindex. pfa_gap_unique_comparisonremovedindex + S (pfp_repeat_index_unique_comparisonremoved) = (u)) -> (((exists ff_h_pfp_unique_comparisonremovedentry. ff_h_pfp_unique_comparisonremovedentry + S (0) = S ((S (pfp_repeat_index_unique_comparisonremoved)) * c)) /\ exists ff_q_pfp_unique_comparisonremovedentry. b = ff_q_pfp_unique_comparisonremovedentry * S ((S (pfp_repeat_index_unique_comparisonremoved)) * c) + (0)))) /\ (((forall pftrim_index_unique_comparisonsuffix pftrim_value_unique_comparisonsuffix. (exists pfa_gap_unique_comparisonsuffixbound. pfa_gap_unique_comparisonsuffixbound + S (pftrim_index_unique_comparisonsuffix) = (N)) -> (((exists ff_h_pfp_unique_comparisonsuffixsource. ff_h_pfp_unique_comparisonsuffixsource + S (pftrim_value_unique_comparisonsuffix) = S ((S ((u)+pftrim_index_unique_comparisonsuffix)) * c)) /\ exists ff_q_pfp_unique_comparisonsuffixsource. b = ff_q_pfp_unique_comparisonsuffixsource * S ((S ((u)+pftrim_index_unique_comparisonsuffix)) * c) + (pftrim_value_unique_comparisonsuffix))) -> (((exists ff_h_pfp_unique_comparisonsuffixoutput. ff_h_pfp_unique_comparisonsuffixoutput + S (pftrim_value_unique_comparisonsuffix) = S ((S (pftrim_index_unique_comparisonsuffix)) * g)) /\ exists ff_q_pfp_unique_comparisonsuffixoutput. f = ff_q_pfp_unique_comparisonsuffixoutput * S ((S (pftrim_index_unique_comparisonsuffix)) * g) + (pftrim_value_unique_comparisonsuffix)))) /\ (((N)=0 \/ (exists pftrim_leading_unique_comparisonnormal. ((((exists ff_h_pfp_unique_comparisonnormalentry. ff_h_pfp_unique_comparisonnormalentry + S (pftrim_leading_unique_comparisonnormal) = S ((S (0)) * g)) /\ exists ff_q_pfp_unique_comparisonnormalentry. f = ff_q_pfp_unique_comparisonnormalentry * S ((S (0)) * g) + (pftrim_leading_unique_comparisonnormal))) /\ ((~(pftrim_leading_unique_comparisonnormal=0))))))))))))))) -> (((t=u) /\ (((M=N) /\ ((forall mdr_i_pfp_exists_unique_values mdr_a_pfp_exists_unique_values. (exists mdr_gap_pfp_exists_unique_valuesb. mdr_gap_pfp_exists_unique_valuesb + S (mdr_i_pfp_exists_unique_values) = (M)) -> (((exists ff_h_mdr_pfp_exists_unique_valueso. ff_h_mdr_pfp_exists_unique_valueso + S (mdr_a_pfp_exists_unique_values) = S ((S (mdr_i_pfp_exists_unique_values)) * e)) /\ exists ff_q_mdr_pfp_exists_unique_valueso. d = ff_q_mdr_pfp_exists_unique_valueso * S ((S (mdr_i_pfp_exists_unique_values)) * e) + (mdr_a_pfp_exists_unique_values))) -> (((exists ff_h_mdr_pfp_exists_unique_valuesn. ff_h_mdr_pfp_exists_unique_valuesn + S (mdr_a_pfp_exists_unique_values) = S ((S (mdr_i_pfp_exists_unique_values)) * g)) /\ exists ff_q_mdr_pfp_exists_unique_valuesn. f = ff_q_mdr_pfp_exists_unique_valuesn * S ((S (mdr_i_pfp_exists_unique_values)) * g) + (mdr_a_pfp_exists_unique_values))))))))))))

Constructive proof overview

Generated structural guide

Construct an actual trim and prove unique removed count, retained length and decoded coefficients against every other actual trim.

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

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

Proof neighborhood

Direct dependencies

PQ0021 prime_field_polynomial_trim_exists PQ002A prime_field_polynomial_trim_removed_count_unique PQ002B prime_field_polynomial_trim_retained_length_unique PQ002C prime_field_polynomial_trim_output_equal

Direct dependents

none

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

74 script commands · 14 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 (4)
prime field polynomial trim existsprime field polynomial trim removed count uniqueprime field polynomial trim retained length uniqueprime field polynomial trim output equal

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

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro L
  5. L5
    intro hc
02Establish htL6–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial trim exists.

  1. L6
    have ht : ∃ t. ∃ d. ∃ e. ∃ M. FpPolynomialTrim(p,b,c,L,t,d,e,M)Definitions: FpPolynomialTrim
  2. L7
    specialize prime_field_polynomial_trim_exists (p)
  3. L8
    specialize prime_field_polynomial_trim_exists (b)
  4. L9
    specialize prime_field_polynomial_trim_exists (c)
  5. L10
    specialize prime_field_polynomial_trim_exists (L)
  6. L11
    apply prime_field_polynomial_trim_exists
  7. L12
    exact hc
03Separate the logical casesL13–16

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

  1. L13
    cases ht
  2. L14
    cases ht_witness
  3. L15
    cases ht_witness_witness
  4. L16
    cases ht_witness_witness_witness
04Construct an explicit witnessL17–20

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

  1. L17
    exists x
  2. L18
    exists x1
  3. L19
    exists x2
  4. L20
    exists x3
05Separate the logical casesL21–21

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

  1. L21
    split
06Use earlier factsL22–22

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

  1. L22
    exact ht_witness_witness_witness_witness
07Fix variables and assumptionsL23–27

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

  1. L23
    intro u
  2. L24
    intro f
  3. L25
    intro g
  4. L26
    intro N
  5. L27
    intro hk
08Separate the logical casesL28–28

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

  1. L28
    split
09Use earlier factsL29–38

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

  1. L29
    specialize prime_field_polynomial_trim_removed_count_unique (p)
  2. L30
    specialize prime_field_polynomial_trim_removed_count_unique (b)
  3. L31
    specialize prime_field_polynomial_trim_removed_count_unique (c)
  4. L32
    specialize prime_field_polynomial_trim_removed_count_unique (L)
  5. L33
    specialize prime_field_polynomial_trim_removed_count_unique (x)
  6. L34
    specialize prime_field_polynomial_trim_removed_count_unique (x1)
  7. L35
    specialize prime_field_polynomial_trim_removed_count_unique (x2)
  8. L36
    specialize prime_field_polynomial_trim_removed_count_unique (x3)
  9. L37
    specialize prime_field_polynomial_trim_removed_count_unique (u)
  10. L38
    specialize prime_field_polynomial_trim_removed_count_unique (f)
10Use earlier factsL39–43

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

  1. L39
    specialize prime_field_polynomial_trim_removed_count_unique (g)
  2. L40
    specialize prime_field_polynomial_trim_removed_count_unique (N)
  3. L41
    apply prime_field_polynomial_trim_removed_count_unique
  4. L42
    exact ht_witness_witness_witness_witness
  5. L43
    exact hk
11Separate the logical casesL44–44

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

  1. L44
    split
12Use earlier factsL45–54

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

  1. L45
    specialize prime_field_polynomial_trim_retained_length_unique (p)
  2. L46
    specialize prime_field_polynomial_trim_retained_length_unique (b)
  3. L47
    specialize prime_field_polynomial_trim_retained_length_unique (c)
  4. L48
    specialize prime_field_polynomial_trim_retained_length_unique (L)
  5. L49
    specialize prime_field_polynomial_trim_retained_length_unique (x)
  6. L50
    specialize prime_field_polynomial_trim_retained_length_unique (x1)
  7. L51
    specialize prime_field_polynomial_trim_retained_length_unique (x2)
  8. L52
    specialize prime_field_polynomial_trim_retained_length_unique (x3)
  9. L53
    specialize prime_field_polynomial_trim_retained_length_unique (u)
  10. L54
    specialize prime_field_polynomial_trim_retained_length_unique (f)
13Use earlier factsL55–64

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

  1. L55
    specialize prime_field_polynomial_trim_retained_length_unique (g)
  2. L56
    specialize prime_field_polynomial_trim_retained_length_unique (N)
  3. L57
    apply prime_field_polynomial_trim_retained_length_unique
  4. L58
    exact ht_witness_witness_witness_witness
  5. L59
    exact hk
  6. L60
    specialize prime_field_polynomial_trim_output_equal (p)
  7. L61
    specialize prime_field_polynomial_trim_output_equal (b)
  8. L62
    specialize prime_field_polynomial_trim_output_equal (c)
  9. L63
    specialize prime_field_polynomial_trim_output_equal (L)
  10. L64
    specialize prime_field_polynomial_trim_output_equal (x)
14Use earlier factsL65–74

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

  1. L65
    specialize prime_field_polynomial_trim_output_equal (x1)
  2. L66
    specialize prime_field_polynomial_trim_output_equal (x2)
  3. L67
    specialize prime_field_polynomial_trim_output_equal (x3)
  4. L68
    specialize prime_field_polynomial_trim_output_equal (u)
  5. L69
    specialize prime_field_polynomial_trim_output_equal (f)
  6. L70
    specialize prime_field_polynomial_trim_output_equal (g)
  7. L71
    specialize prime_field_polynomial_trim_output_equal (N)
  8. L72
    apply prime_field_polynomial_trim_output_equal
  9. L73
    exact ht_witness_witness_witness_witness
  10. L74
    exact hk

Library-wide reading audit

Original exact command ledger · 74 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro L
  5. 0005intro hc
  6. 0006have ht : exists t d e M. ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_exists_unique_choseninput. (exists fom_gap_pfp_exists_unique_choseninput_index_bound. fom_gap_pfp_exists_unique_choseninput_index_bound + S (fom_index_pfp_exists_unique_choseninput) = L) -> exists fom_value_pfp_exists_unique_choseninput. ((((exists fom_beta_height_pfp_exists_unique_choseninput_entry. fom_beta_height_pfp_exists_unique_choseninput_entry + S (fom_value_pfp_exists_unique_choseninput) = S ((S (fom_index_pfp_exists_unique_choseninput)) * c)) /\ exists fom_beta_quotient_pfp_exists_unique_choseninput_entry. b = fom_beta_quotient_pfp_exists_unique_choseninput_entry * S ((S (fom_index_pfp_exists_unique_choseninput)) * c) + (fom_value_pfp_exists_unique_choseninput))) /\ (exists fom_gap_pfp_exists_unique_choseninput_value_bound. fom_gap_pfp_exists_unique_choseninput_value_bound + S (fom_value_pfp_exists_unique_choseninput) = p))) /\ (((forall pfp_repeat_index_exists_unique_chosenremoved. (exists pfa_gap_exists_unique_chosenremovedindex. pfa_gap_exists_unique_chosenremovedindex + S (pfp_repeat_index_exists_unique_chosenremoved) = (t)) -> (((exists ff_h_pfp_exists_unique_chosenremovedentry. ff_h_pfp_exists_unique_chosenremovedentry + S (0) = S ((S (pfp_repeat_index_exists_unique_chosenremoved)) * c)) /\ exists ff_q_pfp_exists_unique_chosenremovedentry. b = ff_q_pfp_exists_unique_chosenremovedentry * S ((S (pfp_repeat_index_exists_unique_chosenremoved)) * c) + (0)))) /\ (((forall pftrim_index_exists_unique_chosensuffix pftrim_value_exists_unique_chosensuffix. (exists pfa_gap_exists_unique_chosensuffixbound. pfa_gap_exists_unique_chosensuffixbound + S (pftrim_index_exists_unique_chosensuffix) = (M)) -> (((exists ff_h_pfp_exists_unique_chosensuffixsource. ff_h_pfp_exists_unique_chosensuffixsource + S (pftrim_value_exists_unique_chosensuffix) = S ((S ((t)+pftrim_index_exists_unique_chosensuffix)) * c)) /\ exists ff_q_pfp_exists_unique_chosensuffixsource. b = ff_q_pfp_exists_unique_chosensuffixsource * S ((S ((t)+pftrim_index_exists_unique_chosensuffix)) * c) + (pftrim_value_exists_unique_chosensuffix))) -> (((exists ff_h_pfp_exists_unique_chosensuffixoutput. ff_h_pfp_exists_unique_chosensuffixoutput + S (pftrim_value_exists_unique_chosensuffix) = S ((S (pftrim_index_exists_unique_chosensuffix)) * e)) /\ exists ff_q_pfp_exists_unique_chosensuffixoutput. d = ff_q_pfp_exists_unique_chosensuffixoutput * S ((S (pftrim_index_exists_unique_chosensuffix)) * e) + (pftrim_value_exists_unique_chosensuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_exists_unique_chosennormal. ((((exists ff_h_pfp_exists_unique_chosennormalentry. ff_h_pfp_exists_unique_chosennormalentry + S (pftrim_leading_exists_unique_chosennormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_exists_unique_chosennormalentry. d = ff_q_pfp_exists_unique_chosennormalentry * S ((S (0)) * e) + (pftrim_leading_exists_unique_chosennormal))) /\ ((~(pftrim_leading_exists_unique_chosennormal=0)))))))))))))))
  7. 0007specialize prime_field_polynomial_trim_exists (p)
  8. 0008specialize prime_field_polynomial_trim_exists (b)
  9. 0009specialize prime_field_polynomial_trim_exists (c)
  10. 0010specialize prime_field_polynomial_trim_exists (L)
  11. 0011apply prime_field_polynomial_trim_exists
  12. 0012exact hc
  13. 0013cases ht
  14. 0014cases ht_witness
  15. 0015cases ht_witness_witness
  16. 0016cases ht_witness_witness_witness
  17. 0017exists x
  18. 0018exists x1
  19. 0019exists x2
  20. 0020exists x3
  21. 0021split
  22. 0022exact ht_witness_witness_witness_witness
  23. 0023intro u
  24. 0024intro f
  25. 0025intro g
  26. 0026intro N
  27. 0027intro hk
  28. 0028split
  29. 0029specialize prime_field_polynomial_trim_removed_count_unique (p)
  30. 0030specialize prime_field_polynomial_trim_removed_count_unique (b)
  31. 0031specialize prime_field_polynomial_trim_removed_count_unique (c)
  32. 0032specialize prime_field_polynomial_trim_removed_count_unique (L)
  33. 0033specialize prime_field_polynomial_trim_removed_count_unique (x)
  34. 0034specialize prime_field_polynomial_trim_removed_count_unique (x1)
  35. 0035specialize prime_field_polynomial_trim_removed_count_unique (x2)
  36. 0036specialize prime_field_polynomial_trim_removed_count_unique (x3)
  37. 0037specialize prime_field_polynomial_trim_removed_count_unique (u)
  38. 0038specialize prime_field_polynomial_trim_removed_count_unique (f)
  39. 0039specialize prime_field_polynomial_trim_removed_count_unique (g)
  40. 0040specialize prime_field_polynomial_trim_removed_count_unique (N)
  41. 0041apply prime_field_polynomial_trim_removed_count_unique
  42. 0042exact ht_witness_witness_witness_witness
  43. 0043exact hk
  44. 0044split
  45. 0045specialize prime_field_polynomial_trim_retained_length_unique (p)
  46. 0046specialize prime_field_polynomial_trim_retained_length_unique (b)
  47. 0047specialize prime_field_polynomial_trim_retained_length_unique (c)
  48. 0048specialize prime_field_polynomial_trim_retained_length_unique (L)
  49. 0049specialize prime_field_polynomial_trim_retained_length_unique (x)
  50. 0050specialize prime_field_polynomial_trim_retained_length_unique (x1)
  51. 0051specialize prime_field_polynomial_trim_retained_length_unique (x2)
  52. 0052specialize prime_field_polynomial_trim_retained_length_unique (x3)
  53. 0053specialize prime_field_polynomial_trim_retained_length_unique (u)
  54. 0054specialize prime_field_polynomial_trim_retained_length_unique (f)
  55. 0055specialize prime_field_polynomial_trim_retained_length_unique (g)
  56. 0056specialize prime_field_polynomial_trim_retained_length_unique (N)
  57. 0057apply prime_field_polynomial_trim_retained_length_unique
  58. 0058exact ht_witness_witness_witness_witness
  59. 0059exact hk
  60. 0060specialize prime_field_polynomial_trim_output_equal (p)
  61. 0061specialize prime_field_polynomial_trim_output_equal (b)
  62. 0062specialize prime_field_polynomial_trim_output_equal (c)
  63. 0063specialize prime_field_polynomial_trim_output_equal (L)
  64. 0064specialize prime_field_polynomial_trim_output_equal (x)
  65. 0065specialize prime_field_polynomial_trim_output_equal (x1)
  66. 0066specialize prime_field_polynomial_trim_output_equal (x2)
  67. 0067specialize prime_field_polynomial_trim_output_equal (x3)
  68. 0068specialize prime_field_polynomial_trim_output_equal (u)
  69. 0069specialize prime_field_polynomial_trim_output_equal (f)
  70. 0070specialize prime_field_polynomial_trim_output_equal (g)
  71. 0071specialize prime_field_polynomial_trim_output_equal (N)
  72. 0072apply prime_field_polynomial_trim_output_equal
  73. 0073exact ht_witness_witness_witness_witness
  74. 0074exact hk