PQ0055

prime_field_polynomial_synthetic_zero_remainder_iff

The actual synthetic remainder vanishes exactly when the actual input evaluation at a vanishes; a general convolution factor theorem remains a separate obligation.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ a. ∀ n. ∀ qb. ∀ qc. ∀ r. Prime(p) → FpSyntheticDivision(p,b,c,a,n,qb,qc,r) → (r = 0 → FpHorner(p,b,c,a,S n,0)) ∧ (FpHorner(p,b,c,a,S n,0) → r = 0)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

FpHorner(p,b,c,x,l,r) · 3FpSyntheticDivision(p,b,c,a,n,qb,qc,r) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_synthetic_remainder_executionprime_field_polynomial_horner_functional · checked external prerequisite
Original expanded first-order statement 
forall p b c a n qb qc r. (~((p) = 1) /\ forall pfa_factor_left_root_prime pfa_factor_right_root_prime. (p) = pfa_factor_left_root_prime * pfa_factor_right_root_prime -> pfa_factor_left_root_prime = 1 \/ pfa_factor_right_root_prime = 1) -> (exists pfs_history_code_root_division pfs_history_scale_root_division. ((((exists pfa_gap_root_divisiontracebase. pfa_gap_root_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_root_divisiontraceinitial. ff_h_pfp_root_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_root_division)) /\ exists ff_q_pfp_root_divisiontraceinitial. pfs_history_code_root_division = ff_q_pfp_root_divisiontraceinitial * S ((S (0)) * pfs_history_scale_root_division) + (0))) /\ (((((exists ff_h_pfp_root_divisiontraceterminal. ff_h_pfp_root_divisiontraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_root_division)) /\ exists ff_q_pfp_root_divisiontraceterminal. pfs_history_code_root_division = ff_q_pfp_root_divisiontraceterminal * S ((S (S (n))) * pfs_history_scale_root_division) + (r))) /\ ((forall pfh_index_root_divisiontracesteps. (exists pfa_gap_root_divisiontracestepsindex. pfa_gap_root_divisiontracestepsindex + S (pfh_index_root_divisiontracesteps) = (S (n))) -> (exists pfh_coefficient_root_divisiontracestepsstep pfh_before_root_divisiontracestepsstep pfh_after_root_divisiontracestepsstep pfh_product_root_divisiontracestepsstep. ((((exists ff_h_pfp_root_divisiontracestepsstepcoefficient. ff_h_pfp_root_divisiontracestepsstepcoefficient + S (pfh_coefficient_root_divisiontracestepsstep) = S ((S (pfh_index_root_divisiontracesteps)) * c)) /\ exists ff_q_pfp_root_divisiontracestepsstepcoefficient. b = ff_q_pfp_root_divisiontracestepsstepcoefficient * S ((S (pfh_index_root_divisiontracesteps)) * c) + (pfh_coefficient_root_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_root_divisiontracestepsstepbefore. ff_h_pfp_root_divisiontracestepsstepbefore + S (pfh_before_root_divisiontracestepsstep) = S ((S (pfh_index_root_divisiontracesteps)) * pfs_history_scale_root_division)) /\ exists ff_q_pfp_root_divisiontracestepsstepbefore. pfs_history_code_root_division = ff_q_pfp_root_divisiontracestepsstepbefore * S ((S (pfh_index_root_divisiontracesteps)) * pfs_history_scale_root_division) + (pfh_before_root_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_root_divisiontracestepsstepafter. ff_h_pfp_root_divisiontracestepsstepafter + S (pfh_after_root_divisiontracestepsstep) = S ((S (S (pfh_index_root_divisiontracesteps))) * pfs_history_scale_root_division)) /\ exists ff_q_pfp_root_divisiontracestepsstepafter. pfs_history_code_root_division = ff_q_pfp_root_divisiontracestepsstepafter * S ((S (S (pfh_index_root_divisiontracesteps))) * pfs_history_scale_root_division) + (pfh_after_root_divisiontracestepsstep))) /\ (((((exists pfa_gap_root_divisiontracestepsstepmultiplyleft. pfa_gap_root_divisiontracestepsstepmultiplyleft + S (pfh_before_root_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_root_divisiontracestepsstepmultiplyright. pfa_gap_root_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_root_divisiontracestepsstepmultiplyresultbound. pfa_gap_root_divisiontracestepsstepmultiplyresultbound + S (pfh_product_root_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_root_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_root_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_root_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_root_divisiontracestepsstep) + (p) * pfa_offset_right_root_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_root_divisiontracestepsstepaddleft. pfa_gap_root_divisiontracestepsstepaddleft + S (pfh_product_root_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_root_divisiontracestepsstepaddright. pfa_gap_root_divisiontracestepsstepaddright + S (pfh_coefficient_root_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_root_divisiontracestepsstepaddresultbound. pfa_gap_root_divisiontracestepsstepaddresultbound + S (pfh_after_root_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_divisiontracestepsstepaddresultcongruence pfa_offset_right_root_divisiontracestepsstepaddresultcongruence. ((pfh_product_root_divisiontracestepsstep) + (pfh_coefficient_root_divisiontracestepsstep)) + (p) * pfa_offset_left_root_divisiontracestepsstepaddresultcongruence = (pfh_after_root_divisiontracestepsstep) + (p) * pfa_offset_right_root_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_root_divisionquotient ff_source_mcp_pfs_root_divisionquotient ff_target_mcp_pfs_root_divisionquotient. (exists mcp_gap_pfs_root_divisionquotient_bound. mcp_gap_pfs_root_divisionquotient_bound + S (ff_index_mcp_pfs_root_divisionquotient) = (n)) -> (((exists fs_h_mcp_pfs_root_divisionquotient_source. fs_h_mcp_pfs_root_divisionquotient_source + S (ff_source_mcp_pfs_root_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_root_divisionquotient)) * pfs_history_scale_root_division)) /\ exists fs_q_mcp_pfs_root_divisionquotient_source. pfs_history_code_root_division = fs_q_mcp_pfs_root_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_root_divisionquotient)) * pfs_history_scale_root_division) + (ff_source_mcp_pfs_root_divisionquotient))) -> (((exists fs_h_mcp_pfs_root_divisionquotient_target. fs_h_mcp_pfs_root_divisionquotient_target + S (ff_target_mcp_pfs_root_divisionquotient) = S ((S (ff_index_mcp_pfs_root_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_root_divisionquotient_target. qb = fs_q_mcp_pfs_root_divisionquotient_target * S ((S (ff_index_mcp_pfs_root_divisionquotient)) * qc) + (ff_target_mcp_pfs_root_divisionquotient))) -> ff_target_mcp_pfs_root_divisionquotient = ff_source_mcp_pfs_root_divisionquotient)))) -> ((r=0 -> (exists pfh_trace_code_root_forward pfh_trace_scale_root_forward. (((exists pfa_gap_root_forwardtracebase. pfa_gap_root_forwardtracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_root_forwardtraceinitial. ff_h_pfp_root_forwardtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_root_forward)) /\ exists ff_q_pfp_root_forwardtraceinitial. pfh_trace_code_root_forward = ff_q_pfp_root_forwardtraceinitial * S ((S (0)) * pfh_trace_scale_root_forward) + (0))) /\ (((((exists ff_h_pfp_root_forwardtraceterminal. ff_h_pfp_root_forwardtraceterminal + S (0) = S ((S (S n)) * pfh_trace_scale_root_forward)) /\ exists ff_q_pfp_root_forwardtraceterminal. pfh_trace_code_root_forward = ff_q_pfp_root_forwardtraceterminal * S ((S (S n)) * pfh_trace_scale_root_forward) + (0))) /\ ((forall pfh_index_root_forwardtracesteps. (exists pfa_gap_root_forwardtracestepsindex. pfa_gap_root_forwardtracestepsindex + S (pfh_index_root_forwardtracesteps) = (S n)) -> (exists pfh_coefficient_root_forwardtracestepsstep pfh_before_root_forwardtracestepsstep pfh_after_root_forwardtracestepsstep pfh_product_root_forwardtracestepsstep. ((((exists ff_h_pfp_root_forwardtracestepsstepcoefficient. ff_h_pfp_root_forwardtracestepsstepcoefficient + S (pfh_coefficient_root_forwardtracestepsstep) = S ((S (pfh_index_root_forwardtracesteps)) * c)) /\ exists ff_q_pfp_root_forwardtracestepsstepcoefficient. b = ff_q_pfp_root_forwardtracestepsstepcoefficient * S ((S (pfh_index_root_forwardtracesteps)) * c) + (pfh_coefficient_root_forwardtracestepsstep))) /\ (((((exists ff_h_pfp_root_forwardtracestepsstepbefore. ff_h_pfp_root_forwardtracestepsstepbefore + S (pfh_before_root_forwardtracestepsstep) = S ((S (pfh_index_root_forwardtracesteps)) * pfh_trace_scale_root_forward)) /\ exists ff_q_pfp_root_forwardtracestepsstepbefore. pfh_trace_code_root_forward = ff_q_pfp_root_forwardtracestepsstepbefore * S ((S (pfh_index_root_forwardtracesteps)) * pfh_trace_scale_root_forward) + (pfh_before_root_forwardtracestepsstep))) /\ (((((exists ff_h_pfp_root_forwardtracestepsstepafter. ff_h_pfp_root_forwardtracestepsstepafter + S (pfh_after_root_forwardtracestepsstep) = S ((S (S (pfh_index_root_forwardtracesteps))) * pfh_trace_scale_root_forward)) /\ exists ff_q_pfp_root_forwardtracestepsstepafter. pfh_trace_code_root_forward = ff_q_pfp_root_forwardtracestepsstepafter * S ((S (S (pfh_index_root_forwardtracesteps))) * pfh_trace_scale_root_forward) + (pfh_after_root_forwardtracestepsstep))) /\ (((((exists pfa_gap_root_forwardtracestepsstepmultiplyleft. pfa_gap_root_forwardtracestepsstepmultiplyleft + S (pfh_before_root_forwardtracestepsstep) = (p)) /\ (((exists pfa_gap_root_forwardtracestepsstepmultiplyright. pfa_gap_root_forwardtracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_root_forwardtracestepsstepmultiplyresultbound. pfa_gap_root_forwardtracestepsstepmultiplyresultbound + S (pfh_product_root_forwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_forwardtracestepsstepmultiplyresultcongruence pfa_offset_right_root_forwardtracestepsstepmultiplyresultcongruence. ((pfh_before_root_forwardtracestepsstep) * (a)) + (p) * pfa_offset_left_root_forwardtracestepsstepmultiplyresultcongruence = (pfh_product_root_forwardtracestepsstep) + (p) * pfa_offset_right_root_forwardtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_root_forwardtracestepsstepaddleft. pfa_gap_root_forwardtracestepsstepaddleft + S (pfh_product_root_forwardtracestepsstep) = (p)) /\ (((exists pfa_gap_root_forwardtracestepsstepaddright. pfa_gap_root_forwardtracestepsstepaddright + S (pfh_coefficient_root_forwardtracestepsstep) = (p)) /\ ((((exists pfa_gap_root_forwardtracestepsstepaddresultbound. pfa_gap_root_forwardtracestepsstepaddresultbound + S (pfh_after_root_forwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_forwardtracestepsstepaddresultcongruence pfa_offset_right_root_forwardtracestepsstepaddresultcongruence. ((pfh_product_root_forwardtracestepsstep) + (pfh_coefficient_root_forwardtracestepsstep)) + (p) * pfa_offset_left_root_forwardtracestepsstepaddresultcongruence = (pfh_after_root_forwardtracestepsstep) + (p) * pfa_offset_right_root_forwardtracestepsstepaddresultcongruence)))))))))))))))))))))))))))) /\ (((exists pfh_trace_code_root_backward pfh_trace_scale_root_backward. (((exists pfa_gap_root_backwardtracebase. pfa_gap_root_backwardtracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_root_backwardtraceinitial. ff_h_pfp_root_backwardtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_root_backward)) /\ exists ff_q_pfp_root_backwardtraceinitial. pfh_trace_code_root_backward = ff_q_pfp_root_backwardtraceinitial * S ((S (0)) * pfh_trace_scale_root_backward) + (0))) /\ (((((exists ff_h_pfp_root_backwardtraceterminal. ff_h_pfp_root_backwardtraceterminal + S (0) = S ((S (S n)) * pfh_trace_scale_root_backward)) /\ exists ff_q_pfp_root_backwardtraceterminal. pfh_trace_code_root_backward = ff_q_pfp_root_backwardtraceterminal * S ((S (S n)) * pfh_trace_scale_root_backward) + (0))) /\ ((forall pfh_index_root_backwardtracesteps. (exists pfa_gap_root_backwardtracestepsindex. pfa_gap_root_backwardtracestepsindex + S (pfh_index_root_backwardtracesteps) = (S n)) -> (exists pfh_coefficient_root_backwardtracestepsstep pfh_before_root_backwardtracestepsstep pfh_after_root_backwardtracestepsstep pfh_product_root_backwardtracestepsstep. ((((exists ff_h_pfp_root_backwardtracestepsstepcoefficient. ff_h_pfp_root_backwardtracestepsstepcoefficient + S (pfh_coefficient_root_backwardtracestepsstep) = S ((S (pfh_index_root_backwardtracesteps)) * c)) /\ exists ff_q_pfp_root_backwardtracestepsstepcoefficient. b = ff_q_pfp_root_backwardtracestepsstepcoefficient * S ((S (pfh_index_root_backwardtracesteps)) * c) + (pfh_coefficient_root_backwardtracestepsstep))) /\ (((((exists ff_h_pfp_root_backwardtracestepsstepbefore. ff_h_pfp_root_backwardtracestepsstepbefore + S (pfh_before_root_backwardtracestepsstep) = S ((S (pfh_index_root_backwardtracesteps)) * pfh_trace_scale_root_backward)) /\ exists ff_q_pfp_root_backwardtracestepsstepbefore. pfh_trace_code_root_backward = ff_q_pfp_root_backwardtracestepsstepbefore * S ((S (pfh_index_root_backwardtracesteps)) * pfh_trace_scale_root_backward) + (pfh_before_root_backwardtracestepsstep))) /\ (((((exists ff_h_pfp_root_backwardtracestepsstepafter. ff_h_pfp_root_backwardtracestepsstepafter + S (pfh_after_root_backwardtracestepsstep) = S ((S (S (pfh_index_root_backwardtracesteps))) * pfh_trace_scale_root_backward)) /\ exists ff_q_pfp_root_backwardtracestepsstepafter. pfh_trace_code_root_backward = ff_q_pfp_root_backwardtracestepsstepafter * S ((S (S (pfh_index_root_backwardtracesteps))) * pfh_trace_scale_root_backward) + (pfh_after_root_backwardtracestepsstep))) /\ (((((exists pfa_gap_root_backwardtracestepsstepmultiplyleft. pfa_gap_root_backwardtracestepsstepmultiplyleft + S (pfh_before_root_backwardtracestepsstep) = (p)) /\ (((exists pfa_gap_root_backwardtracestepsstepmultiplyright. pfa_gap_root_backwardtracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_root_backwardtracestepsstepmultiplyresultbound. pfa_gap_root_backwardtracestepsstepmultiplyresultbound + S (pfh_product_root_backwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_backwardtracestepsstepmultiplyresultcongruence pfa_offset_right_root_backwardtracestepsstepmultiplyresultcongruence. ((pfh_before_root_backwardtracestepsstep) * (a)) + (p) * pfa_offset_left_root_backwardtracestepsstepmultiplyresultcongruence = (pfh_product_root_backwardtracestepsstep) + (p) * pfa_offset_right_root_backwardtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_root_backwardtracestepsstepaddleft. pfa_gap_root_backwardtracestepsstepaddleft + S (pfh_product_root_backwardtracestepsstep) = (p)) /\ (((exists pfa_gap_root_backwardtracestepsstepaddright. pfa_gap_root_backwardtracestepsstepaddright + S (pfh_coefficient_root_backwardtracestepsstep) = (p)) /\ ((((exists pfa_gap_root_backwardtracestepsstepaddresultbound. pfa_gap_root_backwardtracestepsstepaddresultbound + S (pfh_after_root_backwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_backwardtracestepsstepaddresultcongruence pfa_offset_right_root_backwardtracestepsstepaddresultcongruence. ((pfh_product_root_backwardtracestepsstep) + (pfh_coefficient_root_backwardtracestepsstep)) + (p) * pfa_offset_left_root_backwardtracestepsstepaddresultcongruence = (pfh_after_root_backwardtracestepsstep) + (p) * pfa_offset_right_root_backwardtracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> r=0)))

Complete tactic proof in conservative notation

All 38 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

38 script commands · 10 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
prime field polynomial synthetic remainder execution
01Fix variables and assumptionsL1–10

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 a
  5. L5
    intro n
  6. L6
    intro qb
  7. L7
    intro qc
  8. L8
    intro r
  9. L9
    intro hp
  10. L10
    intro hs
02Establish heL11–20

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

  1. L11
    have he : FpHorner(p,b,c,a,S n,r)Definitions: FpHorner(p,b,c,a,S n,r)Original native command in the exact edition
  2. L12
    specialize prime_field_polynomial_synthetic_remainder_execution (p)
  3. L13
    specialize prime_field_polynomial_synthetic_remainder_execution (b)
  4. L14
    specialize prime_field_polynomial_synthetic_remainder_execution (c)
  5. L15
    specialize prime_field_polynomial_synthetic_remainder_execution (a)
  6. L16
    specialize prime_field_polynomial_synthetic_remainder_execution (n)
  7. L17
    specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  8. L18
    specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  9. L19
    specialize prime_field_polynomial_synthetic_remainder_execution (r)
  10. L20
    apply prime_field_polynomial_synthetic_remainder_execution
03Use earlier factsL21–21

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

  1. L21
    exact hs
04Separate the logical casesL22–22

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

  1. L22
    split
05Fix variables and assumptionsL23–23

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

  1. L23
    intro hz
06Calculate and transport equalitiesL24–25

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L24
    rewrite hz at he
  2. L25
    rewrite hz at he
07Use earlier factsL26–26

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

  1. L26
    exact he
08Fix variables and assumptionsL27–27

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

  1. L27
    intro hz
09Use earlier factsL28–37

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

  1. L28
    specialize prime_field_polynomial_horner_functional (p)
  2. L29
    specialize prime_field_polynomial_horner_functional (b)
  3. L30
    specialize prime_field_polynomial_horner_functional (c)
  4. L31
    specialize prime_field_polynomial_horner_functional (a)
  5. L32
    specialize prime_field_polynomial_horner_functional (S n)
  6. L33
    specialize prime_field_polynomial_horner_functional (r)
  7. L34
    specialize prime_field_polynomial_horner_functional (0)
  8. L35
    apply prime_field_polynomial_horner_functional
  9. L36
    exact hp
  10. L37
    exact he
10Use earlier factsL38–38

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

  1. L38
    exact hz

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro a
  5. 0005intro n
  6. 0006intro qb
  7. 0007intro qc
  8. 0008intro r
  9. 0009intro hp
  10. 0010intro hs
  11. 0011have he : FpHorner(p,b,c,a,S n,r)
  12. 0012specialize prime_field_polynomial_synthetic_remainder_execution (p)
  13. 0013specialize prime_field_polynomial_synthetic_remainder_execution (b)
  14. 0014specialize prime_field_polynomial_synthetic_remainder_execution (c)
  15. 0015specialize prime_field_polynomial_synthetic_remainder_execution (a)
  16. 0016specialize prime_field_polynomial_synthetic_remainder_execution (n)
  17. 0017specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  18. 0018specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  19. 0019specialize prime_field_polynomial_synthetic_remainder_execution (r)
  20. 0020apply prime_field_polynomial_synthetic_remainder_execution
  21. 0021exact hs
  22. 0022split
  23. 0023intro hz
  24. 0024rewrite hz at he
  25. 0025rewrite hz at he
  26. 0026exact he
  27. 0027intro hz
  28. 0028specialize prime_field_polynomial_horner_functional (p)
  29. 0029specialize prime_field_polynomial_horner_functional (b)
  30. 0030specialize prime_field_polynomial_horner_functional (c)
  31. 0031specialize prime_field_polynomial_horner_functional (a)
  32. 0032specialize prime_field_polynomial_horner_functional (S n)
  33. 0033specialize prime_field_polynomial_horner_functional (r)
  34. 0034specialize prime_field_polynomial_horner_functional (0)
  35. 0035apply prime_field_polynomial_horner_functional
  36. 0036exact hp
  37. 0037exact he
  38. 0038exact hz