PG0073

prime_field_polynomial_monic_equal_degree_right_divides_equivalent

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

Equal-degree monic right divisibility has a genuinely constructed degree-zero quotient. Its head must be one, so divisor and target are formally equivalent.

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

Exact expanded first-order arithmetic statement

forall p db dc ab ac d. (~((p) = 1) /\ forall pfa_factor_left_monic_degree_prime pfa_factor_right_monic_degree_prime. (p) = pfa_factor_left_monic_degree_prime * pfa_factor_right_monic_degree_prime -> pfa_factor_left_monic_degree_prime = 1 \/ pfa_factor_right_monic_degree_prime = 1) -> (((~((S d) = 0)) /\ (((forall fom_index_pfp_monic_degree_Dcoefficients. (exists fom_gap_pfp_monic_degree_Dcoefficients_index_bound. fom_gap_pfp_monic_degree_Dcoefficients_index_bound + S (fom_index_pfp_monic_degree_Dcoefficients) = S d) -> exists fom_value_pfp_monic_degree_Dcoefficients. ((((exists fom_beta_height_pfp_monic_degree_Dcoefficients_entry. fom_beta_height_pfp_monic_degree_Dcoefficients_entry + S (fom_value_pfp_monic_degree_Dcoefficients) = S ((S (fom_index_pfp_monic_degree_Dcoefficients)) * dc)) /\ exists fom_beta_quotient_pfp_monic_degree_Dcoefficients_entry. db = fom_beta_quotient_pfp_monic_degree_Dcoefficients_entry * S ((S (fom_index_pfp_monic_degree_Dcoefficients)) * dc) + (fom_value_pfp_monic_degree_Dcoefficients))) /\ (exists fom_gap_pfp_monic_degree_Dcoefficients_value_bound. fom_gap_pfp_monic_degree_Dcoefficients_value_bound + S (fom_value_pfp_monic_degree_Dcoefficients) = p))) /\ ((((exists ff_h_pfp_monic_degree_Dleading. ff_h_pfp_monic_degree_Dleading + S (1) = S ((S (0)) * dc)) /\ exists ff_q_pfp_monic_degree_Dleading. db = ff_q_pfp_monic_degree_Dleading * S ((S (0)) * dc) + (1)))))))) -> (((~((S d) = 0)) /\ (((forall fom_index_pfp_monic_degree_Acoefficients. (exists fom_gap_pfp_monic_degree_Acoefficients_index_bound. fom_gap_pfp_monic_degree_Acoefficients_index_bound + S (fom_index_pfp_monic_degree_Acoefficients) = S d) -> exists fom_value_pfp_monic_degree_Acoefficients. ((((exists fom_beta_height_pfp_monic_degree_Acoefficients_entry. fom_beta_height_pfp_monic_degree_Acoefficients_entry + S (fom_value_pfp_monic_degree_Acoefficients) = S ((S (fom_index_pfp_monic_degree_Acoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_monic_degree_Acoefficients_entry. ab = fom_beta_quotient_pfp_monic_degree_Acoefficients_entry * S ((S (fom_index_pfp_monic_degree_Acoefficients)) * ac) + (fom_value_pfp_monic_degree_Acoefficients))) /\ (exists fom_gap_pfp_monic_degree_Acoefficients_value_bound. fom_gap_pfp_monic_degree_Acoefficients_value_bound + S (fom_value_pfp_monic_degree_Acoefficients) = p))) /\ ((((exists ff_h_pfp_monic_degree_Aleading. ff_h_pfp_monic_degree_Aleading + S (1) = S ((S (0)) * ac)) /\ exists ff_q_pfp_monic_degree_Aleading. ab = ff_q_pfp_monic_degree_Aleading * S ((S (0)) * ac) + (1)))))))) -> (((forall fom_index_pfp_monic_degree_RD_canonical. (exists fom_gap_pfp_monic_degree_RD_canonical_index_bound. fom_gap_pfp_monic_degree_RD_canonical_index_bound + S (fom_index_pfp_monic_degree_RD_canonical) = S d) -> exists fom_value_pfp_monic_degree_RD_canonical. ((((exists fom_beta_height_pfp_monic_degree_RD_canonical_entry. fom_beta_height_pfp_monic_degree_RD_canonical_entry + S (fom_value_pfp_monic_degree_RD_canonical) = S ((S (fom_index_pfp_monic_degree_RD_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_monic_degree_RD_canonical_entry. ab = fom_beta_quotient_pfp_monic_degree_RD_canonical_entry * S ((S (fom_index_pfp_monic_degree_RD_canonical)) * ac) + (fom_value_pfp_monic_degree_RD_canonical))) /\ (exists fom_gap_pfp_monic_degree_RD_canonical_value_bound. fom_gap_pfp_monic_degree_RD_canonical_value_bound + S (fom_value_pfp_monic_degree_RD_canonical) = p))) /\ ((exists pfgu_qb_monic_degree_RD pfgu_qc_monic_degree_RD pfgu_Q_monic_degree_RD pfgu_pb_monic_degree_RD pfgu_pc_monic_degree_RD pfgu_P_monic_degree_RD. ((((forall fom_index_pfp_monic_degree_RD_productleft. (exists fom_gap_pfp_monic_degree_RD_productleft_index_bound. fom_gap_pfp_monic_degree_RD_productleft_index_bound + S (fom_index_pfp_monic_degree_RD_productleft) = pfgu_Q_monic_degree_RD) -> exists fom_value_pfp_monic_degree_RD_productleft. ((((exists fom_beta_height_pfp_monic_degree_RD_productleft_entry. fom_beta_height_pfp_monic_degree_RD_productleft_entry + S (fom_value_pfp_monic_degree_RD_productleft) = S ((S (fom_index_pfp_monic_degree_RD_productleft)) * pfgu_qc_monic_degree_RD)) /\ exists fom_beta_quotient_pfp_monic_degree_RD_productleft_entry. pfgu_qb_monic_degree_RD = fom_beta_quotient_pfp_monic_degree_RD_productleft_entry * S ((S (fom_index_pfp_monic_degree_RD_productleft)) * pfgu_qc_monic_degree_RD) + (fom_value_pfp_monic_degree_RD_productleft))) /\ (exists fom_gap_pfp_monic_degree_RD_productleft_value_bound. fom_gap_pfp_monic_degree_RD_productleft_value_bound + S (fom_value_pfp_monic_degree_RD_productleft) = p))) /\ (((forall fom_index_pfp_monic_degree_RD_productright. (exists fom_gap_pfp_monic_degree_RD_productright_index_bound. fom_gap_pfp_monic_degree_RD_productright_index_bound + S (fom_index_pfp_monic_degree_RD_productright) = S d) -> exists fom_value_pfp_monic_degree_RD_productright. ((((exists fom_beta_height_pfp_monic_degree_RD_productright_entry. fom_beta_height_pfp_monic_degree_RD_productright_entry + S (fom_value_pfp_monic_degree_RD_productright) = S ((S (fom_index_pfp_monic_degree_RD_productright)) * dc)) /\ exists fom_beta_quotient_pfp_monic_degree_RD_productright_entry. db = fom_beta_quotient_pfp_monic_degree_RD_productright_entry * S ((S (fom_index_pfp_monic_degree_RD_productright)) * dc) + (fom_value_pfp_monic_degree_RD_productright))) /\ (exists fom_gap_pfp_monic_degree_RD_productright_value_bound. fom_gap_pfp_monic_degree_RD_productright_value_bound + S (fom_value_pfp_monic_degree_RD_productright) = p))) /\ (((((((pfgu_Q_monic_degree_RD)=0 \/ (S d)=0) /\ (((pfgu_P_monic_degree_RD)=0)))) \/ (((~((pfgu_Q_monic_degree_RD)=0)) /\ (((~((S d)=0)) /\ (((pfgu_Q_monic_degree_RD)+(S d)=S (pfgu_P_monic_degree_RD)))))))) /\ ((forall pfc_index_monic_degree_RD_productcoefficients. (exists pfa_gap_monic_degree_RD_productcoefficientsbound. pfa_gap_monic_degree_RD_productcoefficientsbound + S (pfc_index_monic_degree_RD_productcoefficients) = (pfgu_P_monic_degree_RD)) -> exists pfc_value_monic_degree_RD_productcoefficients. ((((exists ff_h_pfp_monic_degree_RD_productcoefficientsentry. ff_h_pfp_monic_degree_RD_productcoefficientsentry + S (pfc_value_monic_degree_RD_productcoefficients) = S ((S (pfc_index_monic_degree_RD_productcoefficients)) * pfgu_pc_monic_degree_RD)) /\ exists ff_q_pfp_monic_degree_RD_productcoefficientsentry. pfgu_pb_monic_degree_RD = ff_q_pfp_monic_degree_RD_productcoefficientsentry * S ((S (pfc_index_monic_degree_RD_productcoefficients)) * pfgu_pc_monic_degree_RD) + (pfc_value_monic_degree_RD_productcoefficients))) /\ ((exists pfc_terms_code_monic_degree_RD_productcoefficientscoefficient pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient pfc_natural_sum_monic_degree_RD_productcoefficientscoefficient. ((forall pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal. (exists pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonalbound. pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonalbound + S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal) = (S (pfc_index_monic_degree_RD_productcoefficients))) -> exists pfc_value_monic_degree_RD_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonalentry. ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonalentry + S (pfc_value_monic_degree_RD_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient)) /\ exists ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonalentry. pfc_terms_code_monic_degree_RD_productcoefficientscoefficient = ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient) + (pfc_value_monic_degree_RD_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm. (((pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)+pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm=(pfc_index_monic_degree_RD_productcoefficients)) /\ ((((((exists pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal) = (pfgu_Q_monic_degree_RD)) /\ ((((exists ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) * pfgu_qc_monic_degree_RD)) /\ exists ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_monic_degree_RD = ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) * pfgu_qc_monic_degree_RD) + (pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_monic_degree_RD)=(pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_monic_degree_RD_productcoefficientscoefficientdiagonal)=pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm*pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum. ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_start. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_start. fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_monic_degree_RD_productcoefficientscoefficient) = S ((S (S (pfc_index_monic_degree_RD_productcoefficients))) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_monic_degree_RD_productcoefficients))) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum) + (pfc_natural_sum_monic_degree_RD_productcoefficientscoefficient))) /\ forall fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps = S (pfc_index_monic_degree_RD_productcoefficients)) -> exists fs_a_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps fs_r_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps fs_s_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_monic_degree_RD_productcoefficientscoefficient = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient) + (fs_a_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum) + (fs_r_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum) + (fs_s_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps = fs_r_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps + fs_a_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_monic_degree_RD_productcoefficientscoefficientresiduebound. pfa_gap_monic_degree_RD_productcoefficientscoefficientresiduebound + S (pfc_value_monic_degree_RD_productcoefficients) = (p)) /\ ((exists pfa_offset_left_monic_degree_RD_productcoefficientscoefficientresiduecongruence pfa_offset_right_monic_degree_RD_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_monic_degree_RD_productcoefficientscoefficient) + (p) * pfa_offset_left_monic_degree_RD_productcoefficientscoefficientresiduecongruence = (pfc_value_monic_degree_RD_productcoefficients) + (p) * pfa_offset_right_monic_degree_RD_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_monic_degree_RD_target pfrep_left_monic_degree_RD_target pfrep_right_monic_degree_RD_target. ((exists pfrep_position_monic_degree_RD_targetfirst. ((pfrep_position_monic_degree_RD_targetfirst+S (pfrep_power_monic_degree_RD_target)=(pfgu_P_monic_degree_RD)) /\ ((((exists ff_h_pfp_monic_degree_RD_targetfirstentry. ff_h_pfp_monic_degree_RD_targetfirstentry + S (pfrep_left_monic_degree_RD_target) = S ((S (pfrep_position_monic_degree_RD_targetfirst)) * pfgu_pc_monic_degree_RD)) /\ exists ff_q_pfp_monic_degree_RD_targetfirstentry. pfgu_pb_monic_degree_RD = ff_q_pfp_monic_degree_RD_targetfirstentry * S ((S (pfrep_position_monic_degree_RD_targetfirst)) * pfgu_pc_monic_degree_RD) + (pfrep_left_monic_degree_RD_target)))))) \/ (((exists pfrep_gap_monic_degree_RD_targetfirstoutside. pfrep_gap_monic_degree_RD_targetfirstoutside+(pfgu_P_monic_degree_RD)=(pfrep_power_monic_degree_RD_target)) /\ (((pfrep_left_monic_degree_RD_target)=0))))) -> ((exists pfrep_position_monic_degree_RD_targetsecond. ((pfrep_position_monic_degree_RD_targetsecond+S (pfrep_power_monic_degree_RD_target)=(S d)) /\ ((((exists ff_h_pfp_monic_degree_RD_targetsecondentry. ff_h_pfp_monic_degree_RD_targetsecondentry + S (pfrep_right_monic_degree_RD_target) = S ((S (pfrep_position_monic_degree_RD_targetsecond)) * ac)) /\ exists ff_q_pfp_monic_degree_RD_targetsecondentry. ab = ff_q_pfp_monic_degree_RD_targetsecondentry * S ((S (pfrep_position_monic_degree_RD_targetsecond)) * ac) + (pfrep_right_monic_degree_RD_target)))))) \/ (((exists pfrep_gap_monic_degree_RD_targetsecondoutside. pfrep_gap_monic_degree_RD_targetsecondoutside+(S d)=(pfrep_power_monic_degree_RD_target)) /\ (((pfrep_right_monic_degree_RD_target)=0))))) -> pfrep_left_monic_degree_RD_target=pfrep_right_monic_degree_RD_target))))))) -> (forall pfrep_power_monic_degree_result pfrep_left_monic_degree_result pfrep_right_monic_degree_result. ((exists pfrep_position_monic_degree_resultfirst. ((pfrep_position_monic_degree_resultfirst+S (pfrep_power_monic_degree_result)=(S d)) /\ ((((exists ff_h_pfp_monic_degree_resultfirstentry. ff_h_pfp_monic_degree_resultfirstentry + S (pfrep_left_monic_degree_result) = S ((S (pfrep_position_monic_degree_resultfirst)) * dc)) /\ exists ff_q_pfp_monic_degree_resultfirstentry. db = ff_q_pfp_monic_degree_resultfirstentry * S ((S (pfrep_position_monic_degree_resultfirst)) * dc) + (pfrep_left_monic_degree_result)))))) \/ (((exists pfrep_gap_monic_degree_resultfirstoutside. pfrep_gap_monic_degree_resultfirstoutside+(S d)=(pfrep_power_monic_degree_result)) /\ (((pfrep_left_monic_degree_result)=0))))) -> ((exists pfrep_position_monic_degree_resultsecond. ((pfrep_position_monic_degree_resultsecond+S (pfrep_power_monic_degree_result)=(S d)) /\ ((((exists ff_h_pfp_monic_degree_resultsecondentry. ff_h_pfp_monic_degree_resultsecondentry + S (pfrep_right_monic_degree_result) = S ((S (pfrep_position_monic_degree_resultsecond)) * ac)) /\ exists ff_q_pfp_monic_degree_resultsecondentry. ab = ff_q_pfp_monic_degree_resultsecondentry * S ((S (pfrep_position_monic_degree_resultsecond)) * ac) + (pfrep_right_monic_degree_result)))))) \/ (((exists pfrep_gap_monic_degree_resultsecondoutside. pfrep_gap_monic_degree_resultsecondoutside+(S d)=(pfrep_power_monic_degree_result)) /\ (((pfrep_right_monic_degree_result)=0))))) -> pfrep_left_monic_degree_result=pfrep_right_monic_degree_result)

Constructive proof overview

Generated structural guide

Equal-degree monic right divisibility has a genuinely constructed degree-zero quotient. Its head must be one, so divisor and target are formally equivalent.

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

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

Proof neighborhood

Direct dependencies

prime_field_polynomial_monic_represented_degree Alpha theorem; checked-use authorized PG0070 prime_field_polynomial_right_divides_represented_factorization add_right_cancel Alpha theorem; checked-use authorized zero_add Alpha theorem; checked-use authorized PG0072 prime_field_polynomial_monic_singleton_multiple_equivalent

Direct dependents

PG0074 prime_field_polynomial_monic_right_associates_equivalent

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

84 script commands · 10 reading checkpoints · 5 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
prime field polynomial right divides represented factorizationprime field polynomial monic singleton multiple equivalent

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro db
  3. L3
    intro dc
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro d
  7. L7
    intro hp
  8. L8
    intro hd
  9. L9
    intro ha
  10. L10
    intro hrd
02Establish hddL11–19

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

  1. L11
    have hdd : FpRepresentedDegree(p,db,dc,S d,d)Definitions: FpRepresentedDegree
  2. L12
    specialize prime_field_polynomial_monic_represented_degree (p)
  3. L13
    specialize prime_field_polynomial_monic_represented_degree (db)
  4. L14
    specialize prime_field_polynomial_monic_represented_degree (dc)
  5. L15
    specialize prime_field_polynomial_monic_represented_degree (S d)
  6. L16
    specialize prime_field_polynomial_monic_represented_degree (d)
  7. L17
    apply prime_field_polynomial_monic_represented_degree
  8. L18
    exact hd
  9. L19
    refl
03Establish hadL20–28

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

  1. L20
    have had : FpRepresentedDegree(p,ab,ac,S d,d)Definitions: FpRepresentedDegree
  2. L21
    specialize prime_field_polynomial_monic_represented_degree (p)
  3. L22
    specialize prime_field_polynomial_monic_represented_degree (ab)
  4. L23
    specialize prime_field_polynomial_monic_represented_degree (ac)
  5. L24
    specialize prime_field_polynomial_monic_represented_degree (S d)
  6. L25
    specialize prime_field_polynomial_monic_represented_degree (d)
  7. L26
    apply prime_field_polynomial_monic_represented_degree
  8. L27
    exact ha
  9. L28
    refl
04Establish hfL29–38

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

  1. L29
    have hf · expand full local formula (607 characters)have hf : ∃ pfgu_qb_monic_degree_factor. ∃ pfgu_qc_monic_degree_factor. ∃ pfgu_e_monic_degree_factor. ∃ pfgu_pb_monic_degree_factor. ∃ pfgu_pc_monic_degree_factor. FpRepresentedDegree(p,pfgu_qb_monic_degree_factor,pfgu_qc_monic_degree_factor,S pfgu_e_monic_degree_factor,pfgu_e_monic_degree_factor) ∧ (FpPolyProduct(p,pfgu_qb_monic_degree_factor,pfgu_qc_monic_degree_factor,S pfgu_e_monic_degree_factor,db,dc,S d,pfgu_pb_monic_degree_factor,pfgu_pc_monic_degree_factor,S d) ∧ (PolynomialEquivalent(pfgu_pb_monic_degree_factor,pfgu_pc_monic_degree_factor,S d,ab,ac,S d) ∧ pfgu_e_monic_degree_factor + d = d))
    Definitions: FpPolyProductFpRepresentedDegreePolynomialEquivalent
  2. L30
    specialize prime_field_polynomial_right_divides_represented_factorization (p)
  3. L31
    specialize prime_field_polynomial_right_divides_represented_factorization (db)
  4. L32
    specialize prime_field_polynomial_right_divides_represented_factorization (dc)
  5. L33
    specialize prime_field_polynomial_right_divides_represented_factorization (S d)
  6. L34
    specialize prime_field_polynomial_right_divides_represented_factorization (d)
  7. L35
    specialize prime_field_polynomial_right_divides_represented_factorization (ab)
  8. L36
    specialize prime_field_polynomial_right_divides_represented_factorization (ac)
  9. L37
    specialize prime_field_polynomial_right_divides_represented_factorization (S d)
  10. L38
    specialize prime_field_polynomial_right_divides_represented_factorization (d)
05Use earlier factsL39–43

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

  1. L39
    apply prime_field_polynomial_right_divides_represented_factorization
  2. L40
    exact hp
  3. L41
    exact hdd
  4. L42
    exact had
  5. L43
    exact hrd
06Separate the logical casesL44–51

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

  1. L44
    cases hf
  2. L45
    cases hf_witness
  3. L46
    cases hf_witness_witness
  4. L47
    cases hf_witness_witness_witness
  5. L48
    cases hf_witness_witness_witness_witness
  6. L49
    cases hf_witness_witness_witness_witness_witness
  7. L50
    cases hf_witness_witness_witness_witness_witness_right
  8. L51
    cases hf_witness_witness_witness_witness_witness_right_right
07Establish hezeroL52–61

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

  1. L52
    have hezero : x2=0
  2. L53
    specialize add_right_cancel (x2)
  3. L54
    specialize add_right_cancel (0)
  4. L55
    specialize add_right_cancel (d)
  5. L56
    apply add_right_cancel
  6. L57
    trans d
  7. L58
    exact hf_witness_witness_witness_witness_witness_right_right_right
  8. L59
    symm
  9. L60
    apply zero_add
  10. L61
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (p)
08Use earlier factsL62–71

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

  1. L62
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x)
  2. L63
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x1)
  3. L64
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (db)
  4. L65
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (dc)
  5. L66
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (ab)
  6. L67
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (ac)
  7. L68
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (d)
  8. L69
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x3)
  9. L70
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x4)
  10. L71
    apply prime_field_polynomial_monic_singleton_multiple_equivalent
09Use earlier factsL72–74

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

  1. L72
    exact hp
  2. L73
    exact hd
  3. L74
    exact ha
10Establish hproductL75–84

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

  1. L75
    have hproduct : FpPolyProduct(p,x,x1,S x2,db,dc,S d,x3,x4,S d)Definitions: FpPolyProduct
  2. L76
    exact hf_witness_witness_witness_witness_witness_right_left
  3. L77
    rewrite hezero at hproduct
  4. L78
    rewrite hezero at hproduct
  5. L79
    rewrite hezero at hproduct
  6. L80
    rewrite hezero at hproduct
  7. L81
    rewrite hezero at hproduct
  8. L82
    rewrite hezero at hproduct
  9. L83
    exact hproduct
  10. L84
    exact hf_witness_witness_witness_witness_witness_right_right_left

Library-wide reading audit

Original exact command ledger · 84 lines
  1. 0001intro p
  2. 0002intro db
  3. 0003intro dc
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro d
  7. 0007intro hp
  8. 0008intro hd
  9. 0009intro ha
  10. 0010intro hrd
  11. 0011have hdd : (((S d)=S (d)) /\ (((forall fom_index_pfp_monic_degree_divisorcoefficients. (exists fom_gap_pfp_monic_degree_divisorcoefficients_index_bound. fom_gap_pfp_monic_degree_divisorcoefficients_index_bound + S (fom_index_pfp_monic_degree_divisorcoefficients) = S d) -> exists fom_value_pfp_monic_degree_divisorcoefficients. ((((exists fom_beta_height_pfp_monic_degree_divisorcoefficients_entry. fom_beta_height_pfp_monic_degree_divisorcoefficients_entry + S (fom_value_pfp_monic_degree_divisorcoefficients) = S ((S (fom_index_pfp_monic_degree_divisorcoefficients)) * dc)) /\ exists fom_beta_quotient_pfp_monic_degree_divisorcoefficients_entry. db = fom_beta_quotient_pfp_monic_degree_divisorcoefficients_entry * S ((S (fom_index_pfp_monic_degree_divisorcoefficients)) * dc) + (fom_value_pfp_monic_degree_divisorcoefficients))) /\ (exists fom_gap_pfp_monic_degree_divisorcoefficients_value_bound. fom_gap_pfp_monic_degree_divisorcoefficients_value_bound + S (fom_value_pfp_monic_degree_divisorcoefficients) = p))) /\ ((exists pfd_leading_monic_degree_divisor. ((((exists ff_h_pfp_monic_degree_divisorentry. ff_h_pfp_monic_degree_divisorentry + S (pfd_leading_monic_degree_divisor) = S ((S (0)) * dc)) /\ exists ff_q_pfp_monic_degree_divisorentry. db = ff_q_pfp_monic_degree_divisorentry * S ((S (0)) * dc) + (pfd_leading_monic_degree_divisor))) /\ ((~(pfd_leading_monic_degree_divisor=0)))))))))
  12. 0012specialize prime_field_polynomial_monic_represented_degree (p)
  13. 0013specialize prime_field_polynomial_monic_represented_degree (db)
  14. 0014specialize prime_field_polynomial_monic_represented_degree (dc)
  15. 0015specialize prime_field_polynomial_monic_represented_degree (S d)
  16. 0016specialize prime_field_polynomial_monic_represented_degree (d)
  17. 0017apply prime_field_polynomial_monic_represented_degree
  18. 0018exact hd
  19. 0019refl
  20. 0020have had : (((S d)=S (d)) /\ (((forall fom_index_pfp_monic_degree_targetcoefficients. (exists fom_gap_pfp_monic_degree_targetcoefficients_index_bound. fom_gap_pfp_monic_degree_targetcoefficients_index_bound + S (fom_index_pfp_monic_degree_targetcoefficients) = S d) -> exists fom_value_pfp_monic_degree_targetcoefficients. ((((exists fom_beta_height_pfp_monic_degree_targetcoefficients_entry. fom_beta_height_pfp_monic_degree_targetcoefficients_entry + S (fom_value_pfp_monic_degree_targetcoefficients) = S ((S (fom_index_pfp_monic_degree_targetcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_monic_degree_targetcoefficients_entry. ab = fom_beta_quotient_pfp_monic_degree_targetcoefficients_entry * S ((S (fom_index_pfp_monic_degree_targetcoefficients)) * ac) + (fom_value_pfp_monic_degree_targetcoefficients))) /\ (exists fom_gap_pfp_monic_degree_targetcoefficients_value_bound. fom_gap_pfp_monic_degree_targetcoefficients_value_bound + S (fom_value_pfp_monic_degree_targetcoefficients) = p))) /\ ((exists pfd_leading_monic_degree_target. ((((exists ff_h_pfp_monic_degree_targetentry. ff_h_pfp_monic_degree_targetentry + S (pfd_leading_monic_degree_target) = S ((S (0)) * ac)) /\ exists ff_q_pfp_monic_degree_targetentry. ab = ff_q_pfp_monic_degree_targetentry * S ((S (0)) * ac) + (pfd_leading_monic_degree_target))) /\ ((~(pfd_leading_monic_degree_target=0)))))))))
  21. 0021specialize prime_field_polynomial_monic_represented_degree (p)
  22. 0022specialize prime_field_polynomial_monic_represented_degree (ab)
  23. 0023specialize prime_field_polynomial_monic_represented_degree (ac)
  24. 0024specialize prime_field_polynomial_monic_represented_degree (S d)
  25. 0025specialize prime_field_polynomial_monic_represented_degree (d)
  26. 0026apply prime_field_polynomial_monic_represented_degree
  27. 0027exact ha
  28. 0028refl
  29. 0029have hf : exists pfgu_qb_monic_degree_factor pfgu_qc_monic_degree_factor pfgu_e_monic_degree_factor pfgu_pb_monic_degree_factor pfgu_pc_monic_degree_factor. (((((S (pfgu_e_monic_degree_factor))=S (pfgu_e_monic_degree_factor)) /\ (((forall fom_index_pfp_monic_degree_factor_quotientcoefficients. (exists fom_gap_pfp_monic_degree_factor_quotientcoefficients_index_bound. fom_gap_pfp_monic_degree_factor_quotientcoefficients_index_bound + S (fom_index_pfp_monic_degree_factor_quotientcoefficients) = S (pfgu_e_monic_degree_factor)) -> exists fom_value_pfp_monic_degree_factor_quotientcoefficients. ((((exists fom_beta_height_pfp_monic_degree_factor_quotientcoefficients_entry. fom_beta_height_pfp_monic_degree_factor_quotientcoefficients_entry + S (fom_value_pfp_monic_degree_factor_quotientcoefficients) = S ((S (fom_index_pfp_monic_degree_factor_quotientcoefficients)) * pfgu_qc_monic_degree_factor)) /\ exists fom_beta_quotient_pfp_monic_degree_factor_quotientcoefficients_entry. pfgu_qb_monic_degree_factor = fom_beta_quotient_pfp_monic_degree_factor_quotientcoefficients_entry * S ((S (fom_index_pfp_monic_degree_factor_quotientcoefficients)) * pfgu_qc_monic_degree_factor) + (fom_value_pfp_monic_degree_factor_quotientcoefficients))) /\ (exists fom_gap_pfp_monic_degree_factor_quotientcoefficients_value_bound. fom_gap_pfp_monic_degree_factor_quotientcoefficients_value_bound + S (fom_value_pfp_monic_degree_factor_quotientcoefficients) = p))) /\ ((exists pfd_leading_monic_degree_factor_quotient. ((((exists ff_h_pfp_monic_degree_factor_quotiententry. ff_h_pfp_monic_degree_factor_quotiententry + S (pfd_leading_monic_degree_factor_quotient) = S ((S (0)) * pfgu_qc_monic_degree_factor)) /\ exists ff_q_pfp_monic_degree_factor_quotiententry. pfgu_qb_monic_degree_factor = ff_q_pfp_monic_degree_factor_quotiententry * S ((S (0)) * pfgu_qc_monic_degree_factor) + (pfd_leading_monic_degree_factor_quotient))) /\ ((~(pfd_leading_monic_degree_factor_quotient=0)))))))))) /\ (((((forall fom_index_pfp_monic_degree_factor_productleft. (exists fom_gap_pfp_monic_degree_factor_productleft_index_bound. fom_gap_pfp_monic_degree_factor_productleft_index_bound + S (fom_index_pfp_monic_degree_factor_productleft) = S (pfgu_e_monic_degree_factor)) -> exists fom_value_pfp_monic_degree_factor_productleft. ((((exists fom_beta_height_pfp_monic_degree_factor_productleft_entry. fom_beta_height_pfp_monic_degree_factor_productleft_entry + S (fom_value_pfp_monic_degree_factor_productleft) = S ((S (fom_index_pfp_monic_degree_factor_productleft)) * pfgu_qc_monic_degree_factor)) /\ exists fom_beta_quotient_pfp_monic_degree_factor_productleft_entry. pfgu_qb_monic_degree_factor = fom_beta_quotient_pfp_monic_degree_factor_productleft_entry * S ((S (fom_index_pfp_monic_degree_factor_productleft)) * pfgu_qc_monic_degree_factor) + (fom_value_pfp_monic_degree_factor_productleft))) /\ (exists fom_gap_pfp_monic_degree_factor_productleft_value_bound. fom_gap_pfp_monic_degree_factor_productleft_value_bound + S (fom_value_pfp_monic_degree_factor_productleft) = p))) /\ (((forall fom_index_pfp_monic_degree_factor_productright. (exists fom_gap_pfp_monic_degree_factor_productright_index_bound. fom_gap_pfp_monic_degree_factor_productright_index_bound + S (fom_index_pfp_monic_degree_factor_productright) = S d) -> exists fom_value_pfp_monic_degree_factor_productright. ((((exists fom_beta_height_pfp_monic_degree_factor_productright_entry. fom_beta_height_pfp_monic_degree_factor_productright_entry + S (fom_value_pfp_monic_degree_factor_productright) = S ((S (fom_index_pfp_monic_degree_factor_productright)) * dc)) /\ exists fom_beta_quotient_pfp_monic_degree_factor_productright_entry. db = fom_beta_quotient_pfp_monic_degree_factor_productright_entry * S ((S (fom_index_pfp_monic_degree_factor_productright)) * dc) + (fom_value_pfp_monic_degree_factor_productright))) /\ (exists fom_gap_pfp_monic_degree_factor_productright_value_bound. fom_gap_pfp_monic_degree_factor_productright_value_bound + S (fom_value_pfp_monic_degree_factor_productright) = p))) /\ (((((((S (pfgu_e_monic_degree_factor))=0 \/ (S d)=0) /\ (((S (d))=0)))) \/ (((~((S (pfgu_e_monic_degree_factor))=0)) /\ (((~((S d)=0)) /\ (((S (pfgu_e_monic_degree_factor))+(S d)=S (S (d))))))))) /\ ((forall pfc_index_monic_degree_factor_productcoefficients. (exists pfa_gap_monic_degree_factor_productcoefficientsbound. pfa_gap_monic_degree_factor_productcoefficientsbound + S (pfc_index_monic_degree_factor_productcoefficients) = (S (d))) -> exists pfc_value_monic_degree_factor_productcoefficients. ((((exists ff_h_pfp_monic_degree_factor_productcoefficientsentry. ff_h_pfp_monic_degree_factor_productcoefficientsentry + S (pfc_value_monic_degree_factor_productcoefficients) = S ((S (pfc_index_monic_degree_factor_productcoefficients)) * pfgu_pc_monic_degree_factor)) /\ exists ff_q_pfp_monic_degree_factor_productcoefficientsentry. pfgu_pb_monic_degree_factor = ff_q_pfp_monic_degree_factor_productcoefficientsentry * S ((S (pfc_index_monic_degree_factor_productcoefficients)) * pfgu_pc_monic_degree_factor) + (pfc_value_monic_degree_factor_productcoefficients))) /\ ((exists pfc_terms_code_monic_degree_factor_productcoefficientscoefficient pfc_terms_scale_monic_degree_factor_productcoefficientscoefficient pfc_natural_sum_monic_degree_factor_productcoefficientscoefficient. ((forall pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal. (exists pfa_gap_monic_degree_factor_productcoefficientscoefficientdiagonalbound. pfa_gap_monic_degree_factor_productcoefficientscoefficientdiagonalbound + S (pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal) = (S (pfc_index_monic_degree_factor_productcoefficients))) -> exists pfc_value_monic_degree_factor_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_monic_degree_factor_productcoefficientscoefficientdiagonalentry. ff_h_pfp_monic_degree_factor_productcoefficientscoefficientdiagonalentry + S (pfc_value_monic_degree_factor_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_monic_degree_factor_productcoefficientscoefficient)) /\ exists ff_q_pfp_monic_degree_factor_productcoefficientscoefficientdiagonalentry. pfc_terms_code_monic_degree_factor_productcoefficientscoefficient = ff_q_pfp_monic_degree_factor_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_monic_degree_factor_productcoefficientscoefficient) + (pfc_value_monic_degree_factor_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_monic_degree_factor_productcoefficientscoefficientdiagonalterm pfc_left_monic_degree_factor_productcoefficientscoefficientdiagonalterm pfc_right_monic_degree_factor_productcoefficientscoefficientdiagonalterm. (((pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal)+pfc_complement_monic_degree_factor_productcoefficientscoefficientdiagonalterm=(pfc_index_monic_degree_factor_productcoefficients)) /\ ((((((exists pfa_gap_monic_degree_factor_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_monic_degree_factor_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal) = (S (pfgu_e_monic_degree_factor))) /\ ((((exists ff_h_pfp_monic_degree_factor_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_monic_degree_factor_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_monic_degree_factor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal)) * pfgu_qc_monic_degree_factor)) /\ exists ff_q_pfp_monic_degree_factor_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_monic_degree_factor = ff_q_pfp_monic_degree_factor_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal)) * pfgu_qc_monic_degree_factor) + (pfc_left_monic_degree_factor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_monic_degree_factor_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_monic_degree_factor_productcoefficientscoefficientdiagonaltermleftoutside+(S (pfgu_e_monic_degree_factor))=(pfc_index_monic_degree_factor_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_monic_degree_factor_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_monic_degree_factor_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_monic_degree_factor_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_monic_degree_factor_productcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_monic_degree_factor_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_monic_degree_factor_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_monic_degree_factor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_monic_degree_factor_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_monic_degree_factor_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_monic_degree_factor_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_monic_degree_factor_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_monic_degree_factor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_monic_degree_factor_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_monic_degree_factor_productcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_monic_degree_factor_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_monic_degree_factor_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_monic_degree_factor_productcoefficientscoefficientdiagonal)=pfc_left_monic_degree_factor_productcoefficientscoefficientdiagonalterm*pfc_right_monic_degree_factor_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_monic_degree_factor_productcoefficientscoefficientsum fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum. ((((exists fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_start. fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_start. fs_u_pfc_monic_degree_factor_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_monic_degree_factor_productcoefficientscoefficient) = S ((S (S (pfc_index_monic_degree_factor_productcoefficients))) * fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_monic_degree_factor_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_monic_degree_factor_productcoefficients))) * fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum) + (pfc_natural_sum_monic_degree_factor_productcoefficientscoefficient))) /\ forall fs_i_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps = S (pfc_index_monic_degree_factor_productcoefficients)) -> exists fs_a_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps fs_r_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps fs_s_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_monic_degree_factor_productcoefficientscoefficient)) /\ exists fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_monic_degree_factor_productcoefficientscoefficient = fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_monic_degree_factor_productcoefficientscoefficient) + (fs_a_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_monic_degree_factor_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum) + (fs_r_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_monic_degree_factor_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_factor_productcoefficientscoefficientsum) + (fs_s_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps = fs_r_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps + fs_a_pfc_monic_degree_factor_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_monic_degree_factor_productcoefficientscoefficientresiduebound. pfa_gap_monic_degree_factor_productcoefficientscoefficientresiduebound + S (pfc_value_monic_degree_factor_productcoefficients) = (p)) /\ ((exists pfa_offset_left_monic_degree_factor_productcoefficientscoefficientresiduecongruence pfa_offset_right_monic_degree_factor_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_monic_degree_factor_productcoefficientscoefficient) + (p) * pfa_offset_left_monic_degree_factor_productcoefficientscoefficientresiduecongruence = (pfc_value_monic_degree_factor_productcoefficients) + (p) * pfa_offset_right_monic_degree_factor_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((forall pfrep_power_monic_degree_factor_equivalent pfrep_left_monic_degree_factor_equivalent pfrep_right_monic_degree_factor_equivalent. ((exists pfrep_position_monic_degree_factor_equivalentfirst. ((pfrep_position_monic_degree_factor_equivalentfirst+S (pfrep_power_monic_degree_factor_equivalent)=(S (d))) /\ ((((exists ff_h_pfp_monic_degree_factor_equivalentfirstentry. ff_h_pfp_monic_degree_factor_equivalentfirstentry + S (pfrep_left_monic_degree_factor_equivalent) = S ((S (pfrep_position_monic_degree_factor_equivalentfirst)) * pfgu_pc_monic_degree_factor)) /\ exists ff_q_pfp_monic_degree_factor_equivalentfirstentry. pfgu_pb_monic_degree_factor = ff_q_pfp_monic_degree_factor_equivalentfirstentry * S ((S (pfrep_position_monic_degree_factor_equivalentfirst)) * pfgu_pc_monic_degree_factor) + (pfrep_left_monic_degree_factor_equivalent)))))) \/ (((exists pfrep_gap_monic_degree_factor_equivalentfirstoutside. pfrep_gap_monic_degree_factor_equivalentfirstoutside+(S (d))=(pfrep_power_monic_degree_factor_equivalent)) /\ (((pfrep_left_monic_degree_factor_equivalent)=0))))) -> ((exists pfrep_position_monic_degree_factor_equivalentsecond. ((pfrep_position_monic_degree_factor_equivalentsecond+S (pfrep_power_monic_degree_factor_equivalent)=(S d)) /\ ((((exists ff_h_pfp_monic_degree_factor_equivalentsecondentry. ff_h_pfp_monic_degree_factor_equivalentsecondentry + S (pfrep_right_monic_degree_factor_equivalent) = S ((S (pfrep_position_monic_degree_factor_equivalentsecond)) * ac)) /\ exists ff_q_pfp_monic_degree_factor_equivalentsecondentry. ab = ff_q_pfp_monic_degree_factor_equivalentsecondentry * S ((S (pfrep_position_monic_degree_factor_equivalentsecond)) * ac) + (pfrep_right_monic_degree_factor_equivalent)))))) \/ (((exists pfrep_gap_monic_degree_factor_equivalentsecondoutside. pfrep_gap_monic_degree_factor_equivalentsecondoutside+(S d)=(pfrep_power_monic_degree_factor_equivalent)) /\ (((pfrep_right_monic_degree_factor_equivalent)=0))))) -> pfrep_left_monic_degree_factor_equivalent=pfrep_right_monic_degree_factor_equivalent) /\ (((pfgu_e_monic_degree_factor)+(d)=(d))))))))
  30. 0030specialize prime_field_polynomial_right_divides_represented_factorization (p)
  31. 0031specialize prime_field_polynomial_right_divides_represented_factorization (db)
  32. 0032specialize prime_field_polynomial_right_divides_represented_factorization (dc)
  33. 0033specialize prime_field_polynomial_right_divides_represented_factorization (S d)
  34. 0034specialize prime_field_polynomial_right_divides_represented_factorization (d)
  35. 0035specialize prime_field_polynomial_right_divides_represented_factorization (ab)
  36. 0036specialize prime_field_polynomial_right_divides_represented_factorization (ac)
  37. 0037specialize prime_field_polynomial_right_divides_represented_factorization (S d)
  38. 0038specialize prime_field_polynomial_right_divides_represented_factorization (d)
  39. 0039apply prime_field_polynomial_right_divides_represented_factorization
  40. 0040exact hp
  41. 0041exact hdd
  42. 0042exact had
  43. 0043exact hrd
  44. 0044cases hf
  45. 0045cases hf_witness
  46. 0046cases hf_witness_witness
  47. 0047cases hf_witness_witness_witness
  48. 0048cases hf_witness_witness_witness_witness
  49. 0049cases hf_witness_witness_witness_witness_witness
  50. 0050cases hf_witness_witness_witness_witness_witness_right
  51. 0051cases hf_witness_witness_witness_witness_witness_right_right
  52. 0052have hezero : x2=0
  53. 0053specialize add_right_cancel (x2)
  54. 0054specialize add_right_cancel (0)
  55. 0055specialize add_right_cancel (d)
  56. 0056apply add_right_cancel
  57. 0057trans d
  58. 0058exact hf_witness_witness_witness_witness_witness_right_right_right
  59. 0059symm
  60. 0060apply zero_add
  61. 0061specialize prime_field_polynomial_monic_singleton_multiple_equivalent (p)
  62. 0062specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x)
  63. 0063specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x1)
  64. 0064specialize prime_field_polynomial_monic_singleton_multiple_equivalent (db)
  65. 0065specialize prime_field_polynomial_monic_singleton_multiple_equivalent (dc)
  66. 0066specialize prime_field_polynomial_monic_singleton_multiple_equivalent (ab)
  67. 0067specialize prime_field_polynomial_monic_singleton_multiple_equivalent (ac)
  68. 0068specialize prime_field_polynomial_monic_singleton_multiple_equivalent (d)
  69. 0069specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x3)
  70. 0070specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x4)
  71. 0071apply prime_field_polynomial_monic_singleton_multiple_equivalent
  72. 0072exact hp
  73. 0073exact hd
  74. 0074exact ha
  75. 0075have hproduct : ((forall fom_index_pfp_monic_degree_productleft. (exists fom_gap_pfp_monic_degree_productleft_index_bound. fom_gap_pfp_monic_degree_productleft_index_bound + S (fom_index_pfp_monic_degree_productleft) = S x2) -> exists fom_value_pfp_monic_degree_productleft. ((((exists fom_beta_height_pfp_monic_degree_productleft_entry. fom_beta_height_pfp_monic_degree_productleft_entry + S (fom_value_pfp_monic_degree_productleft) = S ((S (fom_index_pfp_monic_degree_productleft)) * x1)) /\ exists fom_beta_quotient_pfp_monic_degree_productleft_entry. x = fom_beta_quotient_pfp_monic_degree_productleft_entry * S ((S (fom_index_pfp_monic_degree_productleft)) * x1) + (fom_value_pfp_monic_degree_productleft))) /\ (exists fom_gap_pfp_monic_degree_productleft_value_bound. fom_gap_pfp_monic_degree_productleft_value_bound + S (fom_value_pfp_monic_degree_productleft) = p))) /\ (((forall fom_index_pfp_monic_degree_productright. (exists fom_gap_pfp_monic_degree_productright_index_bound. fom_gap_pfp_monic_degree_productright_index_bound + S (fom_index_pfp_monic_degree_productright) = S d) -> exists fom_value_pfp_monic_degree_productright. ((((exists fom_beta_height_pfp_monic_degree_productright_entry. fom_beta_height_pfp_monic_degree_productright_entry + S (fom_value_pfp_monic_degree_productright) = S ((S (fom_index_pfp_monic_degree_productright)) * dc)) /\ exists fom_beta_quotient_pfp_monic_degree_productright_entry. db = fom_beta_quotient_pfp_monic_degree_productright_entry * S ((S (fom_index_pfp_monic_degree_productright)) * dc) + (fom_value_pfp_monic_degree_productright))) /\ (exists fom_gap_pfp_monic_degree_productright_value_bound. fom_gap_pfp_monic_degree_productright_value_bound + S (fom_value_pfp_monic_degree_productright) = p))) /\ (((((((S x2)=0 \/ (S d)=0) /\ (((S d)=0)))) \/ (((~((S x2)=0)) /\ (((~((S d)=0)) /\ (((S x2)+(S d)=S (S d)))))))) /\ ((forall pfc_index_monic_degree_productcoefficients. (exists pfa_gap_monic_degree_productcoefficientsbound. pfa_gap_monic_degree_productcoefficientsbound + S (pfc_index_monic_degree_productcoefficients) = (S d)) -> exists pfc_value_monic_degree_productcoefficients. ((((exists ff_h_pfp_monic_degree_productcoefficientsentry. ff_h_pfp_monic_degree_productcoefficientsentry + S (pfc_value_monic_degree_productcoefficients) = S ((S (pfc_index_monic_degree_productcoefficients)) * x4)) /\ exists ff_q_pfp_monic_degree_productcoefficientsentry. x3 = ff_q_pfp_monic_degree_productcoefficientsentry * S ((S (pfc_index_monic_degree_productcoefficients)) * x4) + (pfc_value_monic_degree_productcoefficients))) /\ ((exists pfc_terms_code_monic_degree_productcoefficientscoefficient pfc_terms_scale_monic_degree_productcoefficientscoefficient pfc_natural_sum_monic_degree_productcoefficientscoefficient. ((forall pfc_index_monic_degree_productcoefficientscoefficientdiagonal. (exists pfa_gap_monic_degree_productcoefficientscoefficientdiagonalbound. pfa_gap_monic_degree_productcoefficientscoefficientdiagonalbound + S (pfc_index_monic_degree_productcoefficientscoefficientdiagonal) = (S (pfc_index_monic_degree_productcoefficients))) -> exists pfc_value_monic_degree_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_monic_degree_productcoefficientscoefficientdiagonalentry. ff_h_pfp_monic_degree_productcoefficientscoefficientdiagonalentry + S (pfc_value_monic_degree_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_monic_degree_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_monic_degree_productcoefficientscoefficient)) /\ exists ff_q_pfp_monic_degree_productcoefficientscoefficientdiagonalentry. pfc_terms_code_monic_degree_productcoefficientscoefficient = ff_q_pfp_monic_degree_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_monic_degree_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_monic_degree_productcoefficientscoefficient) + (pfc_value_monic_degree_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_monic_degree_productcoefficientscoefficientdiagonalterm pfc_left_monic_degree_productcoefficientscoefficientdiagonalterm pfc_right_monic_degree_productcoefficientscoefficientdiagonalterm. (((pfc_index_monic_degree_productcoefficientscoefficientdiagonal)+pfc_complement_monic_degree_productcoefficientscoefficientdiagonalterm=(pfc_index_monic_degree_productcoefficients)) /\ ((((((exists pfa_gap_monic_degree_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_monic_degree_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_monic_degree_productcoefficientscoefficientdiagonal) = (S x2)) /\ ((((exists ff_h_pfp_monic_degree_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_monic_degree_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_monic_degree_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_monic_degree_productcoefficientscoefficientdiagonal)) * x1)) /\ exists ff_q_pfp_monic_degree_productcoefficientscoefficientdiagonaltermleftentry. x = ff_q_pfp_monic_degree_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_monic_degree_productcoefficientscoefficientdiagonal)) * x1) + (pfc_left_monic_degree_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_monic_degree_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_monic_degree_productcoefficientscoefficientdiagonaltermleftoutside+(S x2)=(pfc_index_monic_degree_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_monic_degree_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_monic_degree_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_monic_degree_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_monic_degree_productcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_monic_degree_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_monic_degree_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_monic_degree_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_monic_degree_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_monic_degree_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_monic_degree_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_monic_degree_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_monic_degree_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_monic_degree_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_monic_degree_productcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_monic_degree_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_monic_degree_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_monic_degree_productcoefficientscoefficientdiagonal)=pfc_left_monic_degree_productcoefficientscoefficientdiagonalterm*pfc_right_monic_degree_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_monic_degree_productcoefficientscoefficientsum fs_v_pfc_monic_degree_productcoefficientscoefficientsum. ((((exists fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_start. fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_monic_degree_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_start. fs_u_pfc_monic_degree_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_monic_degree_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_monic_degree_productcoefficientscoefficient) = S ((S (S (pfc_index_monic_degree_productcoefficients))) * fs_v_pfc_monic_degree_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_monic_degree_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_monic_degree_productcoefficients))) * fs_v_pfc_monic_degree_productcoefficientscoefficientsum) + (pfc_natural_sum_monic_degree_productcoefficientscoefficient))) /\ forall fs_i_pfc_monic_degree_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_monic_degree_productcoefficientscoefficientsum_body_steps = S (pfc_index_monic_degree_productcoefficients)) -> exists fs_a_pfc_monic_degree_productcoefficientscoefficientsum_body_steps fs_r_pfc_monic_degree_productcoefficientscoefficientsum_body_steps fs_s_pfc_monic_degree_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_monic_degree_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_monic_degree_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_monic_degree_productcoefficientscoefficient)) /\ exists fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_monic_degree_productcoefficientscoefficient = fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_monic_degree_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_monic_degree_productcoefficientscoefficient) + (fs_a_pfc_monic_degree_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_monic_degree_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_monic_degree_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_monic_degree_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_monic_degree_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_productcoefficientscoefficientsum) + (fs_r_pfc_monic_degree_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_monic_degree_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_monic_degree_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_monic_degree_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_monic_degree_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_productcoefficientscoefficientsum) + (fs_s_pfc_monic_degree_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_monic_degree_productcoefficientscoefficientsum_body_steps = fs_r_pfc_monic_degree_productcoefficientscoefficientsum_body_steps + fs_a_pfc_monic_degree_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_monic_degree_productcoefficientscoefficientresiduebound. pfa_gap_monic_degree_productcoefficientscoefficientresiduebound + S (pfc_value_monic_degree_productcoefficients) = (p)) /\ ((exists pfa_offset_left_monic_degree_productcoefficientscoefficientresiduecongruence pfa_offset_right_monic_degree_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_monic_degree_productcoefficientscoefficient) + (p) * pfa_offset_left_monic_degree_productcoefficientscoefficientresiduecongruence = (pfc_value_monic_degree_productcoefficients) + (p) * pfa_offset_right_monic_degree_productcoefficientscoefficientresiduecongruence))))))))))))))))))
  76. 0076exact hf_witness_witness_witness_witness_witness_right_left
  77. 0077rewrite hezero at hproduct
  78. 0078rewrite hezero at hproduct
  79. 0079rewrite hezero at hproduct
  80. 0080rewrite hezero at hproduct
  81. 0081rewrite hezero at hproduct
  82. 0082rewrite hezero at hproduct
  83. 0083exact hproduct
  84. 0084exact hf_witness_witness_witness_witness_witness_right_right_left