PQ0029

prime_field_polynomial_trim_removed_le

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

One normalized cut cannot lie after another: otherwise a supposedly leading nonzero coefficient belongs to the other removed zero prefix.

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 t d e M u f g N. ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_unique_firstinput. (exists fom_gap_pfp_unique_firstinput_index_bound. fom_gap_pfp_unique_firstinput_index_bound + S (fom_index_pfp_unique_firstinput) = L) -> exists fom_value_pfp_unique_firstinput. ((((exists fom_beta_height_pfp_unique_firstinput_entry. fom_beta_height_pfp_unique_firstinput_entry + S (fom_value_pfp_unique_firstinput) = S ((S (fom_index_pfp_unique_firstinput)) * c)) /\ exists fom_beta_quotient_pfp_unique_firstinput_entry. b = fom_beta_quotient_pfp_unique_firstinput_entry * S ((S (fom_index_pfp_unique_firstinput)) * c) + (fom_value_pfp_unique_firstinput))) /\ (exists fom_gap_pfp_unique_firstinput_value_bound. fom_gap_pfp_unique_firstinput_value_bound + S (fom_value_pfp_unique_firstinput) = p))) /\ (((forall pfp_repeat_index_unique_firstremoved. (exists pfa_gap_unique_firstremovedindex. pfa_gap_unique_firstremovedindex + S (pfp_repeat_index_unique_firstremoved) = (t)) -> (((exists ff_h_pfp_unique_firstremovedentry. ff_h_pfp_unique_firstremovedentry + S (0) = S ((S (pfp_repeat_index_unique_firstremoved)) * c)) /\ exists ff_q_pfp_unique_firstremovedentry. b = ff_q_pfp_unique_firstremovedentry * S ((S (pfp_repeat_index_unique_firstremoved)) * c) + (0)))) /\ (((forall pftrim_index_unique_firstsuffix pftrim_value_unique_firstsuffix. (exists pfa_gap_unique_firstsuffixbound. pfa_gap_unique_firstsuffixbound + S (pftrim_index_unique_firstsuffix) = (M)) -> (((exists ff_h_pfp_unique_firstsuffixsource. ff_h_pfp_unique_firstsuffixsource + S (pftrim_value_unique_firstsuffix) = S ((S ((t)+pftrim_index_unique_firstsuffix)) * c)) /\ exists ff_q_pfp_unique_firstsuffixsource. b = ff_q_pfp_unique_firstsuffixsource * S ((S ((t)+pftrim_index_unique_firstsuffix)) * c) + (pftrim_value_unique_firstsuffix))) -> (((exists ff_h_pfp_unique_firstsuffixoutput. ff_h_pfp_unique_firstsuffixoutput + S (pftrim_value_unique_firstsuffix) = S ((S (pftrim_index_unique_firstsuffix)) * e)) /\ exists ff_q_pfp_unique_firstsuffixoutput. d = ff_q_pfp_unique_firstsuffixoutput * S ((S (pftrim_index_unique_firstsuffix)) * e) + (pftrim_value_unique_firstsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_unique_firstnormal. ((((exists ff_h_pfp_unique_firstnormalentry. ff_h_pfp_unique_firstnormalentry + S (pftrim_leading_unique_firstnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_unique_firstnormalentry. d = ff_q_pfp_unique_firstnormalentry * S ((S (0)) * e) + (pftrim_leading_unique_firstnormal))) /\ ((~(pftrim_leading_unique_firstnormal=0))))))))))))))) -> ((((L)=(u)+(N)) /\ (((forall fom_index_pfp_unique_secondinput. (exists fom_gap_pfp_unique_secondinput_index_bound. fom_gap_pfp_unique_secondinput_index_bound + S (fom_index_pfp_unique_secondinput) = L) -> exists fom_value_pfp_unique_secondinput. ((((exists fom_beta_height_pfp_unique_secondinput_entry. fom_beta_height_pfp_unique_secondinput_entry + S (fom_value_pfp_unique_secondinput) = S ((S (fom_index_pfp_unique_secondinput)) * c)) /\ exists fom_beta_quotient_pfp_unique_secondinput_entry. b = fom_beta_quotient_pfp_unique_secondinput_entry * S ((S (fom_index_pfp_unique_secondinput)) * c) + (fom_value_pfp_unique_secondinput))) /\ (exists fom_gap_pfp_unique_secondinput_value_bound. fom_gap_pfp_unique_secondinput_value_bound + S (fom_value_pfp_unique_secondinput) = p))) /\ (((forall pfp_repeat_index_unique_secondremoved. (exists pfa_gap_unique_secondremovedindex. pfa_gap_unique_secondremovedindex + S (pfp_repeat_index_unique_secondremoved) = (u)) -> (((exists ff_h_pfp_unique_secondremovedentry. ff_h_pfp_unique_secondremovedentry + S (0) = S ((S (pfp_repeat_index_unique_secondremoved)) * c)) /\ exists ff_q_pfp_unique_secondremovedentry. b = ff_q_pfp_unique_secondremovedentry * S ((S (pfp_repeat_index_unique_secondremoved)) * c) + (0)))) /\ (((forall pftrim_index_unique_secondsuffix pftrim_value_unique_secondsuffix. (exists pfa_gap_unique_secondsuffixbound. pfa_gap_unique_secondsuffixbound + S (pftrim_index_unique_secondsuffix) = (N)) -> (((exists ff_h_pfp_unique_secondsuffixsource. ff_h_pfp_unique_secondsuffixsource + S (pftrim_value_unique_secondsuffix) = S ((S ((u)+pftrim_index_unique_secondsuffix)) * c)) /\ exists ff_q_pfp_unique_secondsuffixsource. b = ff_q_pfp_unique_secondsuffixsource * S ((S ((u)+pftrim_index_unique_secondsuffix)) * c) + (pftrim_value_unique_secondsuffix))) -> (((exists ff_h_pfp_unique_secondsuffixoutput. ff_h_pfp_unique_secondsuffixoutput + S (pftrim_value_unique_secondsuffix) = S ((S (pftrim_index_unique_secondsuffix)) * g)) /\ exists ff_q_pfp_unique_secondsuffixoutput. f = ff_q_pfp_unique_secondsuffixoutput * S ((S (pftrim_index_unique_secondsuffix)) * g) + (pftrim_value_unique_secondsuffix)))) /\ (((N)=0 \/ (exists pftrim_leading_unique_secondnormal. ((((exists ff_h_pfp_unique_secondnormalentry. ff_h_pfp_unique_secondnormalentry + S (pftrim_leading_unique_secondnormal) = S ((S (0)) * g)) /\ exists ff_q_pfp_unique_secondnormalentry. f = ff_q_pfp_unique_secondnormalentry * S ((S (0)) * g) + (pftrim_leading_unique_secondnormal))) /\ ((~(pftrim_leading_unique_secondnormal=0))))))))))))))) -> (exists pftrim_gap_unique_removed_le. pftrim_gap_unique_removed_le+(t)=(u))

