PG0057

prime_field_polynomial_normalized_right_associate_exists

Construct a zero-or-monic right associate of every canonical polynomial, first trimming its actual leading zeros and then normalizing only a nonempty trim. Both divisibility directions have real product witnesses and are transported to the original representation. Empty and all-zero encodings need no degree or inverse of zero.

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) → ∃ x. ∃ y. ∃ z. FpPolynomialZeroOrMonic(p,x,y,z) ∧ (FpPolynomialRightDivides(p,ab,ac,L,x,y,z) ∧ FpPolynomialRightDivides(p,x,y,z,ab,ac,L))

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 2FpRepresentedDegree(p,b,c,L,d) · 1FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1FpMonicNormalization(p,k,ab,ac,bb,bc,L) · 1PolynomialEquivalent(b,c,L,d,e,M) · 1FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 4FpPolynomialZeroOrMonic(p,gb,gc,G) · 1Prime(p) · 1

Actual proof prerequisites

prime_nonzero · checked external prerequisiteprime_field_polynomial_trim_exists · checked external prerequisiteprime_field_polynomial_trim_output_coefficients · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_trim_equivalent · checked external prerequisiteeq_decidable · checked external prerequisiteprime_field_polynomial_right_divides_emptyprime_field_polynomial_right_divides_equivalent_targetprime_field_polynomial_trim_nonempty_degree_exists · checked external prerequisiteprime_field_polynomial_monic_normalization_exists · checked external prerequisiteprime_field_polynomial_monic_normalization_right_associatesprime_field_polynomial_monic_normalization_monic · checked external prerequisiteprime_field_polynomial_right_divides_equivalent_divisor
Original expanded first-order statement 
forall p ab ac L. (~((p) = 1) /\ forall pfa_factor_left_normalized_associate_prime pfa_factor_right_normalized_associate_prime. (p) = pfa_factor_left_normalized_associate_prime * pfa_factor_right_normalized_associate_prime -> pfa_factor_left_normalized_associate_prime = 1 \/ pfa_factor_right_normalized_associate_prime = 1) -> (forall fom_index_pfp_normalized_associate_input. (exists fom_gap_pfp_normalized_associate_input_index_bound. fom_gap_pfp_normalized_associate_input_index_bound + S (fom_index_pfp_normalized_associate_input) = L) -> exists fom_value_pfp_normalized_associate_input. ((((exists fom_beta_height_pfp_normalized_associate_input_entry. fom_beta_height_pfp_normalized_associate_input_entry + S (fom_value_pfp_normalized_associate_input) = S ((S (fom_index_pfp_normalized_associate_input)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_associate_input_entry. ab = fom_beta_quotient_pfp_normalized_associate_input_entry * S ((S (fom_index_pfp_normalized_associate_input)) * ac) + (fom_value_pfp_normalized_associate_input))) /\ (exists fom_gap_pfp_normalized_associate_input_value_bound. fom_gap_pfp_normalized_associate_input_value_bound + S (fom_value_pfp_normalized_associate_input) = p))) -> (exists hb hc H. ((H=0 \/ (((~((H) = 0)) /\ (((forall fom_index_pfp_normalized_associate_result_moniccoefficients. (exists fom_gap_pfp_normalized_associate_result_moniccoefficients_index_bound. fom_gap_pfp_normalized_associate_result_moniccoefficients_index_bound + S (fom_index_pfp_normalized_associate_result_moniccoefficients) = H) -> exists fom_value_pfp_normalized_associate_result_moniccoefficients. ((((exists fom_beta_height_pfp_normalized_associate_result_moniccoefficients_entry. fom_beta_height_pfp_normalized_associate_result_moniccoefficients_entry + S (fom_value_pfp_normalized_associate_result_moniccoefficients) = S ((S (fom_index_pfp_normalized_associate_result_moniccoefficients)) * hc)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_moniccoefficients_entry. hb = fom_beta_quotient_pfp_normalized_associate_result_moniccoefficients_entry * S ((S (fom_index_pfp_normalized_associate_result_moniccoefficients)) * hc) + (fom_value_pfp_normalized_associate_result_moniccoefficients))) /\ (exists fom_gap_pfp_normalized_associate_result_moniccoefficients_value_bound. fom_gap_pfp_normalized_associate_result_moniccoefficients_value_bound + S (fom_value_pfp_normalized_associate_result_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normalized_associate_result_monicleading. ff_h_pfp_normalized_associate_result_monicleading + S (1) = S ((S (0)) * hc)) /\ exists ff_q_pfp_normalized_associate_result_monicleading. hb = ff_q_pfp_normalized_associate_result_monicleading * S ((S (0)) * hc) + (1))))))))) /\ (((((forall fom_index_pfp_normalized_associate_result_forward_canonical. (exists fom_gap_pfp_normalized_associate_result_forward_canonical_index_bound. fom_gap_pfp_normalized_associate_result_forward_canonical_index_bound + S (fom_index_pfp_normalized_associate_result_forward_canonical) = H) -> exists fom_value_pfp_normalized_associate_result_forward_canonical. ((((exists fom_beta_height_pfp_normalized_associate_result_forward_canonical_entry. fom_beta_height_pfp_normalized_associate_result_forward_canonical_entry + S (fom_value_pfp_normalized_associate_result_forward_canonical) = S ((S (fom_index_pfp_normalized_associate_result_forward_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_forward_canonical_entry. hb = fom_beta_quotient_pfp_normalized_associate_result_forward_canonical_entry * S ((S (fom_index_pfp_normalized_associate_result_forward_canonical)) * hc) + (fom_value_pfp_normalized_associate_result_forward_canonical))) /\ (exists fom_gap_pfp_normalized_associate_result_forward_canonical_value_bound. fom_gap_pfp_normalized_associate_result_forward_canonical_value_bound + S (fom_value_pfp_normalized_associate_result_forward_canonical) = p))) /\ ((exists pfen_qb_normalized_associate_result_forward pfen_qc_normalized_associate_result_forward pfen_qlen_normalized_associate_result_forward pfen_pb_normalized_associate_result_forward pfen_pc_normalized_associate_result_forward pfen_plen_normalized_associate_result_forward. ((((forall fom_index_pfp_normalized_associate_result_forward_productleft. (exists fom_gap_pfp_normalized_associate_result_forward_productleft_index_bound. fom_gap_pfp_normalized_associate_result_forward_productleft_index_bound + S (fom_index_pfp_normalized_associate_result_forward_productleft) = pfen_qlen_normalized_associate_result_forward) -> exists fom_value_pfp_normalized_associate_result_forward_productleft. ((((exists fom_beta_height_pfp_normalized_associate_result_forward_productleft_entry. fom_beta_height_pfp_normalized_associate_result_forward_productleft_entry + S (fom_value_pfp_normalized_associate_result_forward_productleft) = S ((S (fom_index_pfp_normalized_associate_result_forward_productleft)) * pfen_qc_normalized_associate_result_forward)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_forward_productleft_entry. pfen_qb_normalized_associate_result_forward = fom_beta_quotient_pfp_normalized_associate_result_forward_productleft_entry * S ((S (fom_index_pfp_normalized_associate_result_forward_productleft)) * pfen_qc_normalized_associate_result_forward) + (fom_value_pfp_normalized_associate_result_forward_productleft))) /\ (exists fom_gap_pfp_normalized_associate_result_forward_productleft_value_bound. fom_gap_pfp_normalized_associate_result_forward_productleft_value_bound + S (fom_value_pfp_normalized_associate_result_forward_productleft) = p))) /\ (((forall fom_index_pfp_normalized_associate_result_forward_productright. (exists fom_gap_pfp_normalized_associate_result_forward_productright_index_bound. fom_gap_pfp_normalized_associate_result_forward_productright_index_bound + S (fom_index_pfp_normalized_associate_result_forward_productright) = L) -> exists fom_value_pfp_normalized_associate_result_forward_productright. ((((exists fom_beta_height_pfp_normalized_associate_result_forward_productright_entry. fom_beta_height_pfp_normalized_associate_result_forward_productright_entry + S (fom_value_pfp_normalized_associate_result_forward_productright) = S ((S (fom_index_pfp_normalized_associate_result_forward_productright)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_forward_productright_entry. ab = fom_beta_quotient_pfp_normalized_associate_result_forward_productright_entry * S ((S (fom_index_pfp_normalized_associate_result_forward_productright)) * ac) + (fom_value_pfp_normalized_associate_result_forward_productright))) /\ (exists fom_gap_pfp_normalized_associate_result_forward_productright_value_bound. fom_gap_pfp_normalized_associate_result_forward_productright_value_bound + S (fom_value_pfp_normalized_associate_result_forward_productright) = p))) /\ (((((((pfen_qlen_normalized_associate_result_forward)=0 \/ (L)=0) /\ (((pfen_plen_normalized_associate_result_forward)=0)))) \/ (((~((pfen_qlen_normalized_associate_result_forward)=0)) /\ (((~((L)=0)) /\ (((pfen_qlen_normalized_associate_result_forward)+(L)=S (pfen_plen_normalized_associate_result_forward)))))))) /\ ((forall pfc_index_normalized_associate_result_forward_productcoefficients. (exists pfa_gap_normalized_associate_result_forward_productcoefficientsbound. pfa_gap_normalized_associate_result_forward_productcoefficientsbound + S (pfc_index_normalized_associate_result_forward_productcoefficients) = (pfen_plen_normalized_associate_result_forward)) -> exists pfc_value_normalized_associate_result_forward_productcoefficients. ((((exists ff_h_pfp_normalized_associate_result_forward_productcoefficientsentry. ff_h_pfp_normalized_associate_result_forward_productcoefficientsentry + S (pfc_value_normalized_associate_result_forward_productcoefficients) = S ((S (pfc_index_normalized_associate_result_forward_productcoefficients)) * pfen_pc_normalized_associate_result_forward)) /\ exists ff_q_pfp_normalized_associate_result_forward_productcoefficientsentry. pfen_pb_normalized_associate_result_forward = ff_q_pfp_normalized_associate_result_forward_productcoefficientsentry * S ((S (pfc_index_normalized_associate_result_forward_productcoefficients)) * pfen_pc_normalized_associate_result_forward) + (pfc_value_normalized_associate_result_forward_productcoefficients))) /\ ((exists pfc_terms_code_normalized_associate_result_forward_productcoefficientscoefficient pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient pfc_natural_sum_normalized_associate_result_forward_productcoefficientscoefficient. ((forall pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_associate_result_forward_productcoefficients))) -> exists pfc_value_normalized_associate_result_forward_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_associate_result_forward_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_associate_result_forward_productcoefficientscoefficient = ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient) + (pfc_value_normalized_associate_result_forward_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_associate_result_forward_productcoefficients)) /\ ((((((exists pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal) = (pfen_qlen_normalized_associate_result_forward)) /\ ((((exists ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalized_associate_result_forward)) /\ exists ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftentry. pfen_qb_normalized_associate_result_forward = ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalized_associate_result_forward) + (pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftoutside+(pfen_qlen_normalized_associate_result_forward)=(pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)=pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_associate_result_forward_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_associate_result_forward_productcoefficients))) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_associate_result_forward_productcoefficients))) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_associate_result_forward_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_associate_result_forward_productcoefficients)) -> exists fs_a_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_associate_result_forward_productcoefficientscoefficient = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient) + (fs_a_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientresiduebound. pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_associate_result_forward_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_associate_result_forward_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_associate_result_forward_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_associate_result_forward_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_associate_result_forward_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_associate_result_forward_productcoefficients) + (p) * pfa_offset_right_normalized_associate_result_forward_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_associate_result_forward_target pfrep_left_normalized_associate_result_forward_target pfrep_right_normalized_associate_result_forward_target. ((exists pfrep_position_normalized_associate_result_forward_targetfirst. ((pfrep_position_normalized_associate_result_forward_targetfirst+S (pfrep_power_normalized_associate_result_forward_target)=(pfen_plen_normalized_associate_result_forward)) /\ ((((exists ff_h_pfp_normalized_associate_result_forward_targetfirstentry. ff_h_pfp_normalized_associate_result_forward_targetfirstentry + S (pfrep_left_normalized_associate_result_forward_target) = S ((S (pfrep_position_normalized_associate_result_forward_targetfirst)) * pfen_pc_normalized_associate_result_forward)) /\ exists ff_q_pfp_normalized_associate_result_forward_targetfirstentry. pfen_pb_normalized_associate_result_forward = ff_q_pfp_normalized_associate_result_forward_targetfirstentry * S ((S (pfrep_position_normalized_associate_result_forward_targetfirst)) * pfen_pc_normalized_associate_result_forward) + (pfrep_left_normalized_associate_result_forward_target)))))) \/ (((exists pfrep_gap_normalized_associate_result_forward_targetfirstoutside. pfrep_gap_normalized_associate_result_forward_targetfirstoutside+(pfen_plen_normalized_associate_result_forward)=(pfrep_power_normalized_associate_result_forward_target)) /\ (((pfrep_left_normalized_associate_result_forward_target)=0))))) -> ((exists pfrep_position_normalized_associate_result_forward_targetsecond. ((pfrep_position_normalized_associate_result_forward_targetsecond+S (pfrep_power_normalized_associate_result_forward_target)=(H)) /\ ((((exists ff_h_pfp_normalized_associate_result_forward_targetsecondentry. ff_h_pfp_normalized_associate_result_forward_targetsecondentry + S (pfrep_right_normalized_associate_result_forward_target) = S ((S (pfrep_position_normalized_associate_result_forward_targetsecond)) * hc)) /\ exists ff_q_pfp_normalized_associate_result_forward_targetsecondentry. hb = ff_q_pfp_normalized_associate_result_forward_targetsecondentry * S ((S (pfrep_position_normalized_associate_result_forward_targetsecond)) * hc) + (pfrep_right_normalized_associate_result_forward_target)))))) \/ (((exists pfrep_gap_normalized_associate_result_forward_targetsecondoutside. pfrep_gap_normalized_associate_result_forward_targetsecondoutside+(H)=(pfrep_power_normalized_associate_result_forward_target)) /\ (((pfrep_right_normalized_associate_result_forward_target)=0))))) -> pfrep_left_normalized_associate_result_forward_target=pfrep_right_normalized_associate_result_forward_target))))))) /\ ((((forall fom_index_pfp_normalized_associate_result_backward_canonical. (exists fom_gap_pfp_normalized_associate_result_backward_canonical_index_bound. fom_gap_pfp_normalized_associate_result_backward_canonical_index_bound + S (fom_index_pfp_normalized_associate_result_backward_canonical) = L) -> exists fom_value_pfp_normalized_associate_result_backward_canonical. ((((exists fom_beta_height_pfp_normalized_associate_result_backward_canonical_entry. fom_beta_height_pfp_normalized_associate_result_backward_canonical_entry + S (fom_value_pfp_normalized_associate_result_backward_canonical) = S ((S (fom_index_pfp_normalized_associate_result_backward_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_backward_canonical_entry. ab = fom_beta_quotient_pfp_normalized_associate_result_backward_canonical_entry * S ((S (fom_index_pfp_normalized_associate_result_backward_canonical)) * ac) + (fom_value_pfp_normalized_associate_result_backward_canonical))) /\ (exists fom_gap_pfp_normalized_associate_result_backward_canonical_value_bound. fom_gap_pfp_normalized_associate_result_backward_canonical_value_bound + S (fom_value_pfp_normalized_associate_result_backward_canonical) = p))) /\ ((exists pfen_qb_normalized_associate_result_backward pfen_qc_normalized_associate_result_backward pfen_qlen_normalized_associate_result_backward pfen_pb_normalized_associate_result_backward pfen_pc_normalized_associate_result_backward pfen_plen_normalized_associate_result_backward. ((((forall fom_index_pfp_normalized_associate_result_backward_productleft. (exists fom_gap_pfp_normalized_associate_result_backward_productleft_index_bound. fom_gap_pfp_normalized_associate_result_backward_productleft_index_bound + S (fom_index_pfp_normalized_associate_result_backward_productleft) = pfen_qlen_normalized_associate_result_backward) -> exists fom_value_pfp_normalized_associate_result_backward_productleft. ((((exists fom_beta_height_pfp_normalized_associate_result_backward_productleft_entry. fom_beta_height_pfp_normalized_associate_result_backward_productleft_entry + S (fom_value_pfp_normalized_associate_result_backward_productleft) = S ((S (fom_index_pfp_normalized_associate_result_backward_productleft)) * pfen_qc_normalized_associate_result_backward)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_backward_productleft_entry. pfen_qb_normalized_associate_result_backward = fom_beta_quotient_pfp_normalized_associate_result_backward_productleft_entry * S ((S (fom_index_pfp_normalized_associate_result_backward_productleft)) * pfen_qc_normalized_associate_result_backward) + (fom_value_pfp_normalized_associate_result_backward_productleft))) /\ (exists fom_gap_pfp_normalized_associate_result_backward_productleft_value_bound. fom_gap_pfp_normalized_associate_result_backward_productleft_value_bound + S (fom_value_pfp_normalized_associate_result_backward_productleft) = p))) /\ (((forall fom_index_pfp_normalized_associate_result_backward_productright. (exists fom_gap_pfp_normalized_associate_result_backward_productright_index_bound. fom_gap_pfp_normalized_associate_result_backward_productright_index_bound + S (fom_index_pfp_normalized_associate_result_backward_productright) = H) -> exists fom_value_pfp_normalized_associate_result_backward_productright. ((((exists fom_beta_height_pfp_normalized_associate_result_backward_productright_entry. fom_beta_height_pfp_normalized_associate_result_backward_productright_entry + S (fom_value_pfp_normalized_associate_result_backward_productright) = S ((S (fom_index_pfp_normalized_associate_result_backward_productright)) * hc)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_backward_productright_entry. hb = fom_beta_quotient_pfp_normalized_associate_result_backward_productright_entry * S ((S (fom_index_pfp_normalized_associate_result_backward_productright)) * hc) + (fom_value_pfp_normalized_associate_result_backward_productright))) /\ (exists fom_gap_pfp_normalized_associate_result_backward_productright_value_bound. fom_gap_pfp_normalized_associate_result_backward_productright_value_bound + S (fom_value_pfp_normalized_associate_result_backward_productright) = p))) /\ (((((((pfen_qlen_normalized_associate_result_backward)=0 \/ (H)=0) /\ (((pfen_plen_normalized_associate_result_backward)=0)))) \/ (((~((pfen_qlen_normalized_associate_result_backward)=0)) /\ (((~((H)=0)) /\ (((pfen_qlen_normalized_associate_result_backward)+(H)=S (pfen_plen_normalized_associate_result_backward)))))))) /\ ((forall pfc_index_normalized_associate_result_backward_productcoefficients. (exists pfa_gap_normalized_associate_result_backward_productcoefficientsbound. pfa_gap_normalized_associate_result_backward_productcoefficientsbound + S (pfc_index_normalized_associate_result_backward_productcoefficients) = (pfen_plen_normalized_associate_result_backward)) -> exists pfc_value_normalized_associate_result_backward_productcoefficients. ((((exists ff_h_pfp_normalized_associate_result_backward_productcoefficientsentry. ff_h_pfp_normalized_associate_result_backward_productcoefficientsentry + S (pfc_value_normalized_associate_result_backward_productcoefficients) = S ((S (pfc_index_normalized_associate_result_backward_productcoefficients)) * pfen_pc_normalized_associate_result_backward)) /\ exists ff_q_pfp_normalized_associate_result_backward_productcoefficientsentry. pfen_pb_normalized_associate_result_backward = ff_q_pfp_normalized_associate_result_backward_productcoefficientsentry * S ((S (pfc_index_normalized_associate_result_backward_productcoefficients)) * pfen_pc_normalized_associate_result_backward) + (pfc_value_normalized_associate_result_backward_productcoefficients))) /\ ((exists pfc_terms_code_normalized_associate_result_backward_productcoefficientscoefficient pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient pfc_natural_sum_normalized_associate_result_backward_productcoefficientscoefficient. ((forall pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_associate_result_backward_productcoefficients))) -> exists pfc_value_normalized_associate_result_backward_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_associate_result_backward_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_associate_result_backward_productcoefficientscoefficient = ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient) + (pfc_value_normalized_associate_result_backward_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_associate_result_backward_productcoefficients)) /\ ((((((exists pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal) = (pfen_qlen_normalized_associate_result_backward)) /\ ((((exists ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalized_associate_result_backward)) /\ exists ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftentry. pfen_qb_normalized_associate_result_backward = ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalized_associate_result_backward) + (pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftoutside+(pfen_qlen_normalized_associate_result_backward)=(pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)=pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_associate_result_backward_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_associate_result_backward_productcoefficients))) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_associate_result_backward_productcoefficients))) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_associate_result_backward_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_associate_result_backward_productcoefficients)) -> exists fs_a_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_associate_result_backward_productcoefficientscoefficient = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient) + (fs_a_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientresiduebound. pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_associate_result_backward_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_associate_result_backward_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_associate_result_backward_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_associate_result_backward_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_associate_result_backward_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_associate_result_backward_productcoefficients) + (p) * pfa_offset_right_normalized_associate_result_backward_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_associate_result_backward_target pfrep_left_normalized_associate_result_backward_target pfrep_right_normalized_associate_result_backward_target. ((exists pfrep_position_normalized_associate_result_backward_targetfirst. ((pfrep_position_normalized_associate_result_backward_targetfirst+S (pfrep_power_normalized_associate_result_backward_target)=(pfen_plen_normalized_associate_result_backward)) /\ ((((exists ff_h_pfp_normalized_associate_result_backward_targetfirstentry. ff_h_pfp_normalized_associate_result_backward_targetfirstentry + S (pfrep_left_normalized_associate_result_backward_target) = S ((S (pfrep_position_normalized_associate_result_backward_targetfirst)) * pfen_pc_normalized_associate_result_backward)) /\ exists ff_q_pfp_normalized_associate_result_backward_targetfirstentry. pfen_pb_normalized_associate_result_backward = ff_q_pfp_normalized_associate_result_backward_targetfirstentry * S ((S (pfrep_position_normalized_associate_result_backward_targetfirst)) * pfen_pc_normalized_associate_result_backward) + (pfrep_left_normalized_associate_result_backward_target)))))) \/ (((exists pfrep_gap_normalized_associate_result_backward_targetfirstoutside. pfrep_gap_normalized_associate_result_backward_targetfirstoutside+(pfen_plen_normalized_associate_result_backward)=(pfrep_power_normalized_associate_result_backward_target)) /\ (((pfrep_left_normalized_associate_result_backward_target)=0))))) -> ((exists pfrep_position_normalized_associate_result_backward_targetsecond. ((pfrep_position_normalized_associate_result_backward_targetsecond+S (pfrep_power_normalized_associate_result_backward_target)=(L)) /\ ((((exists ff_h_pfp_normalized_associate_result_backward_targetsecondentry. ff_h_pfp_normalized_associate_result_backward_targetsecondentry + S (pfrep_right_normalized_associate_result_backward_target) = S ((S (pfrep_position_normalized_associate_result_backward_targetsecond)) * ac)) /\ exists ff_q_pfp_normalized_associate_result_backward_targetsecondentry. ab = ff_q_pfp_normalized_associate_result_backward_targetsecondentry * S ((S (pfrep_position_normalized_associate_result_backward_targetsecond)) * ac) + (pfrep_right_normalized_associate_result_backward_target)))))) \/ (((exists pfrep_gap_normalized_associate_result_backward_targetsecondoutside. pfrep_gap_normalized_associate_result_backward_targetsecondoutside+(L)=(pfrep_power_normalized_associate_result_backward_target)) /\ (((pfrep_right_normalized_associate_result_backward_target)=0))))) -> pfrep_left_normalized_associate_result_backward_target=pfrep_right_normalized_associate_result_backward_target))))))))))))

Complete tactic proof in conservative notation

All 177 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

177 script commands · 33 reading checkpoints · 8 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 (4)
prime field polynomial right divides emptyprime field polynomial right divides equivalent targetprime field polynomial monic normalization right associatesprime field polynomial right divides equivalent divisor
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 hp0L7–12

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

  1. L7
    have hp0 : ~(p=0)
  2. L8
    intro hpzero
  3. L9
    specialize prime_nonzero (p)
  4. L10
    apply prime_nonzero
  5. L11
    exact hp
  6. L12
    exact hpzero
03Establish htrimL13–19

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

  1. L13
    have htrim : ∃ t. ∃ tb. ∃ tc. ∃ M. FpPolynomialTrim(p,ab,ac,L,t,tb,tc,M)Definitions: FpPolynomialTrim(p,ab,ac,L,t,tb,tc,M)Original native command in the exact edition
  2. L14
    specialize prime_field_polynomial_trim_exists (p)
  3. L15
    specialize prime_field_polynomial_trim_exists (ab)
  4. L16
    specialize prime_field_polynomial_trim_exists (ac)
  5. L17
    specialize prime_field_polynomial_trim_exists (L)
  6. L18
    apply prime_field_polynomial_trim_exists
  7. L19
    exact hA
04Separate the logical casesL20–23

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

  1. L20
    cases htrim
  2. L21
    cases htrim_witness
  3. L22
    cases htrim_witness_witness
  4. L23
    cases htrim_witness_witness_witness
05Establish hTL24–33

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

  1. L24
    have hT : BetaPrefixInto(x1,x2,x3,p)Definitions: BetaPrefixInto(x1,x2,x3,p)Original native command in the exact edition
  2. L25
    specialize prime_field_polynomial_trim_output_coefficients (p)
  3. L26
    specialize prime_field_polynomial_trim_output_coefficients (ab)
  4. L27
    specialize prime_field_polynomial_trim_output_coefficients (ac)
  5. L28
    specialize prime_field_polynomial_trim_output_coefficients (L)
  6. L29
    specialize prime_field_polynomial_trim_output_coefficients (x)
  7. L30
    specialize prime_field_polynomial_trim_output_coefficients (x1)
  8. L31
    specialize prime_field_polynomial_trim_output_coefficients (x2)
  9. L32
    specialize prime_field_polynomial_trim_output_coefficients (x3)
  10. L33
    apply prime_field_polynomial_trim_output_coefficients
06Use earlier factsL34–34

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

  1. L34
    exact htrim_witness_witness_witness_witness
07Establish hTAL35–44

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

  1. L35
    have hTA : PolynomialEquivalent(x1,x2,x3,ab,ac,L)Definitions: PolynomialEquivalent(x1,x2,x3,ab,ac,L)Original native command in the exact edition
  2. L36
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  3. L37
    specialize prime_field_polynomial_equivalent_symmetric (ac)
  4. L38
    specialize prime_field_polynomial_equivalent_symmetric (L)
  5. L39
    specialize prime_field_polynomial_equivalent_symmetric (x1)
  6. L40
    specialize prime_field_polynomial_equivalent_symmetric (x2)
  7. L41
    specialize prime_field_polynomial_equivalent_symmetric (x3)
  8. L42
    apply prime_field_polynomial_equivalent_symmetric
  9. L43
    specialize prime_field_polynomial_trim_equivalent (p)
  10. L44
    specialize prime_field_polynomial_trim_equivalent (ab)
08Use earlier factsL45–52

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

  1. L45
    specialize prime_field_polynomial_trim_equivalent (ac)
  2. L46
    specialize prime_field_polynomial_trim_equivalent (L)
  3. L47
    specialize prime_field_polynomial_trim_equivalent (x)
  4. L48
    specialize prime_field_polynomial_trim_equivalent (x1)
  5. L49
    specialize prime_field_polynomial_trim_equivalent (x2)
  6. L50
    specialize prime_field_polynomial_trim_equivalent (x3)
  7. L51
    apply prime_field_polynomial_trim_equivalent
  8. L52
    exact htrim_witness_witness_witness_witness
09Establish hcaseL53–56

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

  1. L53
    have hcase : x3=0 \/ ~(x3=0)
  2. L54
    specialize eq_decidable (x3)
  3. L55
    specialize eq_decidable (0)
  4. L56
    apply eq_decidable
10Separate the logical casesL57–57

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

  1. L57
    cases hcase
11Calculate and transport equalitiesL58–60

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

  1. L58
    rewrite hcase_left at hT
  2. L59
    rewrite hcase_left at hTA
  3. L60
    rewrite hcase_left at hTA
12Construct an explicit witnessL61–63

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

  1. L61
    exists x1
  2. L62
    exists x2
  3. L63
    exists 0
13Separate the logical casesL64–65

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

  1. L64
    split
  2. L65
    left
14Calculate and transport equalitiesL66–66

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

  1. L66
    refl
15Separate the logical casesL67–67

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

  1. L67
    split
16Use earlier factsL68–77

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

  1. L68
    specialize prime_field_polynomial_right_divides_empty (p)
  2. L69
    specialize prime_field_polynomial_right_divides_empty (ab)
  3. L70
    specialize prime_field_polynomial_right_divides_empty (ac)
  4. L71
    specialize prime_field_polynomial_right_divides_empty (L)
  5. L72
    specialize prime_field_polynomial_right_divides_empty (x1)
  6. L73
    specialize prime_field_polynomial_right_divides_empty (x2)
  7. L74
    apply prime_field_polynomial_right_divides_empty
  8. L75
    exact hA
  9. L76
    specialize prime_field_polynomial_right_divides_equivalent_target (p)
  10. L77
    specialize prime_field_polynomial_right_divides_equivalent_target (x1)
17Use earlier factsL78–87

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

  1. L78
    specialize prime_field_polynomial_right_divides_equivalent_target (x2)
  2. L79
    specialize prime_field_polynomial_right_divides_equivalent_target (0)
  3. L80
    specialize prime_field_polynomial_right_divides_equivalent_target (x1)
  4. L81
    specialize prime_field_polynomial_right_divides_equivalent_target (x2)
  5. L82
    specialize prime_field_polynomial_right_divides_equivalent_target (0)
  6. L83
    specialize prime_field_polynomial_right_divides_equivalent_target (ab)
  7. L84
    specialize prime_field_polynomial_right_divides_equivalent_target (ac)
  8. L85
    specialize prime_field_polynomial_right_divides_equivalent_target (L)
  9. L86
    apply prime_field_polynomial_right_divides_equivalent_target
  10. L87
    exact hA
18Use earlier factsL88–96

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

  1. L88
    specialize prime_field_polynomial_right_divides_empty (p)
  2. L89
    specialize prime_field_polynomial_right_divides_empty (x1)
  3. L90
    specialize prime_field_polynomial_right_divides_empty (x2)
  4. L91
    specialize prime_field_polynomial_right_divides_empty (0)
  5. L92
    specialize prime_field_polynomial_right_divides_empty (x1)
  6. L93
    specialize prime_field_polynomial_right_divides_empty (x2)
  7. L94
    apply prime_field_polynomial_right_divides_empty
  8. L95
    exact hT
  9. L96
    exact hTA
19Establish hdegreeL97–106

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

  1. L97
    have hdegree : ∃ d. FpRepresentedDegree(p,x1,x2,x3,d)Definitions: FpRepresentedDegree(p,x1,x2,x3,d)Original native command in the exact edition
  2. L98
    specialize prime_field_polynomial_trim_nonempty_degree_exists (p)
  3. L99
    specialize prime_field_polynomial_trim_nonempty_degree_exists (ab)
  4. L100
    specialize prime_field_polynomial_trim_nonempty_degree_exists (ac)
  5. L101
    specialize prime_field_polynomial_trim_nonempty_degree_exists (L)
  6. L102
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x)
  7. L103
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x1)
  8. L104
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x2)
  9. L105
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x3)
  10. L106
    apply prime_field_polynomial_trim_nonempty_degree_exists
20Use earlier factsL107–108

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

  1. L107
    exact htrim_witness_witness_witness_witness
  2. L108
    exact hcase_right
21Separate the logical casesL109–109

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

  1. L109
    cases hdegree
22Establish hnormalizationL110–118

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

  1. L110
    have hnormalization : ∃ k. ∃ hb. ∃ hc. FpMonicNormalization(p,k,x1,x2,hb,hc,x3)Definitions: FpMonicNormalization(p,k,x1,x2,hb,hc,x3)Original native command in the exact edition
  2. L111
    specialize prime_field_polynomial_monic_normalization_exists (p)
  3. L112
    specialize prime_field_polynomial_monic_normalization_exists (x1)
  4. L113
    specialize prime_field_polynomial_monic_normalization_exists (x2)
  5. L114
    specialize prime_field_polynomial_monic_normalization_exists (x3)
  6. L115
    specialize prime_field_polynomial_monic_normalization_exists (x4)
  7. L116
    apply prime_field_polynomial_monic_normalization_exists
  8. L117
    exact hp
  9. L118
    exact hdegree_witness
23Separate the logical casesL119–121

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

  1. L119
    cases hnormalization
  2. L120
    cases hnormalization_witness
  3. L121
    cases hnormalization_witness_witness
24Establish hassociatesL122–131

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial monic normalization right associates.

  1. L122
    have hassociates : FpPolynomialRightDivides(p,x1,x2,x3,x6,x7,x3) ∧ FpPolynomialRightDivides(p,x6,x7,x3,x1,x2,x3)Definitions: FpPolynomialRightDivides(p,x1,x2,x3,x6,x7,x3)FpPolynomialRightDivides(p,x6,x7,x3,x1,x2,x3)Original native command in the exact edition
  2. L123
    specialize prime_field_polynomial_monic_normalization_right_associates (p)
  3. L124
    specialize prime_field_polynomial_monic_normalization_right_associates (x5)
  4. L125
    specialize prime_field_polynomial_monic_normalization_right_associates (x1)
  5. L126
    specialize prime_field_polynomial_monic_normalization_right_associates (x2)
  6. L127
    specialize prime_field_polynomial_monic_normalization_right_associates (x6)
  7. L128
    specialize prime_field_polynomial_monic_normalization_right_associates (x7)
  8. L129
    specialize prime_field_polynomial_monic_normalization_right_associates (x3)
  9. L130
    apply prime_field_polynomial_monic_normalization_right_associates
  10. L131
    exact hp
25Use earlier factsL132–132

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

  1. L132
    exact hnormalization_witness_witness_witness
26Separate the logical casesL133–133

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

  1. L133
    cases hassociates
27Construct an explicit witnessL134–136

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

  1. L134
    exists x6
  2. L135
    exists x7
  3. L136
    exists x3
28Separate the logical casesL137–138

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

  1. L137
    split
  2. L138
    right
29Use earlier factsL139–147

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

  1. L139
    specialize prime_field_polynomial_monic_normalization_monic (p)
  2. L140
    specialize prime_field_polynomial_monic_normalization_monic (x5)
  3. L141
    specialize prime_field_polynomial_monic_normalization_monic (x1)
  4. L142
    specialize prime_field_polynomial_monic_normalization_monic (x2)
  5. L143
    specialize prime_field_polynomial_monic_normalization_monic (x6)
  6. L144
    specialize prime_field_polynomial_monic_normalization_monic (x7)
  7. L145
    specialize prime_field_polynomial_monic_normalization_monic (x3)
  8. L146
    apply prime_field_polynomial_monic_normalization_monic
  9. L147
    exact hnormalization_witness_witness_witness
30Separate the logical casesL148–148

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

  1. L148
    split
31Use earlier factsL149–158

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

  1. L149
    specialize prime_field_polynomial_right_divides_equivalent_divisor (p)
  2. L150
    specialize prime_field_polynomial_right_divides_equivalent_divisor (x1)
  3. L151
    specialize prime_field_polynomial_right_divides_equivalent_divisor (x2)
  4. L152
    specialize prime_field_polynomial_right_divides_equivalent_divisor (x3)
  5. L153
    specialize prime_field_polynomial_right_divides_equivalent_divisor (x6)
  6. L154
    specialize prime_field_polynomial_right_divides_equivalent_divisor (x7)
  7. L155
    specialize prime_field_polynomial_right_divides_equivalent_divisor (x3)
  8. L156
    specialize prime_field_polynomial_right_divides_equivalent_divisor (ab)
  9. L157
    specialize prime_field_polynomial_right_divides_equivalent_divisor (ac)
  10. L158
    specialize prime_field_polynomial_right_divides_equivalent_divisor (L)
32Use earlier factsL159–168

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

  1. L159
    apply prime_field_polynomial_right_divides_equivalent_divisor
  2. L160
    exact hp0
  3. L161
    exact hA
  4. L162
    exact hTA
  5. L163
    exact hassociates_left
  6. L164
    specialize prime_field_polynomial_right_divides_equivalent_target (p)
  7. L165
    specialize prime_field_polynomial_right_divides_equivalent_target (x6)
  8. L166
    specialize prime_field_polynomial_right_divides_equivalent_target (x7)
  9. L167
    specialize prime_field_polynomial_right_divides_equivalent_target (x3)
  10. L168
    specialize prime_field_polynomial_right_divides_equivalent_target (x1)
33Use earlier factsL169–177

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

  1. L169
    specialize prime_field_polynomial_right_divides_equivalent_target (x2)
  2. L170
    specialize prime_field_polynomial_right_divides_equivalent_target (x3)
  3. L171
    specialize prime_field_polynomial_right_divides_equivalent_target (ab)
  4. L172
    specialize prime_field_polynomial_right_divides_equivalent_target (ac)
  5. L173
    specialize prime_field_polynomial_right_divides_equivalent_target (L)
  6. L174
    apply prime_field_polynomial_right_divides_equivalent_target
  7. L175
    exact hA
  8. L176
    exact hassociates_right
  9. L177
    exact hTA

Library-wide reading audit

Original defined command ledger · 177 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro hp
  6. 0006intro hA
  7. 0007have hp0 : ~(p=0)
  8. 0008intro hpzero
  9. 0009specialize prime_nonzero (p)
  10. 0010apply prime_nonzero
  11. 0011exact hp
  12. 0012exact hpzero
  13. 0013have htrim : ∃ t. ∃ tb. ∃ tc. ∃ M. FpPolynomialTrim(p,ab,ac,L,t,tb,tc,M)
  14. 0014specialize prime_field_polynomial_trim_exists (p)
  15. 0015specialize prime_field_polynomial_trim_exists (ab)
  16. 0016specialize prime_field_polynomial_trim_exists (ac)
  17. 0017specialize prime_field_polynomial_trim_exists (L)
  18. 0018apply prime_field_polynomial_trim_exists
  19. 0019exact hA
  20. 0020cases htrim
  21. 0021cases htrim_witness
  22. 0022cases htrim_witness_witness
  23. 0023cases htrim_witness_witness_witness
  24. 0024have hT : BetaPrefixInto(x1,x2,x3,p)
  25. 0025specialize prime_field_polynomial_trim_output_coefficients (p)
  26. 0026specialize prime_field_polynomial_trim_output_coefficients (ab)
  27. 0027specialize prime_field_polynomial_trim_output_coefficients (ac)
  28. 0028specialize prime_field_polynomial_trim_output_coefficients (L)
  29. 0029specialize prime_field_polynomial_trim_output_coefficients (x)
  30. 0030specialize prime_field_polynomial_trim_output_coefficients (x1)
  31. 0031specialize prime_field_polynomial_trim_output_coefficients (x2)
  32. 0032specialize prime_field_polynomial_trim_output_coefficients (x3)
  33. 0033apply prime_field_polynomial_trim_output_coefficients
  34. 0034exact htrim_witness_witness_witness_witness
  35. 0035have hTA : PolynomialEquivalent(x1,x2,x3,ab,ac,L)
  36. 0036specialize prime_field_polynomial_equivalent_symmetric (ab)
  37. 0037specialize prime_field_polynomial_equivalent_symmetric (ac)
  38. 0038specialize prime_field_polynomial_equivalent_symmetric (L)
  39. 0039specialize prime_field_polynomial_equivalent_symmetric (x1)
  40. 0040specialize prime_field_polynomial_equivalent_symmetric (x2)
  41. 0041specialize prime_field_polynomial_equivalent_symmetric (x3)
  42. 0042apply prime_field_polynomial_equivalent_symmetric
  43. 0043specialize prime_field_polynomial_trim_equivalent (p)
  44. 0044specialize prime_field_polynomial_trim_equivalent (ab)
  45. 0045specialize prime_field_polynomial_trim_equivalent (ac)
  46. 0046specialize prime_field_polynomial_trim_equivalent (L)
  47. 0047specialize prime_field_polynomial_trim_equivalent (x)
  48. 0048specialize prime_field_polynomial_trim_equivalent (x1)
  49. 0049specialize prime_field_polynomial_trim_equivalent (x2)
  50. 0050specialize prime_field_polynomial_trim_equivalent (x3)
  51. 0051apply prime_field_polynomial_trim_equivalent
  52. 0052exact htrim_witness_witness_witness_witness
  53. 0053have hcase : x3=0 \/ ~(x3=0)
  54. 0054specialize eq_decidable (x3)
  55. 0055specialize eq_decidable (0)
  56. 0056apply eq_decidable
  57. 0057cases hcase
  58. 0058rewrite hcase_left at hT
  59. 0059rewrite hcase_left at hTA
  60. 0060rewrite hcase_left at hTA
  61. 0061exists x1
  62. 0062exists x2
  63. 0063exists 0
  64. 0064split
  65. 0065left
  66. 0066refl
  67. 0067split
  68. 0068specialize prime_field_polynomial_right_divides_empty (p)
  69. 0069specialize prime_field_polynomial_right_divides_empty (ab)
  70. 0070specialize prime_field_polynomial_right_divides_empty (ac)
  71. 0071specialize prime_field_polynomial_right_divides_empty (L)
  72. 0072specialize prime_field_polynomial_right_divides_empty (x1)
  73. 0073specialize prime_field_polynomial_right_divides_empty (x2)
  74. 0074apply prime_field_polynomial_right_divides_empty
  75. 0075exact hA
  76. 0076specialize prime_field_polynomial_right_divides_equivalent_target (p)
  77. 0077specialize prime_field_polynomial_right_divides_equivalent_target (x1)
  78. 0078specialize prime_field_polynomial_right_divides_equivalent_target (x2)
  79. 0079specialize prime_field_polynomial_right_divides_equivalent_target (0)
  80. 0080specialize prime_field_polynomial_right_divides_equivalent_target (x1)
  81. 0081specialize prime_field_polynomial_right_divides_equivalent_target (x2)
  82. 0082specialize prime_field_polynomial_right_divides_equivalent_target (0)
  83. 0083specialize prime_field_polynomial_right_divides_equivalent_target (ab)
  84. 0084specialize prime_field_polynomial_right_divides_equivalent_target (ac)
  85. 0085specialize prime_field_polynomial_right_divides_equivalent_target (L)
  86. 0086apply prime_field_polynomial_right_divides_equivalent_target
  87. 0087exact hA
  88. 0088specialize prime_field_polynomial_right_divides_empty (p)
  89. 0089specialize prime_field_polynomial_right_divides_empty (x1)
  90. 0090specialize prime_field_polynomial_right_divides_empty (x2)
  91. 0091specialize prime_field_polynomial_right_divides_empty (0)
  92. 0092specialize prime_field_polynomial_right_divides_empty (x1)
  93. 0093specialize prime_field_polynomial_right_divides_empty (x2)
  94. 0094apply prime_field_polynomial_right_divides_empty
  95. 0095exact hT
  96. 0096exact hTA
  97. 0097have hdegree : ∃ d. FpRepresentedDegree(p,x1,x2,x3,d)
  98. 0098specialize prime_field_polynomial_trim_nonempty_degree_exists (p)
  99. 0099specialize prime_field_polynomial_trim_nonempty_degree_exists (ab)
  100. 0100specialize prime_field_polynomial_trim_nonempty_degree_exists (ac)
  101. 0101specialize prime_field_polynomial_trim_nonempty_degree_exists (L)
  102. 0102specialize prime_field_polynomial_trim_nonempty_degree_exists (x)
  103. 0103specialize prime_field_polynomial_trim_nonempty_degree_exists (x1)
  104. 0104specialize prime_field_polynomial_trim_nonempty_degree_exists (x2)
  105. 0105specialize prime_field_polynomial_trim_nonempty_degree_exists (x3)
  106. 0106apply prime_field_polynomial_trim_nonempty_degree_exists
  107. 0107exact htrim_witness_witness_witness_witness
  108. 0108exact hcase_right
  109. 0109cases hdegree
  110. 0110have hnormalization : ∃ k. ∃ hb. ∃ hc. FpMonicNormalization(p,k,x1,x2,hb,hc,x3)
  111. 0111specialize prime_field_polynomial_monic_normalization_exists (p)
  112. 0112specialize prime_field_polynomial_monic_normalization_exists (x1)
  113. 0113specialize prime_field_polynomial_monic_normalization_exists (x2)
  114. 0114specialize prime_field_polynomial_monic_normalization_exists (x3)
  115. 0115specialize prime_field_polynomial_monic_normalization_exists (x4)
  116. 0116apply prime_field_polynomial_monic_normalization_exists
  117. 0117exact hp
  118. 0118exact hdegree_witness
  119. 0119cases hnormalization
  120. 0120cases hnormalization_witness
  121. 0121cases hnormalization_witness_witness
  122. 0122have hassociates : FpPolynomialRightDivides(p,x1,x2,x3,x6,x7,x3) ∧ FpPolynomialRightDivides(p,x6,x7,x3,x1,x2,x3)
  123. 0123specialize prime_field_polynomial_monic_normalization_right_associates (p)
  124. 0124specialize prime_field_polynomial_monic_normalization_right_associates (x5)
  125. 0125specialize prime_field_polynomial_monic_normalization_right_associates (x1)
  126. 0126specialize prime_field_polynomial_monic_normalization_right_associates (x2)
  127. 0127specialize prime_field_polynomial_monic_normalization_right_associates (x6)
  128. 0128specialize prime_field_polynomial_monic_normalization_right_associates (x7)
  129. 0129specialize prime_field_polynomial_monic_normalization_right_associates (x3)
  130. 0130apply prime_field_polynomial_monic_normalization_right_associates
  131. 0131exact hp
  132. 0132exact hnormalization_witness_witness_witness
  133. 0133cases hassociates
  134. 0134exists x6
  135. 0135exists x7
  136. 0136exists x3
  137. 0137split
  138. 0138right
  139. 0139specialize prime_field_polynomial_monic_normalization_monic (p)
  140. 0140specialize prime_field_polynomial_monic_normalization_monic (x5)
  141. 0141specialize prime_field_polynomial_monic_normalization_monic (x1)
  142. 0142specialize prime_field_polynomial_monic_normalization_monic (x2)
  143. 0143specialize prime_field_polynomial_monic_normalization_monic (x6)
  144. 0144specialize prime_field_polynomial_monic_normalization_monic (x7)
  145. 0145specialize prime_field_polynomial_monic_normalization_monic (x3)
  146. 0146apply prime_field_polynomial_monic_normalization_monic
  147. 0147exact hnormalization_witness_witness_witness
  148. 0148split
  149. 0149specialize prime_field_polynomial_right_divides_equivalent_divisor (p)
  150. 0150specialize prime_field_polynomial_right_divides_equivalent_divisor (x1)
  151. 0151specialize prime_field_polynomial_right_divides_equivalent_divisor (x2)
  152. 0152specialize prime_field_polynomial_right_divides_equivalent_divisor (x3)
  153. 0153specialize prime_field_polynomial_right_divides_equivalent_divisor (x6)
  154. 0154specialize prime_field_polynomial_right_divides_equivalent_divisor (x7)
  155. 0155specialize prime_field_polynomial_right_divides_equivalent_divisor (x3)
  156. 0156specialize prime_field_polynomial_right_divides_equivalent_divisor (ab)
  157. 0157specialize prime_field_polynomial_right_divides_equivalent_divisor (ac)
  158. 0158specialize prime_field_polynomial_right_divides_equivalent_divisor (L)
  159. 0159apply prime_field_polynomial_right_divides_equivalent_divisor
  160. 0160exact hp0
  161. 0161exact hA
  162. 0162exact hTA
  163. 0163exact hassociates_left
  164. 0164specialize prime_field_polynomial_right_divides_equivalent_target (p)
  165. 0165specialize prime_field_polynomial_right_divides_equivalent_target (x6)
  166. 0166specialize prime_field_polynomial_right_divides_equivalent_target (x7)
  167. 0167specialize prime_field_polynomial_right_divides_equivalent_target (x3)
  168. 0168specialize prime_field_polynomial_right_divides_equivalent_target (x1)
  169. 0169specialize prime_field_polynomial_right_divides_equivalent_target (x2)
  170. 0170specialize prime_field_polynomial_right_divides_equivalent_target (x3)
  171. 0171specialize prime_field_polynomial_right_divides_equivalent_target (ab)
  172. 0172specialize prime_field_polynomial_right_divides_equivalent_target (ac)
  173. 0173specialize prime_field_polynomial_right_divides_equivalent_target (L)
  174. 0174apply prime_field_polynomial_right_divides_equivalent_target
  175. 0175exact hA
  176. 0176exact hassociates_right
  177. 0177exact hTA