PG0076

prime_field_polynomial_normal_right_associates_equivalent

Two zero-or-monic mutual right associates are formally equivalent, including both-zero and one-empty branches. Both normalization premises are essential; beta encodings need not agree.

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. ∀ gb. ∀ gc. ∀ G. ∀ hb. ∀ hc. ∀ H. Prime(p) → FpPolynomialZeroOrMonic(p,gb,gc,G) → FpPolynomialZeroOrMonic(p,hb,hc,H) → FpPolynomialRightDivides(p,gb,gc,G,hb,hc,H) → FpPolynomialRightDivides(p,hb,hc,H,gb,gc,G) → PolynomialEquivalent(gb,gc,G,hb,hc,H)

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

Definition DAG

PolynomialEquivalent(b,c,L,d,e,M) · 1FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 4FpPolynomialZeroOrMonic(p,gb,gc,G) · 2Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_empty_right_divisor_implies_equivalent_zeroprime_field_polynomial_monic_right_associates_equivalent
Original expanded first-order statement 
forall p gb gc G hb hc H. (~((p) = 1) /\ forall pfa_factor_left_normal_prime pfa_factor_right_normal_prime. (p) = pfa_factor_left_normal_prime * pfa_factor_right_normal_prime -> pfa_factor_left_normal_prime = 1 \/ pfa_factor_right_normal_prime = 1) -> ((G)=0 \/ (((~((G) = 0)) /\ (((forall fom_index_pfp_normal_G_moniccoefficients. (exists fom_gap_pfp_normal_G_moniccoefficients_index_bound. fom_gap_pfp_normal_G_moniccoefficients_index_bound + S (fom_index_pfp_normal_G_moniccoefficients) = G) -> exists fom_value_pfp_normal_G_moniccoefficients. ((((exists fom_beta_height_pfp_normal_G_moniccoefficients_entry. fom_beta_height_pfp_normal_G_moniccoefficients_entry + S (fom_value_pfp_normal_G_moniccoefficients) = S ((S (fom_index_pfp_normal_G_moniccoefficients)) * gc)) /\ exists fom_beta_quotient_pfp_normal_G_moniccoefficients_entry. gb = fom_beta_quotient_pfp_normal_G_moniccoefficients_entry * S ((S (fom_index_pfp_normal_G_moniccoefficients)) * gc) + (fom_value_pfp_normal_G_moniccoefficients))) /\ (exists fom_gap_pfp_normal_G_moniccoefficients_value_bound. fom_gap_pfp_normal_G_moniccoefficients_value_bound + S (fom_value_pfp_normal_G_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normal_G_monicleading. ff_h_pfp_normal_G_monicleading + S (1) = S ((S (0)) * gc)) /\ exists ff_q_pfp_normal_G_monicleading. gb = ff_q_pfp_normal_G_monicleading * S ((S (0)) * gc) + (1))))))))) -> ((H)=0 \/ (((~((H) = 0)) /\ (((forall fom_index_pfp_normal_H_moniccoefficients. (exists fom_gap_pfp_normal_H_moniccoefficients_index_bound. fom_gap_pfp_normal_H_moniccoefficients_index_bound + S (fom_index_pfp_normal_H_moniccoefficients) = H) -> exists fom_value_pfp_normal_H_moniccoefficients. ((((exists fom_beta_height_pfp_normal_H_moniccoefficients_entry. fom_beta_height_pfp_normal_H_moniccoefficients_entry + S (fom_value_pfp_normal_H_moniccoefficients) = S ((S (fom_index_pfp_normal_H_moniccoefficients)) * hc)) /\ exists fom_beta_quotient_pfp_normal_H_moniccoefficients_entry. hb = fom_beta_quotient_pfp_normal_H_moniccoefficients_entry * S ((S (fom_index_pfp_normal_H_moniccoefficients)) * hc) + (fom_value_pfp_normal_H_moniccoefficients))) /\ (exists fom_gap_pfp_normal_H_moniccoefficients_value_bound. fom_gap_pfp_normal_H_moniccoefficients_value_bound + S (fom_value_pfp_normal_H_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normal_H_monicleading. ff_h_pfp_normal_H_monicleading + S (1) = S ((S (0)) * hc)) /\ exists ff_q_pfp_normal_H_monicleading. hb = ff_q_pfp_normal_H_monicleading * S ((S (0)) * hc) + (1))))))))) -> (((forall fom_index_pfp_normal_GH_canonical. (exists fom_gap_pfp_normal_GH_canonical_index_bound. fom_gap_pfp_normal_GH_canonical_index_bound + S (fom_index_pfp_normal_GH_canonical) = H) -> exists fom_value_pfp_normal_GH_canonical. ((((exists fom_beta_height_pfp_normal_GH_canonical_entry. fom_beta_height_pfp_normal_GH_canonical_entry + S (fom_value_pfp_normal_GH_canonical) = S ((S (fom_index_pfp_normal_GH_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_normal_GH_canonical_entry. hb = fom_beta_quotient_pfp_normal_GH_canonical_entry * S ((S (fom_index_pfp_normal_GH_canonical)) * hc) + (fom_value_pfp_normal_GH_canonical))) /\ (exists fom_gap_pfp_normal_GH_canonical_value_bound. fom_gap_pfp_normal_GH_canonical_value_bound + S (fom_value_pfp_normal_GH_canonical) = p))) /\ ((exists pfgu_qb_normal_GH pfgu_qc_normal_GH pfgu_Q_normal_GH pfgu_pb_normal_GH pfgu_pc_normal_GH pfgu_P_normal_GH. ((((forall fom_index_pfp_normal_GH_productleft. (exists fom_gap_pfp_normal_GH_productleft_index_bound. fom_gap_pfp_normal_GH_productleft_index_bound + S (fom_index_pfp_normal_GH_productleft) = pfgu_Q_normal_GH) -> exists fom_value_pfp_normal_GH_productleft. ((((exists fom_beta_height_pfp_normal_GH_productleft_entry. fom_beta_height_pfp_normal_GH_productleft_entry + S (fom_value_pfp_normal_GH_productleft) = S ((S (fom_index_pfp_normal_GH_productleft)) * pfgu_qc_normal_GH)) /\ exists fom_beta_quotient_pfp_normal_GH_productleft_entry. pfgu_qb_normal_GH = fom_beta_quotient_pfp_normal_GH_productleft_entry * S ((S (fom_index_pfp_normal_GH_productleft)) * pfgu_qc_normal_GH) + (fom_value_pfp_normal_GH_productleft))) /\ (exists fom_gap_pfp_normal_GH_productleft_value_bound. fom_gap_pfp_normal_GH_productleft_value_bound + S (fom_value_pfp_normal_GH_productleft) = p))) /\ (((forall fom_index_pfp_normal_GH_productright. (exists fom_gap_pfp_normal_GH_productright_index_bound. fom_gap_pfp_normal_GH_productright_index_bound + S (fom_index_pfp_normal_GH_productright) = G) -> exists fom_value_pfp_normal_GH_productright. ((((exists fom_beta_height_pfp_normal_GH_productright_entry. fom_beta_height_pfp_normal_GH_productright_entry + S (fom_value_pfp_normal_GH_productright) = S ((S (fom_index_pfp_normal_GH_productright)) * gc)) /\ exists fom_beta_quotient_pfp_normal_GH_productright_entry. gb = fom_beta_quotient_pfp_normal_GH_productright_entry * S ((S (fom_index_pfp_normal_GH_productright)) * gc) + (fom_value_pfp_normal_GH_productright))) /\ (exists fom_gap_pfp_normal_GH_productright_value_bound. fom_gap_pfp_normal_GH_productright_value_bound + S (fom_value_pfp_normal_GH_productright) = p))) /\ (((((((pfgu_Q_normal_GH)=0 \/ (G)=0) /\ (((pfgu_P_normal_GH)=0)))) \/ (((~((pfgu_Q_normal_GH)=0)) /\ (((~((G)=0)) /\ (((pfgu_Q_normal_GH)+(G)=S (pfgu_P_normal_GH)))))))) /\ ((forall pfc_index_normal_GH_productcoefficients. (exists pfa_gap_normal_GH_productcoefficientsbound. pfa_gap_normal_GH_productcoefficientsbound + S (pfc_index_normal_GH_productcoefficients) = (pfgu_P_normal_GH)) -> exists pfc_value_normal_GH_productcoefficients. ((((exists ff_h_pfp_normal_GH_productcoefficientsentry. ff_h_pfp_normal_GH_productcoefficientsentry + S (pfc_value_normal_GH_productcoefficients) = S ((S (pfc_index_normal_GH_productcoefficients)) * pfgu_pc_normal_GH)) /\ exists ff_q_pfp_normal_GH_productcoefficientsentry. pfgu_pb_normal_GH = ff_q_pfp_normal_GH_productcoefficientsentry * S ((S (pfc_index_normal_GH_productcoefficients)) * pfgu_pc_normal_GH) + (pfc_value_normal_GH_productcoefficients))) /\ ((exists pfc_terms_code_normal_GH_productcoefficientscoefficient pfc_terms_scale_normal_GH_productcoefficientscoefficient pfc_natural_sum_normal_GH_productcoefficientscoefficient. ((forall pfc_index_normal_GH_productcoefficientscoefficientdiagonal. (exists pfa_gap_normal_GH_productcoefficientscoefficientdiagonalbound. pfa_gap_normal_GH_productcoefficientscoefficientdiagonalbound + S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal) = (S (pfc_index_normal_GH_productcoefficients))) -> exists pfc_value_normal_GH_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonalentry + S (pfc_value_normal_GH_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normal_GH_productcoefficientscoefficient)) /\ exists ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normal_GH_productcoefficientscoefficient = ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normal_GH_productcoefficientscoefficient) + (pfc_value_normal_GH_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm. (((pfc_index_normal_GH_productcoefficientscoefficientdiagonal)+pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm=(pfc_index_normal_GH_productcoefficients)) /\ ((((((exists pfa_gap_normal_GH_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normal_GH_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal) = (pfgu_Q_normal_GH)) /\ ((((exists ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) * pfgu_qc_normal_GH)) /\ exists ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_normal_GH = ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) * pfgu_qc_normal_GH) + (pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normal_GH_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normal_GH_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_normal_GH)=(pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normal_GH_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normal_GH_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normal_GH_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normal_GH_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normal_GH_productcoefficientscoefficientdiagonal)=pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm*pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normal_GH_productcoefficientscoefficientsum fs_v_pfc_normal_GH_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_start. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_start. fs_u_pfc_normal_GH_productcoefficientscoefficientsum = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normal_GH_productcoefficientscoefficient) = S ((S (S (pfc_index_normal_GH_productcoefficients))) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normal_GH_productcoefficientscoefficientsum = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normal_GH_productcoefficients))) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum) + (pfc_natural_sum_normal_GH_productcoefficientscoefficient))) /\ forall fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps = S (pfc_index_normal_GH_productcoefficients)) -> exists fs_a_pfc_normal_GH_productcoefficientscoefficientsum_body_steps fs_r_pfc_normal_GH_productcoefficientscoefficientsum_body_steps fs_s_pfc_normal_GH_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normal_GH_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normal_GH_productcoefficientscoefficient)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normal_GH_productcoefficientscoefficient = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normal_GH_productcoefficientscoefficient) + (fs_a_pfc_normal_GH_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normal_GH_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normal_GH_productcoefficientscoefficientsum = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum) + (fs_r_pfc_normal_GH_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normal_GH_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normal_GH_productcoefficientscoefficientsum = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum) + (fs_s_pfc_normal_GH_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normal_GH_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normal_GH_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normal_GH_productcoefficientscoefficientresiduebound. pfa_gap_normal_GH_productcoefficientscoefficientresiduebound + S (pfc_value_normal_GH_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normal_GH_productcoefficientscoefficientresiduecongruence pfa_offset_right_normal_GH_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normal_GH_productcoefficientscoefficient) + (p) * pfa_offset_left_normal_GH_productcoefficientscoefficientresiduecongruence = (pfc_value_normal_GH_productcoefficients) + (p) * pfa_offset_right_normal_GH_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normal_GH_target pfrep_left_normal_GH_target pfrep_right_normal_GH_target. ((exists pfrep_position_normal_GH_targetfirst. ((pfrep_position_normal_GH_targetfirst+S (pfrep_power_normal_GH_target)=(pfgu_P_normal_GH)) /\ ((((exists ff_h_pfp_normal_GH_targetfirstentry. ff_h_pfp_normal_GH_targetfirstentry + S (pfrep_left_normal_GH_target) = S ((S (pfrep_position_normal_GH_targetfirst)) * pfgu_pc_normal_GH)) /\ exists ff_q_pfp_normal_GH_targetfirstentry. pfgu_pb_normal_GH = ff_q_pfp_normal_GH_targetfirstentry * S ((S (pfrep_position_normal_GH_targetfirst)) * pfgu_pc_normal_GH) + (pfrep_left_normal_GH_target)))))) \/ (((exists pfrep_gap_normal_GH_targetfirstoutside. pfrep_gap_normal_GH_targetfirstoutside+(pfgu_P_normal_GH)=(pfrep_power_normal_GH_target)) /\ (((pfrep_left_normal_GH_target)=0))))) -> ((exists pfrep_position_normal_GH_targetsecond. ((pfrep_position_normal_GH_targetsecond+S (pfrep_power_normal_GH_target)=(H)) /\ ((((exists ff_h_pfp_normal_GH_targetsecondentry. ff_h_pfp_normal_GH_targetsecondentry + S (pfrep_right_normal_GH_target) = S ((S (pfrep_position_normal_GH_targetsecond)) * hc)) /\ exists ff_q_pfp_normal_GH_targetsecondentry. hb = ff_q_pfp_normal_GH_targetsecondentry * S ((S (pfrep_position_normal_GH_targetsecond)) * hc) + (pfrep_right_normal_GH_target)))))) \/ (((exists pfrep_gap_normal_GH_targetsecondoutside. pfrep_gap_normal_GH_targetsecondoutside+(H)=(pfrep_power_normal_GH_target)) /\ (((pfrep_right_normal_GH_target)=0))))) -> pfrep_left_normal_GH_target=pfrep_right_normal_GH_target))))))) -> (((forall fom_index_pfp_normal_HG_canonical. (exists fom_gap_pfp_normal_HG_canonical_index_bound. fom_gap_pfp_normal_HG_canonical_index_bound + S (fom_index_pfp_normal_HG_canonical) = G) -> exists fom_value_pfp_normal_HG_canonical. ((((exists fom_beta_height_pfp_normal_HG_canonical_entry. fom_beta_height_pfp_normal_HG_canonical_entry + S (fom_value_pfp_normal_HG_canonical) = S ((S (fom_index_pfp_normal_HG_canonical)) * gc)) /\ exists fom_beta_quotient_pfp_normal_HG_canonical_entry. gb = fom_beta_quotient_pfp_normal_HG_canonical_entry * S ((S (fom_index_pfp_normal_HG_canonical)) * gc) + (fom_value_pfp_normal_HG_canonical))) /\ (exists fom_gap_pfp_normal_HG_canonical_value_bound. fom_gap_pfp_normal_HG_canonical_value_bound + S (fom_value_pfp_normal_HG_canonical) = p))) /\ ((exists pfgu_qb_normal_HG pfgu_qc_normal_HG pfgu_Q_normal_HG pfgu_pb_normal_HG pfgu_pc_normal_HG pfgu_P_normal_HG. ((((forall fom_index_pfp_normal_HG_productleft. (exists fom_gap_pfp_normal_HG_productleft_index_bound. fom_gap_pfp_normal_HG_productleft_index_bound + S (fom_index_pfp_normal_HG_productleft) = pfgu_Q_normal_HG) -> exists fom_value_pfp_normal_HG_productleft. ((((exists fom_beta_height_pfp_normal_HG_productleft_entry. fom_beta_height_pfp_normal_HG_productleft_entry + S (fom_value_pfp_normal_HG_productleft) = S ((S (fom_index_pfp_normal_HG_productleft)) * pfgu_qc_normal_HG)) /\ exists fom_beta_quotient_pfp_normal_HG_productleft_entry. pfgu_qb_normal_HG = fom_beta_quotient_pfp_normal_HG_productleft_entry * S ((S (fom_index_pfp_normal_HG_productleft)) * pfgu_qc_normal_HG) + (fom_value_pfp_normal_HG_productleft))) /\ (exists fom_gap_pfp_normal_HG_productleft_value_bound. fom_gap_pfp_normal_HG_productleft_value_bound + S (fom_value_pfp_normal_HG_productleft) = p))) /\ (((forall fom_index_pfp_normal_HG_productright. (exists fom_gap_pfp_normal_HG_productright_index_bound. fom_gap_pfp_normal_HG_productright_index_bound + S (fom_index_pfp_normal_HG_productright) = H) -> exists fom_value_pfp_normal_HG_productright. ((((exists fom_beta_height_pfp_normal_HG_productright_entry. fom_beta_height_pfp_normal_HG_productright_entry + S (fom_value_pfp_normal_HG_productright) = S ((S (fom_index_pfp_normal_HG_productright)) * hc)) /\ exists fom_beta_quotient_pfp_normal_HG_productright_entry. hb = fom_beta_quotient_pfp_normal_HG_productright_entry * S ((S (fom_index_pfp_normal_HG_productright)) * hc) + (fom_value_pfp_normal_HG_productright))) /\ (exists fom_gap_pfp_normal_HG_productright_value_bound. fom_gap_pfp_normal_HG_productright_value_bound + S (fom_value_pfp_normal_HG_productright) = p))) /\ (((((((pfgu_Q_normal_HG)=0 \/ (H)=0) /\ (((pfgu_P_normal_HG)=0)))) \/ (((~((pfgu_Q_normal_HG)=0)) /\ (((~((H)=0)) /\ (((pfgu_Q_normal_HG)+(H)=S (pfgu_P_normal_HG)))))))) /\ ((forall pfc_index_normal_HG_productcoefficients. (exists pfa_gap_normal_HG_productcoefficientsbound. pfa_gap_normal_HG_productcoefficientsbound + S (pfc_index_normal_HG_productcoefficients) = (pfgu_P_normal_HG)) -> exists pfc_value_normal_HG_productcoefficients. ((((exists ff_h_pfp_normal_HG_productcoefficientsentry. ff_h_pfp_normal_HG_productcoefficientsentry + S (pfc_value_normal_HG_productcoefficients) = S ((S (pfc_index_normal_HG_productcoefficients)) * pfgu_pc_normal_HG)) /\ exists ff_q_pfp_normal_HG_productcoefficientsentry. pfgu_pb_normal_HG = ff_q_pfp_normal_HG_productcoefficientsentry * S ((S (pfc_index_normal_HG_productcoefficients)) * pfgu_pc_normal_HG) + (pfc_value_normal_HG_productcoefficients))) /\ ((exists pfc_terms_code_normal_HG_productcoefficientscoefficient pfc_terms_scale_normal_HG_productcoefficientscoefficient pfc_natural_sum_normal_HG_productcoefficientscoefficient. ((forall pfc_index_normal_HG_productcoefficientscoefficientdiagonal. (exists pfa_gap_normal_HG_productcoefficientscoefficientdiagonalbound. pfa_gap_normal_HG_productcoefficientscoefficientdiagonalbound + S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal) = (S (pfc_index_normal_HG_productcoefficients))) -> exists pfc_value_normal_HG_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonalentry + S (pfc_value_normal_HG_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normal_HG_productcoefficientscoefficient)) /\ exists ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normal_HG_productcoefficientscoefficient = ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normal_HG_productcoefficientscoefficient) + (pfc_value_normal_HG_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm. (((pfc_index_normal_HG_productcoefficientscoefficientdiagonal)+pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm=(pfc_index_normal_HG_productcoefficients)) /\ ((((((exists pfa_gap_normal_HG_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normal_HG_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal) = (pfgu_Q_normal_HG)) /\ ((((exists ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) * pfgu_qc_normal_HG)) /\ exists ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_normal_HG = ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) * pfgu_qc_normal_HG) + (pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normal_HG_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normal_HG_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_normal_HG)=(pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normal_HG_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normal_HG_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normal_HG_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normal_HG_productcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normal_HG_productcoefficientscoefficientdiagonal)=pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm*pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normal_HG_productcoefficientscoefficientsum fs_v_pfc_normal_HG_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_start. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_start. fs_u_pfc_normal_HG_productcoefficientscoefficientsum = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normal_HG_productcoefficientscoefficient) = S ((S (S (pfc_index_normal_HG_productcoefficients))) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normal_HG_productcoefficientscoefficientsum = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normal_HG_productcoefficients))) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum) + (pfc_natural_sum_normal_HG_productcoefficientscoefficient))) /\ forall fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps = S (pfc_index_normal_HG_productcoefficients)) -> exists fs_a_pfc_normal_HG_productcoefficientscoefficientsum_body_steps fs_r_pfc_normal_HG_productcoefficientscoefficientsum_body_steps fs_s_pfc_normal_HG_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normal_HG_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normal_HG_productcoefficientscoefficient)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normal_HG_productcoefficientscoefficient = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normal_HG_productcoefficientscoefficient) + (fs_a_pfc_normal_HG_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normal_HG_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normal_HG_productcoefficientscoefficientsum = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum) + (fs_r_pfc_normal_HG_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normal_HG_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normal_HG_productcoefficientscoefficientsum = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum) + (fs_s_pfc_normal_HG_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normal_HG_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normal_HG_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normal_HG_productcoefficientscoefficientresiduebound. pfa_gap_normal_HG_productcoefficientscoefficientresiduebound + S (pfc_value_normal_HG_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normal_HG_productcoefficientscoefficientresiduecongruence pfa_offset_right_normal_HG_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normal_HG_productcoefficientscoefficient) + (p) * pfa_offset_left_normal_HG_productcoefficientscoefficientresiduecongruence = (pfc_value_normal_HG_productcoefficients) + (p) * pfa_offset_right_normal_HG_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normal_HG_target pfrep_left_normal_HG_target pfrep_right_normal_HG_target. ((exists pfrep_position_normal_HG_targetfirst. ((pfrep_position_normal_HG_targetfirst+S (pfrep_power_normal_HG_target)=(pfgu_P_normal_HG)) /\ ((((exists ff_h_pfp_normal_HG_targetfirstentry. ff_h_pfp_normal_HG_targetfirstentry + S (pfrep_left_normal_HG_target) = S ((S (pfrep_position_normal_HG_targetfirst)) * pfgu_pc_normal_HG)) /\ exists ff_q_pfp_normal_HG_targetfirstentry. pfgu_pb_normal_HG = ff_q_pfp_normal_HG_targetfirstentry * S ((S (pfrep_position_normal_HG_targetfirst)) * pfgu_pc_normal_HG) + (pfrep_left_normal_HG_target)))))) \/ (((exists pfrep_gap_normal_HG_targetfirstoutside. pfrep_gap_normal_HG_targetfirstoutside+(pfgu_P_normal_HG)=(pfrep_power_normal_HG_target)) /\ (((pfrep_left_normal_HG_target)=0))))) -> ((exists pfrep_position_normal_HG_targetsecond. ((pfrep_position_normal_HG_targetsecond+S (pfrep_power_normal_HG_target)=(G)) /\ ((((exists ff_h_pfp_normal_HG_targetsecondentry. ff_h_pfp_normal_HG_targetsecondentry + S (pfrep_right_normal_HG_target) = S ((S (pfrep_position_normal_HG_targetsecond)) * gc)) /\ exists ff_q_pfp_normal_HG_targetsecondentry. gb = ff_q_pfp_normal_HG_targetsecondentry * S ((S (pfrep_position_normal_HG_targetsecond)) * gc) + (pfrep_right_normal_HG_target)))))) \/ (((exists pfrep_gap_normal_HG_targetsecondoutside. pfrep_gap_normal_HG_targetsecondoutside+(G)=(pfrep_power_normal_HG_target)) /\ (((pfrep_right_normal_HG_target)=0))))) -> pfrep_left_normal_HG_target=pfrep_right_normal_HG_target))))))) -> (forall pfrep_power_normal_result pfrep_left_normal_result pfrep_right_normal_result. ((exists pfrep_position_normal_resultfirst. ((pfrep_position_normal_resultfirst+S (pfrep_power_normal_result)=(G)) /\ ((((exists ff_h_pfp_normal_resultfirstentry. ff_h_pfp_normal_resultfirstentry + S (pfrep_left_normal_result) = S ((S (pfrep_position_normal_resultfirst)) * gc)) /\ exists ff_q_pfp_normal_resultfirstentry. gb = ff_q_pfp_normal_resultfirstentry * S ((S (pfrep_position_normal_resultfirst)) * gc) + (pfrep_left_normal_result)))))) \/ (((exists pfrep_gap_normal_resultfirstoutside. pfrep_gap_normal_resultfirstoutside+(G)=(pfrep_power_normal_result)) /\ (((pfrep_left_normal_result)=0))))) -> ((exists pfrep_position_normal_resultsecond. ((pfrep_position_normal_resultsecond+S (pfrep_power_normal_result)=(H)) /\ ((((exists ff_h_pfp_normal_resultsecondentry. ff_h_pfp_normal_resultsecondentry + S (pfrep_right_normal_result) = S ((S (pfrep_position_normal_resultsecond)) * hc)) /\ exists ff_q_pfp_normal_resultsecondentry. hb = ff_q_pfp_normal_resultsecondentry * S ((S (pfrep_position_normal_resultsecond)) * hc) + (pfrep_right_normal_result)))))) \/ (((exists pfrep_gap_normal_resultsecondoutside. pfrep_gap_normal_resultsecondoutside+(H)=(pfrep_power_normal_result)) /\ (((pfrep_right_normal_result)=0))))) -> pfrep_left_normal_result=pfrep_right_normal_result)

Complete tactic proof in conservative notation

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

70 script commands · 13 reading checkpoints · 2 local claims

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

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

Named ingredients (2)
prime field polynomial empty right divisor implies equivalent zeroprime field polynomial monic right associates equivalent
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro gb
  3. L3
    intro gc
  4. L4
    intro G
  5. L5
    intro hb
  6. L6
    intro hc
  7. L7
    intro H
  8. L8
    intro hp
  9. L9
    intro hg
  10. L10
    intro hh
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hgh
  2. L12
    intro hhg
03Separate the logical casesL13–13

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

  1. L13
    cases hg
04Calculate and transport equalitiesL14–15

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

  1. L14
    rewrite hg_left
  2. L15
    rewrite hg_left
05Use earlier factsL16–25

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

  1. L16
    specialize prime_field_polynomial_equivalent_symmetric (hb)
  2. L17
    specialize prime_field_polynomial_equivalent_symmetric (hc)
  3. L18
    specialize prime_field_polynomial_equivalent_symmetric (H)
  4. L19
    specialize prime_field_polynomial_equivalent_symmetric (gb)
  5. L20
    specialize prime_field_polynomial_equivalent_symmetric (gc)
  6. L21
    specialize prime_field_polynomial_equivalent_symmetric (0)
  7. L22
    apply prime_field_polynomial_equivalent_symmetric
  8. L23
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (p)
  9. L24
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (gb)
  10. L25
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (gc)
06Use earlier factsL26–29

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

  1. L26
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (hb)
  2. L27
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (hc)
  3. L28
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (H)
  4. L29
    apply prime_field_polynomial_empty_right_divisor_implies_equivalent_zero
07Establish hcopyL30–38

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

  1. L30
    have hcopy : FpPolynomialRightDivides(p,gb,gc,G,hb,hc,H)Definitions: FpPolynomialRightDivides(p,gb,gc,G,hb,hc,H)Original native command in the exact edition
  2. L31
    exact hgh
  3. L32
    rewrite hg_left at hcopy
  4. L33
    rewrite hg_left at hcopy
  5. L34
    rewrite hg_left at hcopy
  6. L35
    rewrite hg_left at hcopy
  7. L36
    rewrite hg_left at hcopy
  8. L37
    rewrite hg_left at hcopy
  9. L38
    exact hcopy
08Separate the logical casesL39–39

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

  1. L39
    cases hh
09Calculate and transport equalitiesL40–41

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

  1. L40
    rewrite hh_left
  2. L41
    rewrite hh_left
10Use earlier factsL42–48

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

  1. L42
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (p)
  2. L43
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (hb)
  3. L44
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (hc)
  4. L45
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (gb)
  5. L46
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (gc)
  6. L47
    specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (G)
  7. L48
    apply prime_field_polynomial_empty_right_divisor_implies_equivalent_zero
11Establish hcopyL49–58

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

  1. L49
    have hcopy : FpPolynomialRightDivides(p,hb,hc,H,gb,gc,G)Definitions: FpPolynomialRightDivides(p,hb,hc,H,gb,gc,G)Original native command in the exact edition
  2. L50
    exact hhg
  3. L51
    rewrite hh_left at hcopy
  4. L52
    rewrite hh_left at hcopy
  5. L53
    rewrite hh_left at hcopy
  6. L54
    rewrite hh_left at hcopy
  7. L55
    rewrite hh_left at hcopy
  8. L56
    rewrite hh_left at hcopy
  9. L57
    exact hcopy
  10. L58
    specialize prime_field_polynomial_monic_right_associates_equivalent (p)
12Use earlier factsL59–68

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

  1. L59
    specialize prime_field_polynomial_monic_right_associates_equivalent (gb)
  2. L60
    specialize prime_field_polynomial_monic_right_associates_equivalent (gc)
  3. L61
    specialize prime_field_polynomial_monic_right_associates_equivalent (G)
  4. L62
    specialize prime_field_polynomial_monic_right_associates_equivalent (hb)
  5. L63
    specialize prime_field_polynomial_monic_right_associates_equivalent (hc)
  6. L64
    specialize prime_field_polynomial_monic_right_associates_equivalent (H)
  7. L65
    apply prime_field_polynomial_monic_right_associates_equivalent
  8. L66
    exact hp
  9. L67
    exact hg_right
  10. L68
    exact hh_right
13Use earlier factsL69–70

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

  1. L69
    exact hgh
  2. L70
    exact hhg

Library-wide reading audit

Original defined command ledger · 70 lines
  1. 0001intro p
  2. 0002intro gb
  3. 0003intro gc
  4. 0004intro G
  5. 0005intro hb
  6. 0006intro hc
  7. 0007intro H
  8. 0008intro hp
  9. 0009intro hg
  10. 0010intro hh
  11. 0011intro hgh
  12. 0012intro hhg
  13. 0013cases hg
  14. 0014rewrite hg_left
  15. 0015rewrite hg_left
  16. 0016specialize prime_field_polynomial_equivalent_symmetric (hb)
  17. 0017specialize prime_field_polynomial_equivalent_symmetric (hc)
  18. 0018specialize prime_field_polynomial_equivalent_symmetric (H)
  19. 0019specialize prime_field_polynomial_equivalent_symmetric (gb)
  20. 0020specialize prime_field_polynomial_equivalent_symmetric (gc)
  21. 0021specialize prime_field_polynomial_equivalent_symmetric (0)
  22. 0022apply prime_field_polynomial_equivalent_symmetric
  23. 0023specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (p)
  24. 0024specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (gb)
  25. 0025specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (gc)
  26. 0026specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (hb)
  27. 0027specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (hc)
  28. 0028specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (H)
  29. 0029apply prime_field_polynomial_empty_right_divisor_implies_equivalent_zero
  30. 0030have hcopy : FpPolynomialRightDivides(p,gb,gc,G,hb,hc,H)
  31. 0031exact hgh
  32. 0032rewrite hg_left at hcopy
  33. 0033rewrite hg_left at hcopy
  34. 0034rewrite hg_left at hcopy
  35. 0035rewrite hg_left at hcopy
  36. 0036rewrite hg_left at hcopy
  37. 0037rewrite hg_left at hcopy
  38. 0038exact hcopy
  39. 0039cases hh
  40. 0040rewrite hh_left
  41. 0041rewrite hh_left
  42. 0042specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (p)
  43. 0043specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (hb)
  44. 0044specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (hc)
  45. 0045specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (gb)
  46. 0046specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (gc)
  47. 0047specialize prime_field_polynomial_empty_right_divisor_implies_equivalent_zero (G)
  48. 0048apply prime_field_polynomial_empty_right_divisor_implies_equivalent_zero
  49. 0049have hcopy : FpPolynomialRightDivides(p,hb,hc,H,gb,gc,G)
  50. 0050exact hhg
  51. 0051rewrite hh_left at hcopy
  52. 0052rewrite hh_left at hcopy
  53. 0053rewrite hh_left at hcopy
  54. 0054rewrite hh_left at hcopy
  55. 0055rewrite hh_left at hcopy
  56. 0056rewrite hh_left at hcopy
  57. 0057exact hcopy
  58. 0058specialize prime_field_polynomial_monic_right_associates_equivalent (p)
  59. 0059specialize prime_field_polynomial_monic_right_associates_equivalent (gb)
  60. 0060specialize prime_field_polynomial_monic_right_associates_equivalent (gc)
  61. 0061specialize prime_field_polynomial_monic_right_associates_equivalent (G)
  62. 0062specialize prime_field_polynomial_monic_right_associates_equivalent (hb)
  63. 0063specialize prime_field_polynomial_monic_right_associates_equivalent (hc)
  64. 0064specialize prime_field_polynomial_monic_right_associates_equivalent (H)
  65. 0065apply prime_field_polynomial_monic_right_associates_equivalent
  66. 0066exact hp
  67. 0067exact hg_right
  68. 0068exact hh_right
  69. 0069exact hgh
  70. 0070exact hhg