Constructive proof overview

Generated structural guide

One normalized cut cannot lie after another: otherwise a supposedly leading nonzero coefficient belongs to the other removed zero prefix.

The unchanged tactic script uses 5 declared prerequisites and contains 79 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PQ0024 prime_field_polynomial_trim_length_bounds le_or_lt Stable theorem; checked-use authorized eq_decidable Stable theorem; checked-use authorized lt_not_le Stable theorem; checked-use authorized PQ0025 prime_field_polynomial_trim_leading_source_nonzero

Direct dependents

PQ002A prime_field_polynomial_trim_removed_count_unique

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

79 script commands · 20 reading checkpoints · 7 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 (2)
prime field polynomial trim length boundsprime field polynomial trim leading source nonzero

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–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 L
  5. L5
    intro t
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro M
  9. L9
    intro u
  10. L10
    intro f
02Fix variables and assumptionsL11–14

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

  1. L11
    intro g
  2. L12
    intro N
  3. L13
    intro h
  4. L14
    intro hk
03Establish hboundL15–24

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

  1. L15
    have hbound : ((exists pftrim_gap_compare_t. pftrim_gap_compare_t+(t)=(L)) /\ ((exists pftrim_gap_compare_M. pftrim_gap_compare_M+(M)=(L))))
  2. L16
    specialize prime_field_polynomial_trim_length_bounds (p)
  3. L17
    specialize prime_field_polynomial_trim_length_bounds (b)
  4. L18
    specialize prime_field_polynomial_trim_length_bounds (c)
  5. L19
    specialize prime_field_polynomial_trim_length_bounds (L)
  6. L20
    specialize prime_field_polynomial_trim_length_bounds (t)
  7. L21
    specialize prime_field_polynomial_trim_length_bounds (d)
  8. L22
    specialize prime_field_polynomial_trim_length_bounds (e)
  9. L23
    specialize prime_field_polynomial_trim_length_bounds (M)
  10. L24
    apply prime_field_polynomial_trim_length_bounds
