PG0034

prime_field_polynomial_right_divides_reflexive

Every canonical polynomial right-divides itself using a constructed left unit and actual product. Empty and zero prefixes are included, without assuming commutative multiplication.

Alpha v34 checked-use · first admitted v34 · 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 products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. Prime(p) → BetaPrefixInto(ab,ac,L,p) → FpPolynomialRightDivides(p,ab,ac,L,ab,ac,L)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 2FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 1PolynomialEquivalent(b,c,L,d,e,M) · 1FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

prime_field_polynomial_convolution_left_unit_existsprime_field_polynomial_right_divides_from_product
Original expanded first-order statement 
forall p ab ac L. (~((p) = 1) /\ forall pfa_factor_left_unit_divides_prime pfa_factor_right_unit_divides_prime. (p) = pfa_factor_left_unit_divides_prime * pfa_factor_right_unit_divides_prime -> pfa_factor_left_unit_divides_prime = 1 \/ pfa_factor_right_unit_divides_prime = 1) -> (forall fom_index_pfp_unit_divides_A. (exists fom_gap_pfp_unit_divides_A_index_bound. fom_gap_pfp_unit_divides_A_index_bound + S (fom_index_pfp_unit_divides_A) = L) -> exists fom_value_pfp_unit_divides_A. ((((exists fom_beta_height_pfp_unit_divides_A_entry. fom_beta_height_pfp_unit_divides_A_entry + S (fom_value_pfp_unit_divides_A) = S ((S (fom_index_pfp_unit_divides_A)) * ac)) /\ exists fom_beta_quotient_pfp_unit_divides_A_entry. ab = fom_beta_quotient_pfp_unit_divides_A_entry * S ((S (fom_index_pfp_unit_divides_A)) * ac) + (fom_value_pfp_unit_divides_A))) /\ (exists fom_gap_pfp_unit_divides_A_value_bound. fom_gap_pfp_unit_divides_A_value_bound + S (fom_value_pfp_unit_divides_A) = p))) -> (((forall fom_index_pfp_unit_divides_bound. (exists fom_gap_pfp_unit_divides_bound_index_bound. fom_gap_pfp_unit_divides_bound_index_bound + S (fom_index_pfp_unit_divides_bound) = L) -> exists fom_value_pfp_unit_divides_bound. ((((exists fom_beta_height_pfp_unit_divides_bound_entry. fom_beta_height_pfp_unit_divides_bound_entry + S (fom_value_pfp_unit_divides_bound) = S ((S (fom_index_pfp_unit_divides_bound)) * ac)) /\ exists fom_beta_quotient_pfp_unit_divides_bound_entry. ab = fom_beta_quotient_pfp_unit_divides_bound_entry * S ((S (fom_index_pfp_unit_divides_bound)) * ac) + (fom_value_pfp_unit_divides_bound))) /\ (exists fom_gap_pfp_unit_divides_bound_value_bound. fom_gap_pfp_unit_divides_bound_value_bound + S (fom_value_pfp_unit_divides_bound) = p))) /\ ((exists qb qc Q pb pc P. ((((forall fom_index_pfp_unit_divides_productleft. (exists fom_gap_pfp_unit_divides_productleft_index_bound. fom_gap_pfp_unit_divides_productleft_index_bound + S (fom_index_pfp_unit_divides_productleft) = Q) -> exists fom_value_pfp_unit_divides_productleft. ((((exists fom_beta_height_pfp_unit_divides_productleft_entry. fom_beta_height_pfp_unit_divides_productleft_entry + S (fom_value_pfp_unit_divides_productleft) = S ((S (fom_index_pfp_unit_divides_productleft)) * qc)) /\ exists fom_beta_quotient_pfp_unit_divides_productleft_entry. qb = fom_beta_quotient_pfp_unit_divides_productleft_entry * S ((S (fom_index_pfp_unit_divides_productleft)) * qc) + (fom_value_pfp_unit_divides_productleft))) /\ (exists fom_gap_pfp_unit_divides_productleft_value_bound. fom_gap_pfp_unit_divides_productleft_value_bound + S (fom_value_pfp_unit_divides_productleft) = p))) /\ (((forall fom_index_pfp_unit_divides_productright. (exists fom_gap_pfp_unit_divides_productright_index_bound. fom_gap_pfp_unit_divides_productright_index_bound + S (fom_index_pfp_unit_divides_productright) = L) -> exists fom_value_pfp_unit_divides_productright. ((((exists fom_beta_height_pfp_unit_divides_productright_entry. fom_beta_height_pfp_unit_divides_productright_entry + S (fom_value_pfp_unit_divides_productright) = S ((S (fom_index_pfp_unit_divides_productright)) * ac)) /\ exists fom_beta_quotient_pfp_unit_divides_productright_entry. ab = fom_beta_quotient_pfp_unit_divides_productright_entry * S ((S (fom_index_pfp_unit_divides_productright)) * ac) + (fom_value_pfp_unit_divides_productright))) /\ (exists fom_gap_pfp_unit_divides_productright_value_bound. fom_gap_pfp_unit_divides_productright_value_bound + S (fom_value_pfp_unit_divides_productright) = p))) /\ (((((((Q)=0 \/ (L)=0) /\ (((P)=0)))) \/ (((~((Q)=0)) /\ (((~((L)=0)) /\ (((Q)+(L)=S (P)))))))) /\ ((forall pfc_index_unit_divides_productcoefficients. (exists pfa_gap_unit_divides_productcoefficientsbound. pfa_gap_unit_divides_productcoefficientsbound + S (pfc_index_unit_divides_productcoefficients) = (P)) -> exists pfc_value_unit_divides_productcoefficients. ((((exists ff_h_pfp_unit_divides_productcoefficientsentry. ff_h_pfp_unit_divides_productcoefficientsentry + S (pfc_value_unit_divides_productcoefficients) = S ((S (pfc_index_unit_divides_productcoefficients)) * pc)) /\ exists ff_q_pfp_unit_divides_productcoefficientsentry. pb = ff_q_pfp_unit_divides_productcoefficientsentry * S ((S (pfc_index_unit_divides_productcoefficients)) * pc) + (pfc_value_unit_divides_productcoefficients))) /\ ((exists pfc_terms_code_unit_divides_productcoefficientscoefficient pfc_terms_scale_unit_divides_productcoefficientscoefficient pfc_natural_sum_unit_divides_productcoefficientscoefficient. ((forall pfc_index_unit_divides_productcoefficientscoefficientdiagonal. (exists pfa_gap_unit_divides_productcoefficientscoefficientdiagonalbound. pfa_gap_unit_divides_productcoefficientscoefficientdiagonalbound + S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal) = (S (pfc_index_unit_divides_productcoefficients))) -> exists pfc_value_unit_divides_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonalentry. ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonalentry + S (pfc_value_unit_divides_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_divides_productcoefficientscoefficient)) /\ exists ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonalentry. pfc_terms_code_unit_divides_productcoefficientscoefficient = ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_divides_productcoefficientscoefficient) + (pfc_value_unit_divides_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm. (((pfc_index_unit_divides_productcoefficientscoefficientdiagonal)+pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm=(pfc_index_unit_divides_productcoefficients)) /\ ((((((exists pfa_gap_unit_divides_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_unit_divides_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal) = (Q)) /\ ((((exists ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) * qc) + (pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_divides_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_unit_divides_productcoefficientscoefficientdiagonaltermleftoutside+(Q)=(pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_divides_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_unit_divides_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_divides_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_unit_divides_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_unit_divides_productcoefficientscoefficientdiagonal)=pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm*pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_divides_productcoefficientscoefficientsum fs_v_pfc_unit_divides_productcoefficientscoefficientsum. ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_start. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_start. fs_u_pfc_unit_divides_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_unit_divides_productcoefficientscoefficient) = S ((S (S (pfc_index_unit_divides_productcoefficients))) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_unit_divides_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_unit_divides_productcoefficients))) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum) + (pfc_natural_sum_unit_divides_productcoefficientscoefficient))) /\ forall fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps = S (pfc_index_unit_divides_productcoefficients)) -> exists fs_a_pfc_unit_divides_productcoefficientscoefficientsum_body_steps fs_r_pfc_unit_divides_productcoefficientscoefficientsum_body_steps fs_s_pfc_unit_divides_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_unit_divides_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_divides_productcoefficientscoefficient)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_unit_divides_productcoefficientscoefficient = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_divides_productcoefficientscoefficient) + (fs_a_pfc_unit_divides_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_unit_divides_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_unit_divides_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum) + (fs_r_pfc_unit_divides_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_unit_divides_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_unit_divides_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum) + (fs_s_pfc_unit_divides_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_unit_divides_productcoefficientscoefficientsum_body_steps = fs_r_pfc_unit_divides_productcoefficientscoefficientsum_body_steps + fs_a_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_unit_divides_productcoefficientscoefficientresiduebound. pfa_gap_unit_divides_productcoefficientscoefficientresiduebound + S (pfc_value_unit_divides_productcoefficients) = (p)) /\ ((exists pfa_offset_left_unit_divides_productcoefficientscoefficientresiduecongruence pfa_offset_right_unit_divides_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_unit_divides_productcoefficientscoefficient) + (p) * pfa_offset_left_unit_divides_productcoefficientscoefficientresiduecongruence = (pfc_value_unit_divides_productcoefficients) + (p) * pfa_offset_right_unit_divides_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_unit_divides_equivalent pfrep_left_unit_divides_equivalent pfrep_right_unit_divides_equivalent. ((exists pfrep_position_unit_divides_equivalentfirst. ((pfrep_position_unit_divides_equivalentfirst+S (pfrep_power_unit_divides_equivalent)=(P)) /\ ((((exists ff_h_pfp_unit_divides_equivalentfirstentry. ff_h_pfp_unit_divides_equivalentfirstentry + S (pfrep_left_unit_divides_equivalent) = S ((S (pfrep_position_unit_divides_equivalentfirst)) * pc)) /\ exists ff_q_pfp_unit_divides_equivalentfirstentry. pb = ff_q_pfp_unit_divides_equivalentfirstentry * S ((S (pfrep_position_unit_divides_equivalentfirst)) * pc) + (pfrep_left_unit_divides_equivalent)))))) \/ (((exists pfrep_gap_unit_divides_equivalentfirstoutside. pfrep_gap_unit_divides_equivalentfirstoutside+(P)=(pfrep_power_unit_divides_equivalent)) /\ (((pfrep_left_unit_divides_equivalent)=0))))) -> ((exists pfrep_position_unit_divides_equivalentsecond. ((pfrep_position_unit_divides_equivalentsecond+S (pfrep_power_unit_divides_equivalent)=(L)) /\ ((((exists ff_h_pfp_unit_divides_equivalentsecondentry. ff_h_pfp_unit_divides_equivalentsecondentry + S (pfrep_right_unit_divides_equivalent) = S ((S (pfrep_position_unit_divides_equivalentsecond)) * ac)) /\ exists ff_q_pfp_unit_divides_equivalentsecondentry. ab = ff_q_pfp_unit_divides_equivalentsecondentry * S ((S (pfrep_position_unit_divides_equivalentsecond)) * ac) + (pfrep_right_unit_divides_equivalent)))))) \/ (((exists pfrep_gap_unit_divides_equivalentsecondoutside. pfrep_gap_unit_divides_equivalentsecondoutside+(L)=(pfrep_power_unit_divides_equivalent)) /\ (((pfrep_right_unit_divides_equivalent)=0))))) -> pfrep_left_unit_divides_equivalent=pfrep_right_unit_divides_equivalent)))))))

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 · 5 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 (2)
prime field polynomial convolution left unit existsprime field polynomial right divides from product
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro hp
  6. L6
    intro hA
02Establish huL7–14

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

  1. L7
    have hu : ∃ ub. ∃ uc. ∃ cb. ∃ cc. BetaPrefixInto(ub,uc,1,p) ∧ (BetaAt(ub,uc,0,1) ∧ (FpPolyProduct(p,ub,uc,1,ab,ac,L,cb,cc,L) ∧ PolynomialEquivalent(cb,cc,L,ab,ac,L)))Definitions: BetaPrefixInto(ub,uc,1,p)BetaAt(ub,uc,0,1)FpPolyProduct(p,ub,uc,1,ab,ac,L,cb,cc,L)PolynomialEquivalent(cb,cc,L,ab,ac,L)Original native command in the exact edition
  2. L8
    specialize prime_field_polynomial_convolution_left_unit_exists (p)
  3. L9
    specialize prime_field_polynomial_convolution_left_unit_exists (ab)
  4. L10
    specialize prime_field_polynomial_convolution_left_unit_exists (ac)
  5. L11
    specialize prime_field_polynomial_convolution_left_unit_exists (L)
  6. L12
    apply prime_field_polynomial_convolution_left_unit_exists
  7. L13
    exact hp
  8. L14
    exact hA
03Separate the logical casesL15–21

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

  1. L15
    cases hu
  2. L16
    cases hu_witness
  3. L17
    cases hu_witness_witness
  4. L18
    cases hu_witness_witness_witness
  5. L19
    cases hu_witness_witness_witness_witness
  6. L20
    cases hu_witness_witness_witness_witness_right
  7. L21
    cases hu_witness_witness_witness_witness_right_right
04Use earlier factsL22–31

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

  1. L22
    specialize prime_field_polynomial_right_divides_from_product (p)
  2. L23
    specialize prime_field_polynomial_right_divides_from_product (ab)
  3. L24
    specialize prime_field_polynomial_right_divides_from_product (ac)
  4. L25
    specialize prime_field_polynomial_right_divides_from_product (L)
  5. L26
    specialize prime_field_polynomial_right_divides_from_product (ab)
  6. L27
    specialize prime_field_polynomial_right_divides_from_product (ac)
  7. L28
    specialize prime_field_polynomial_right_divides_from_product (L)
  8. L29
    specialize prime_field_polynomial_right_divides_from_product (x)
  9. L30
    specialize prime_field_polynomial_right_divides_from_product (x1)
  10. L31
    specialize prime_field_polynomial_right_divides_from_product (1)
05Use earlier factsL32–38

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

  1. L32
    specialize prime_field_polynomial_right_divides_from_product (x2)
  2. L33
    specialize prime_field_polynomial_right_divides_from_product (x3)
  3. L34
    specialize prime_field_polynomial_right_divides_from_product (L)
  4. L35
    apply prime_field_polynomial_right_divides_from_product
  5. L36
    exact hA
  6. L37
    exact hu_witness_witness_witness_witness_right_right_left
  7. L38
    exact hu_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro hp
  6. 0006intro hA
  7. 0007have hu : ∃ ub. ∃ uc. ∃ cb. ∃ cc. BetaPrefixInto(ub,uc,1,p) ∧ (BetaAt(ub,uc,0,1) ∧ (FpPolyProduct(p,ub,uc,1,ab,ac,L,cb,cc,L) ∧ PolynomialEquivalent(cb,cc,L,ab,ac,L)))
  8. 0008specialize prime_field_polynomial_convolution_left_unit_exists (p)
  9. 0009specialize prime_field_polynomial_convolution_left_unit_exists (ab)
  10. 0010specialize prime_field_polynomial_convolution_left_unit_exists (ac)
  11. 0011specialize prime_field_polynomial_convolution_left_unit_exists (L)
  12. 0012apply prime_field_polynomial_convolution_left_unit_exists
  13. 0013exact hp
  14. 0014exact hA
  15. 0015cases hu
  16. 0016cases hu_witness
  17. 0017cases hu_witness_witness
  18. 0018cases hu_witness_witness_witness
  19. 0019cases hu_witness_witness_witness_witness
  20. 0020cases hu_witness_witness_witness_witness_right
  21. 0021cases hu_witness_witness_witness_witness_right_right
  22. 0022specialize prime_field_polynomial_right_divides_from_product (p)
  23. 0023specialize prime_field_polynomial_right_divides_from_product (ab)
  24. 0024specialize prime_field_polynomial_right_divides_from_product (ac)
  25. 0025specialize prime_field_polynomial_right_divides_from_product (L)
  26. 0026specialize prime_field_polynomial_right_divides_from_product (ab)
  27. 0027specialize prime_field_polynomial_right_divides_from_product (ac)
  28. 0028specialize prime_field_polynomial_right_divides_from_product (L)
  29. 0029specialize prime_field_polynomial_right_divides_from_product (x)
  30. 0030specialize prime_field_polynomial_right_divides_from_product (x1)
  31. 0031specialize prime_field_polynomial_right_divides_from_product (1)
  32. 0032specialize prime_field_polynomial_right_divides_from_product (x2)
  33. 0033specialize prime_field_polynomial_right_divides_from_product (x3)
  34. 0034specialize prime_field_polynomial_right_divides_from_product (L)
  35. 0035apply prime_field_polynomial_right_divides_from_product
  36. 0036exact hA
  37. 0037exact hu_witness_witness_witness_witness_right_right_left
  38. 0038exact hu_witness_witness_witness_witness_right_right_right