04Use earlier factsL25–25

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

  1. L25
    exact h
05Separate the logical casesL26–26

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

  1. L26
    cases hbound
06Establish horderL27–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le or lt.

  1. L27
    have horder : (exists pftrim_gap_compare_le. pftrim_gap_compare_le+(t)=(u)) \/ (exists pfa_gap_compare_lt. pfa_gap_compare_lt + S (u) = (t))
  2. L28
    specialize le_or_lt (t)
  3. L29
    specialize le_or_lt (u)
  4. L30
    apply le_or_lt
07Separate the logical casesL31–31

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

  1. L31
    cases horder
08Use earlier factsL32–32

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

  1. L32
    exact horder_left
09Separate the logical casesL33–33

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

  1. L33
    exfalso
10Establish hNL34–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eq decidable.

  1. L34
    have hN : N=0 \/ ~(N=0)
  2. L35
    specialize eq_decidable (N)
  3. L36
    specialize eq_decidable (0)
  4. L37
    apply eq_decidable
11Separate the logical casesL38–38

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

  1. L38
    cases hN
12Establish hkcopyL39–40

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

  1. L39
    have hkcopy : FpPolynomialTrim(p,b,c,L,u,f,g,N)Definitions: FpPolynomialTrim
  2. L40
    exact hk
13Separate the logical casesL41–44

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

  1. L41
    cases hkcopy
  2. L42
    cases hkcopy_right
  3. L43
    cases hkcopy_right_right
  4. L44
    cases hkcopy_right_right_right
14Establish hlenL45–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt not le.

  1. L45
    have hlen : L=u
  2. L46
    trans u+N
  3. L47
    exact hkcopy_left
  4. L48
    rewrite hN_left
  5. L49
    simp
  6. L50
    rewrite hlen at hbound_left
  7. L51
    specialize lt_not_le (u)
  8. L52
    specialize lt_not_le (t)
  9. L53
    apply lt_not_le
  10. L54
    exact horder_right
15Use earlier factsL55–55

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

  1. L55
    exact hbound_left
16Establish hcopyL56–57

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

  1. L56
    have hcopy : FpPolynomialTrim(p,b,c,L,t,d,e,M)Definitions: FpPolynomialTrim
  2. L57
    exact h
17Separate the logical casesL58–61

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

  1. L58
    cases hcopy
  2. L59
    cases hcopy_right
  3. L60
    cases hcopy_right_right
  4. L61
    cases hcopy_right_right_right
18Establish hzL62–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcopy right right left.

  1. L62
    have hz : ((exists ff_h_pfp_compare_zero. ff_h_pfp_compare_zero + S (0) = S ((S (u)) * c)) /\ exists ff_q_pfp_compare_zero. b = ff_q_pfp_compare_zero * S ((S (u)) * c) + (0))
  2. L63
    specialize hcopy_right_right_left (u)
  3. L64
    apply hcopy_right_right_left
  4. L65
    exact horder_right
  5. L66
    specialize prime_field_polynomial_trim_leading_source_nonzero (p)
  6. L67
    specialize prime_field_polynomial_trim_leading_source_nonzero (b)
  7. L68
    specialize prime_field_polynomial_trim_leading_source_nonzero (c)
  8. L69
    specialize prime_field_polynomial_trim_leading_source_nonzero (L)
  9. L70
    specialize prime_field_polynomial_trim_leading_source_nonzero (u)
  10. L71
    specialize prime_field_polynomial_trim_leading_source_nonzero (f)
19Use earlier factsL72–78

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

  1. L72
    specialize prime_field_polynomial_trim_leading_source_nonzero (g)
  2. L73
    specialize prime_field_polynomial_trim_leading_source_nonzero (N)
  3. L74
    specialize prime_field_polynomial_trim_leading_source_nonzero (0)
  4. L75
    apply prime_field_polynomial_trim_leading_source_nonzero
  5. L76
    exact hk
  6. L77
    exact hN_right
  7. L78
    exact hz
20Calculate and transport equalitiesL79–79

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

  1. L79
    refl

Library-wide reading audit

Original exact command ledger · 79 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro L
  5. 0005intro t
  6. 0006intro d
  7. 0007intro e
  8. 0008intro M
  9. 0009intro u
  10. 0010intro f
  11. 0011intro g
  12. 0012intro N
  13. 0013intro h
  14. 0014intro hk
  15. 0015have hbound : ((exists pftrim_gap_compare_t. pftrim_gap_compare_t+(t)=(L)) /\ ((exists pftrim_gap_compare_M. pftrim_gap_compare_M+(M)=(L))))
  16. 0016specialize prime_field_polynomial_trim_length_bounds (p)
  17. 0017specialize prime_field_polynomial_trim_length_bounds (b)
  18. 0018specialize prime_field_polynomial_trim_length_bounds (c)
  19. 0019specialize prime_field_polynomial_trim_length_bounds (L)
  20. 0020specialize prime_field_polynomial_trim_length_bounds (t)
  21. 0021specialize prime_field_polynomial_trim_length_bounds (d)
  22. 0022specialize prime_field_polynomial_trim_length_bounds (e)
  23. 0023specialize prime_field_polynomial_trim_length_bounds (M)
  24. 0024apply prime_field_polynomial_trim_length_bounds
  25. 0025exact h
  26. 0026cases hbound
  27. 0027have horder : (exists pftrim_gap_compare_le. pftrim_gap_compare_le+(t)=(u)) \/ (exists pfa_gap_compare_lt. pfa_gap_compare_lt + S (u) = (t))
  28. 0028specialize le_or_lt (t)
  29. 0029specialize le_or_lt (u)
  30. 0030apply le_or_lt
  31. 0031cases horder
  32. 0032exact horder_left
  33. 0033exfalso
  34. 0034have hN : N=0 \/ ~(N=0)
  35. 0035specialize eq_decidable (N)
  36. 0036specialize eq_decidable (0)
  37. 0037apply eq_decidable
  38. 0038cases hN
  39. 0039have hkcopy : (((L)=(u)+(N)) /\ (((forall fom_index_pfp_compare_second_copyinput. (exists fom_gap_pfp_compare_second_copyinput_index_bound. fom_gap_pfp_compare_second_copyinput_index_bound + S (fom_index_pfp_compare_second_copyinput) = L) -> exists fom_value_pfp_compare_second_copyinput. ((((exists fom_beta_height_pfp_compare_second_copyinput_entry. fom_beta_height_pfp_compare_second_copyinput_entry + S (fom_value_pfp_compare_second_copyinput) = S ((S (fom_index_pfp_compare_second_copyinput)) * c)) /\ exists fom_beta_quotient_pfp_compare_second_copyinput_entry. b = fom_beta_quotient_pfp_compare_second_copyinput_entry * S ((S (fom_index_pfp_compare_second_copyinput)) * c) + (fom_value_pfp_compare_second_copyinput))) /\ (exists fom_gap_pfp_compare_second_copyinput_value_bound. fom_gap_pfp_compare_second_copyinput_value_bound + S (fom_value_pfp_compare_second_copyinput) = p))) /\ (((forall pfp_repeat_index_compare_second_copyremoved. (exists pfa_gap_compare_second_copyremovedindex. pfa_gap_compare_second_copyremovedindex + S (pfp_repeat_index_compare_second_copyremoved) = (u)) -> (((exists ff_h_pfp_compare_second_copyremovedentry. ff_h_pfp_compare_second_copyremovedentry + S (0) = S ((S (pfp_repeat_index_compare_second_copyremoved)) * c)) /\ exists ff_q_pfp_compare_second_copyremovedentry. b = ff_q_pfp_compare_second_copyremovedentry * S ((S (pfp_repeat_index_compare_second_copyremoved)) * c) + (0)))) /\ (((forall pftrim_index_compare_second_copysuffix pftrim_value_compare_second_copysuffix. (exists pfa_gap_compare_second_copysuffixbound. pfa_gap_compare_second_copysuffixbound + S (pftrim_index_compare_second_copysuffix) = (N)) -> (((exists ff_h_pfp_compare_second_copysuffixsource. ff_h_pfp_compare_second_copysuffixsource + S (pftrim_value_compare_second_copysuffix) = S ((S ((u)+pftrim_index_compare_second_copysuffix)) * c)) /\ exists ff_q_pfp_compare_second_copysuffixsource. b = ff_q_pfp_compare_second_copysuffixsource * S ((S ((u)+pftrim_index_compare_second_copysuffix)) * c) + (pftrim_value_compare_second_copysuffix))) -> (((exists ff_h_pfp_compare_second_copysuffixoutput. ff_h_pfp_compare_second_copysuffixoutput + S (pftrim_value_compare_second_copysuffix) = S ((S (pftrim_index_compare_second_copysuffix)) * g)) /\ exists ff_q_pfp_compare_second_copysuffixoutput. f = ff_q_pfp_compare_second_copysuffixoutput * S ((S (pftrim_index_compare_second_copysuffix)) * g) + (pftrim_value_compare_second_copysuffix)))) /\ (((N)=0 \/ (exists pftrim_leading_compare_second_copynormal. ((((exists ff_h_pfp_compare_second_copynormalentry. ff_h_pfp_compare_second_copynormalentry + S (pftrim_leading_compare_second_copynormal) = S ((S (0)) * g)) /\ exists ff_q_pfp_compare_second_copynormalentry. f = ff_q_pfp_compare_second_copynormalentry * S ((S (0)) * g) + (pftrim_leading_compare_second_copynormal))) /\ ((~(pftrim_leading_compare_second_copynormal=0))))))))))))))
  40. 0040exact hk
  41. 0041cases hkcopy
  42. 0042cases hkcopy_right
  43. 0043cases hkcopy_right_right
  44. 0044cases hkcopy_right_right_right
  45. 0045have hlen : L=u
  46. 0046trans u+N
  47. 0047exact hkcopy_left
  48. 0048rewrite hN_left
  49. 0049simp
  50. 0050rewrite hlen at hbound_left
  51. 0051specialize lt_not_le (u)
  52. 0052specialize lt_not_le (t)
  53. 0053apply lt_not_le
  54. 0054exact horder_right
  55. 0055exact hbound_left
  56. 0056have hcopy : (((L)=(t)+(M)) /\ (((forall fom_index_pfp_compare_first_copyinput. (exists fom_gap_pfp_compare_first_copyinput_index_bound. fom_gap_pfp_compare_first_copyinput_index_bound + S (fom_index_pfp_compare_first_copyinput) = L) -> exists fom_value_pfp_compare_first_copyinput. ((((exists fom_beta_height_pfp_compare_first_copyinput_entry. fom_beta_height_pfp_compare_first_copyinput_entry + S (fom_value_pfp_compare_first_copyinput) = S ((S (fom_index_pfp_compare_first_copyinput)) * c)) /\ exists fom_beta_quotient_pfp_compare_first_copyinput_entry. b = fom_beta_quotient_pfp_compare_first_copyinput_entry * S ((S (fom_index_pfp_compare_first_copyinput)) * c) + (fom_value_pfp_compare_first_copyinput))) /\ (exists fom_gap_pfp_compare_first_copyinput_value_bound. fom_gap_pfp_compare_first_copyinput_value_bound + S (fom_value_pfp_compare_first_copyinput) = p))) /\ (((forall pfp_repeat_index_compare_first_copyremoved. (exists pfa_gap_compare_first_copyremovedindex. pfa_gap_compare_first_copyremovedindex + S (pfp_repeat_index_compare_first_copyremoved) = (t)) -> (((exists ff_h_pfp_compare_first_copyremovedentry. ff_h_pfp_compare_first_copyremovedentry + S (0) = S ((S (pfp_repeat_index_compare_first_copyremoved)) * c)) /\ exists ff_q_pfp_compare_first_copyremovedentry. b = ff_q_pfp_compare_first_copyremovedentry * S ((S (pfp_repeat_index_compare_first_copyremoved)) * c) + (0)))) /\ (((forall pftrim_index_compare_first_copysuffix pftrim_value_compare_first_copysuffix. (exists pfa_gap_compare_first_copysuffixbound. pfa_gap_compare_first_copysuffixbound + S (pftrim_index_compare_first_copysuffix) = (M)) -> (((exists ff_h_pfp_compare_first_copysuffixsource. ff_h_pfp_compare_first_copysuffixsource + S (pftrim_value_compare_first_copysuffix) = S ((S ((t)+pftrim_index_compare_first_copysuffix)) * c)) /\ exists ff_q_pfp_compare_first_copysuffixsource. b = ff_q_pfp_compare_first_copysuffixsource * S ((S ((t)+pftrim_index_compare_first_copysuffix)) * c) + (pftrim_value_compare_first_copysuffix))) -> (((exists ff_h_pfp_compare_first_copysuffixoutput. ff_h_pfp_compare_first_copysuffixoutput + S (pftrim_value_compare_first_copysuffix) = S ((S (pftrim_index_compare_first_copysuffix)) * e)) /\ exists ff_q_pfp_compare_first_copysuffixoutput. d = ff_q_pfp_compare_first_copysuffixoutput * S ((S (pftrim_index_compare_first_copysuffix)) * e) + (pftrim_value_compare_first_copysuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_compare_first_copynormal. ((((exists ff_h_pfp_compare_first_copynormalentry. ff_h_pfp_compare_first_copynormalentry + S (pftrim_leading_compare_first_copynormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_compare_first_copynormalentry. d = ff_q_pfp_compare_first_copynormalentry * S ((S (0)) * e) + (pftrim_leading_compare_first_copynormal))) /\ ((~(pftrim_leading_compare_first_copynormal=0))))))))))))))
  57. 0057exact h
  58. 0058cases hcopy
  59. 0059cases hcopy_right
  60. 0060cases hcopy_right_right
  61. 0061cases hcopy_right_right_right
  62. 0062have hz : ((exists ff_h_pfp_compare_zero. ff_h_pfp_compare_zero + S (0) = S ((S (u)) * c)) /\ exists ff_q_pfp_compare_zero. b = ff_q_pfp_compare_zero * S ((S (u)) * c) + (0))
  63. 0063specialize hcopy_right_right_left (u)
  64. 0064apply hcopy_right_right_left
  65. 0065exact horder_right
  66. 0066specialize prime_field_polynomial_trim_leading_source_nonzero (p)
  67. 0067specialize prime_field_polynomial_trim_leading_source_nonzero (b)
  68. 0068specialize prime_field_polynomial_trim_leading_source_nonzero (c)
  69. 0069specialize prime_field_polynomial_trim_leading_source_nonzero (L)
  70. 0070specialize prime_field_polynomial_trim_leading_source_nonzero (u)
  71. 0071specialize prime_field_polynomial_trim_leading_source_nonzero (f)
  72. 0072specialize prime_field_polynomial_trim_leading_source_nonzero (g)
  73. 0073specialize prime_field_polynomial_trim_leading_source_nonzero (N)
  74. 0074specialize prime_field_polynomial_trim_leading_source_nonzero (0)
  75. 0075apply prime_field_polynomial_trim_leading_source_nonzero
  76. 0076exact hk
  77. 0077exact hN_right
  78. 0078exact hz
  79. 0079refl