PG0074

prime_field_polynomial_monic_right_associates_equivalent

Mutual right divisibility forces equal represented degrees. Both actual monic normalizations then force formal coefficient equivalence, without selecting unique beta codes.

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) → FpMonic(p,gb,gc,G) → FpMonic(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

FpRepresentedDegree(p,b,c,L,d) · 2FpMonic(p,b,c,L) · 6PolynomialEquivalent(b,c,L,d,e,M) · 1FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 4Prime(p) · 1

Actual proof prerequisites

nonzero_is_succ · checked external prerequisiteprime_field_polynomial_monic_represented_degree · checked external prerequisitele_antisymm · checked external prerequisiteprime_field_polynomial_right_divides_represented_degree_boundprime_field_polynomial_monic_equal_degree_right_divides_equivalent
Original expanded first-order statement 
forall p gb gc G hb hc H. (~((p) = 1) /\ forall pfa_factor_left_associates_prime pfa_factor_right_associates_prime. (p) = pfa_factor_left_associates_prime * pfa_factor_right_associates_prime -> pfa_factor_left_associates_prime = 1 \/ pfa_factor_right_associates_prime = 1) -> (((~((G) = 0)) /\ (((forall fom_index_pfp_associates_Gcoefficients. (exists fom_gap_pfp_associates_Gcoefficients_index_bound. fom_gap_pfp_associates_Gcoefficients_index_bound + S (fom_index_pfp_associates_Gcoefficients) = G) -> exists fom_value_pfp_associates_Gcoefficients. ((((exists fom_beta_height_pfp_associates_Gcoefficients_entry. fom_beta_height_pfp_associates_Gcoefficients_entry + S (fom_value_pfp_associates_Gcoefficients) = S ((S (fom_index_pfp_associates_Gcoefficients)) * gc)) /\ exists fom_beta_quotient_pfp_associates_Gcoefficients_entry. gb = fom_beta_quotient_pfp_associates_Gcoefficients_entry * S ((S (fom_index_pfp_associates_Gcoefficients)) * gc) + (fom_value_pfp_associates_Gcoefficients))) /\ (exists fom_gap_pfp_associates_Gcoefficients_value_bound. fom_gap_pfp_associates_Gcoefficients_value_bound + S (fom_value_pfp_associates_Gcoefficients) = p))) /\ ((((exists ff_h_pfp_associates_Gleading. ff_h_pfp_associates_Gleading + S (1) = S ((S (0)) * gc)) /\ exists ff_q_pfp_associates_Gleading. gb = ff_q_pfp_associates_Gleading * S ((S (0)) * gc) + (1)))))))) -> (((~((H) = 0)) /\ (((forall fom_index_pfp_associates_Hcoefficients. (exists fom_gap_pfp_associates_Hcoefficients_index_bound. fom_gap_pfp_associates_Hcoefficients_index_bound + S (fom_index_pfp_associates_Hcoefficients) = H) -> exists fom_value_pfp_associates_Hcoefficients. ((((exists fom_beta_height_pfp_associates_Hcoefficients_entry. fom_beta_height_pfp_associates_Hcoefficients_entry + S (fom_value_pfp_associates_Hcoefficients) = S ((S (fom_index_pfp_associates_Hcoefficients)) * hc)) /\ exists fom_beta_quotient_pfp_associates_Hcoefficients_entry. hb = fom_beta_quotient_pfp_associates_Hcoefficients_entry * S ((S (fom_index_pfp_associates_Hcoefficients)) * hc) + (fom_value_pfp_associates_Hcoefficients))) /\ (exists fom_gap_pfp_associates_Hcoefficients_value_bound. fom_gap_pfp_associates_Hcoefficients_value_bound + S (fom_value_pfp_associates_Hcoefficients) = p))) /\ ((((exists ff_h_pfp_associates_Hleading. ff_h_pfp_associates_Hleading + S (1) = S ((S (0)) * hc)) /\ exists ff_q_pfp_associates_Hleading. hb = ff_q_pfp_associates_Hleading * S ((S (0)) * hc) + (1)))))))) -> (((forall fom_index_pfp_associates_GH_canonical. (exists fom_gap_pfp_associates_GH_canonical_index_bound. fom_gap_pfp_associates_GH_canonical_index_bound + S (fom_index_pfp_associates_GH_canonical) = H) -> exists fom_value_pfp_associates_GH_canonical. ((((exists fom_beta_height_pfp_associates_GH_canonical_entry. fom_beta_height_pfp_associates_GH_canonical_entry + S (fom_value_pfp_associates_GH_canonical) = S ((S (fom_index_pfp_associates_GH_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_associates_GH_canonical_entry. hb = fom_beta_quotient_pfp_associates_GH_canonical_entry * S ((S (fom_index_pfp_associates_GH_canonical)) * hc) + (fom_value_pfp_associates_GH_canonical))) /\ (exists fom_gap_pfp_associates_GH_canonical_value_bound. fom_gap_pfp_associates_GH_canonical_value_bound + S (fom_value_pfp_associates_GH_canonical) = p))) /\ ((exists pfgu_qb_associates_GH pfgu_qc_associates_GH pfgu_Q_associates_GH pfgu_pb_associates_GH pfgu_pc_associates_GH pfgu_P_associates_GH. ((((forall fom_index_pfp_associates_GH_productleft. (exists fom_gap_pfp_associates_GH_productleft_index_bound. fom_gap_pfp_associates_GH_productleft_index_bound + S (fom_index_pfp_associates_GH_productleft) = pfgu_Q_associates_GH) -> exists fom_value_pfp_associates_GH_productleft. ((((exists fom_beta_height_pfp_associates_GH_productleft_entry. fom_beta_height_pfp_associates_GH_productleft_entry + S (fom_value_pfp_associates_GH_productleft) = S ((S (fom_index_pfp_associates_GH_productleft)) * pfgu_qc_associates_GH)) /\ exists fom_beta_quotient_pfp_associates_GH_productleft_entry. pfgu_qb_associates_GH = fom_beta_quotient_pfp_associates_GH_productleft_entry * S ((S (fom_index_pfp_associates_GH_productleft)) * pfgu_qc_associates_GH) + (fom_value_pfp_associates_GH_productleft))) /\ (exists fom_gap_pfp_associates_GH_productleft_value_bound. fom_gap_pfp_associates_GH_productleft_value_bound + S (fom_value_pfp_associates_GH_productleft) = p))) /\ (((forall fom_index_pfp_associates_GH_productright. (exists fom_gap_pfp_associates_GH_productright_index_bound. fom_gap_pfp_associates_GH_productright_index_bound + S (fom_index_pfp_associates_GH_productright) = G) -> exists fom_value_pfp_associates_GH_productright. ((((exists fom_beta_height_pfp_associates_GH_productright_entry. fom_beta_height_pfp_associates_GH_productright_entry + S (fom_value_pfp_associates_GH_productright) = S ((S (fom_index_pfp_associates_GH_productright)) * gc)) /\ exists fom_beta_quotient_pfp_associates_GH_productright_entry. gb = fom_beta_quotient_pfp_associates_GH_productright_entry * S ((S (fom_index_pfp_associates_GH_productright)) * gc) + (fom_value_pfp_associates_GH_productright))) /\ (exists fom_gap_pfp_associates_GH_productright_value_bound. fom_gap_pfp_associates_GH_productright_value_bound + S (fom_value_pfp_associates_GH_productright) = p))) /\ (((((((pfgu_Q_associates_GH)=0 \/ (G)=0) /\ (((pfgu_P_associates_GH)=0)))) \/ (((~((pfgu_Q_associates_GH)=0)) /\ (((~((G)=0)) /\ (((pfgu_Q_associates_GH)+(G)=S (pfgu_P_associates_GH)))))))) /\ ((forall pfc_index_associates_GH_productcoefficients. (exists pfa_gap_associates_GH_productcoefficientsbound. pfa_gap_associates_GH_productcoefficientsbound + S (pfc_index_associates_GH_productcoefficients) = (pfgu_P_associates_GH)) -> exists pfc_value_associates_GH_productcoefficients. ((((exists ff_h_pfp_associates_GH_productcoefficientsentry. ff_h_pfp_associates_GH_productcoefficientsentry + S (pfc_value_associates_GH_productcoefficients) = S ((S (pfc_index_associates_GH_productcoefficients)) * pfgu_pc_associates_GH)) /\ exists ff_q_pfp_associates_GH_productcoefficientsentry. pfgu_pb_associates_GH = ff_q_pfp_associates_GH_productcoefficientsentry * S ((S (pfc_index_associates_GH_productcoefficients)) * pfgu_pc_associates_GH) + (pfc_value_associates_GH_productcoefficients))) /\ ((exists pfc_terms_code_associates_GH_productcoefficientscoefficient pfc_terms_scale_associates_GH_productcoefficientscoefficient pfc_natural_sum_associates_GH_productcoefficientscoefficient. ((forall pfc_index_associates_GH_productcoefficientscoefficientdiagonal. (exists pfa_gap_associates_GH_productcoefficientscoefficientdiagonalbound. pfa_gap_associates_GH_productcoefficientscoefficientdiagonalbound + S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal) = (S (pfc_index_associates_GH_productcoefficients))) -> exists pfc_value_associates_GH_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonalentry. ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonalentry + S (pfc_value_associates_GH_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_associates_GH_productcoefficientscoefficient)) /\ exists ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonalentry. pfc_terms_code_associates_GH_productcoefficientscoefficient = ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_associates_GH_productcoefficientscoefficient) + (pfc_value_associates_GH_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm. (((pfc_index_associates_GH_productcoefficientscoefficientdiagonal)+pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm=(pfc_index_associates_GH_productcoefficients)) /\ ((((((exists pfa_gap_associates_GH_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associates_GH_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal) = (pfgu_Q_associates_GH)) /\ ((((exists ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) * pfgu_qc_associates_GH)) /\ exists ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_associates_GH = ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) * pfgu_qc_associates_GH) + (pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associates_GH_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associates_GH_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_associates_GH)=(pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associates_GH_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associates_GH_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associates_GH_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associates_GH_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associates_GH_productcoefficientscoefficientdiagonal)=pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm*pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associates_GH_productcoefficientscoefficientsum fs_v_pfc_associates_GH_productcoefficientscoefficientsum. ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_start. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_start. fs_u_pfc_associates_GH_productcoefficientscoefficientsum = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associates_GH_productcoefficientscoefficient) = S ((S (S (pfc_index_associates_GH_productcoefficients))) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_associates_GH_productcoefficientscoefficientsum = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associates_GH_productcoefficients))) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum) + (pfc_natural_sum_associates_GH_productcoefficientscoefficient))) /\ forall fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps = S (pfc_index_associates_GH_productcoefficients)) -> exists fs_a_pfc_associates_GH_productcoefficientscoefficientsum_body_steps fs_r_pfc_associates_GH_productcoefficientscoefficientsum_body_steps fs_s_pfc_associates_GH_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associates_GH_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associates_GH_productcoefficientscoefficient)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associates_GH_productcoefficientscoefficient = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associates_GH_productcoefficientscoefficient) + (fs_a_pfc_associates_GH_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associates_GH_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associates_GH_productcoefficientscoefficientsum = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum) + (fs_r_pfc_associates_GH_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associates_GH_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associates_GH_productcoefficientscoefficientsum = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum) + (fs_s_pfc_associates_GH_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associates_GH_productcoefficientscoefficientsum_body_steps = fs_r_pfc_associates_GH_productcoefficientscoefficientsum_body_steps + fs_a_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associates_GH_productcoefficientscoefficientresiduebound. pfa_gap_associates_GH_productcoefficientscoefficientresiduebound + S (pfc_value_associates_GH_productcoefficients) = (p)) /\ ((exists pfa_offset_left_associates_GH_productcoefficientscoefficientresiduecongruence pfa_offset_right_associates_GH_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associates_GH_productcoefficientscoefficient) + (p) * pfa_offset_left_associates_GH_productcoefficientscoefficientresiduecongruence = (pfc_value_associates_GH_productcoefficients) + (p) * pfa_offset_right_associates_GH_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_associates_GH_target pfrep_left_associates_GH_target pfrep_right_associates_GH_target. ((exists pfrep_position_associates_GH_targetfirst. ((pfrep_position_associates_GH_targetfirst+S (pfrep_power_associates_GH_target)=(pfgu_P_associates_GH)) /\ ((((exists ff_h_pfp_associates_GH_targetfirstentry. ff_h_pfp_associates_GH_targetfirstentry + S (pfrep_left_associates_GH_target) = S ((S (pfrep_position_associates_GH_targetfirst)) * pfgu_pc_associates_GH)) /\ exists ff_q_pfp_associates_GH_targetfirstentry. pfgu_pb_associates_GH = ff_q_pfp_associates_GH_targetfirstentry * S ((S (pfrep_position_associates_GH_targetfirst)) * pfgu_pc_associates_GH) + (pfrep_left_associates_GH_target)))))) \/ (((exists pfrep_gap_associates_GH_targetfirstoutside. pfrep_gap_associates_GH_targetfirstoutside+(pfgu_P_associates_GH)=(pfrep_power_associates_GH_target)) /\ (((pfrep_left_associates_GH_target)=0))))) -> ((exists pfrep_position_associates_GH_targetsecond. ((pfrep_position_associates_GH_targetsecond+S (pfrep_power_associates_GH_target)=(H)) /\ ((((exists ff_h_pfp_associates_GH_targetsecondentry. ff_h_pfp_associates_GH_targetsecondentry + S (pfrep_right_associates_GH_target) = S ((S (pfrep_position_associates_GH_targetsecond)) * hc)) /\ exists ff_q_pfp_associates_GH_targetsecondentry. hb = ff_q_pfp_associates_GH_targetsecondentry * S ((S (pfrep_position_associates_GH_targetsecond)) * hc) + (pfrep_right_associates_GH_target)))))) \/ (((exists pfrep_gap_associates_GH_targetsecondoutside. pfrep_gap_associates_GH_targetsecondoutside+(H)=(pfrep_power_associates_GH_target)) /\ (((pfrep_right_associates_GH_target)=0))))) -> pfrep_left_associates_GH_target=pfrep_right_associates_GH_target))))))) -> (((forall fom_index_pfp_associates_HG_canonical. (exists fom_gap_pfp_associates_HG_canonical_index_bound. fom_gap_pfp_associates_HG_canonical_index_bound + S (fom_index_pfp_associates_HG_canonical) = G) -> exists fom_value_pfp_associates_HG_canonical. ((((exists fom_beta_height_pfp_associates_HG_canonical_entry. fom_beta_height_pfp_associates_HG_canonical_entry + S (fom_value_pfp_associates_HG_canonical) = S ((S (fom_index_pfp_associates_HG_canonical)) * gc)) /\ exists fom_beta_quotient_pfp_associates_HG_canonical_entry. gb = fom_beta_quotient_pfp_associates_HG_canonical_entry * S ((S (fom_index_pfp_associates_HG_canonical)) * gc) + (fom_value_pfp_associates_HG_canonical))) /\ (exists fom_gap_pfp_associates_HG_canonical_value_bound. fom_gap_pfp_associates_HG_canonical_value_bound + S (fom_value_pfp_associates_HG_canonical) = p))) /\ ((exists pfgu_qb_associates_HG pfgu_qc_associates_HG pfgu_Q_associates_HG pfgu_pb_associates_HG pfgu_pc_associates_HG pfgu_P_associates_HG. ((((forall fom_index_pfp_associates_HG_productleft. (exists fom_gap_pfp_associates_HG_productleft_index_bound. fom_gap_pfp_associates_HG_productleft_index_bound + S (fom_index_pfp_associates_HG_productleft) = pfgu_Q_associates_HG) -> exists fom_value_pfp_associates_HG_productleft. ((((exists fom_beta_height_pfp_associates_HG_productleft_entry. fom_beta_height_pfp_associates_HG_productleft_entry + S (fom_value_pfp_associates_HG_productleft) = S ((S (fom_index_pfp_associates_HG_productleft)) * pfgu_qc_associates_HG)) /\ exists fom_beta_quotient_pfp_associates_HG_productleft_entry. pfgu_qb_associates_HG = fom_beta_quotient_pfp_associates_HG_productleft_entry * S ((S (fom_index_pfp_associates_HG_productleft)) * pfgu_qc_associates_HG) + (fom_value_pfp_associates_HG_productleft))) /\ (exists fom_gap_pfp_associates_HG_productleft_value_bound. fom_gap_pfp_associates_HG_productleft_value_bound + S (fom_value_pfp_associates_HG_productleft) = p))) /\ (((forall fom_index_pfp_associates_HG_productright. (exists fom_gap_pfp_associates_HG_productright_index_bound. fom_gap_pfp_associates_HG_productright_index_bound + S (fom_index_pfp_associates_HG_productright) = H) -> exists fom_value_pfp_associates_HG_productright. ((((exists fom_beta_height_pfp_associates_HG_productright_entry. fom_beta_height_pfp_associates_HG_productright_entry + S (fom_value_pfp_associates_HG_productright) = S ((S (fom_index_pfp_associates_HG_productright)) * hc)) /\ exists fom_beta_quotient_pfp_associates_HG_productright_entry. hb = fom_beta_quotient_pfp_associates_HG_productright_entry * S ((S (fom_index_pfp_associates_HG_productright)) * hc) + (fom_value_pfp_associates_HG_productright))) /\ (exists fom_gap_pfp_associates_HG_productright_value_bound. fom_gap_pfp_associates_HG_productright_value_bound + S (fom_value_pfp_associates_HG_productright) = p))) /\ (((((((pfgu_Q_associates_HG)=0 \/ (H)=0) /\ (((pfgu_P_associates_HG)=0)))) \/ (((~((pfgu_Q_associates_HG)=0)) /\ (((~((H)=0)) /\ (((pfgu_Q_associates_HG)+(H)=S (pfgu_P_associates_HG)))))))) /\ ((forall pfc_index_associates_HG_productcoefficients. (exists pfa_gap_associates_HG_productcoefficientsbound. pfa_gap_associates_HG_productcoefficientsbound + S (pfc_index_associates_HG_productcoefficients) = (pfgu_P_associates_HG)) -> exists pfc_value_associates_HG_productcoefficients. ((((exists ff_h_pfp_associates_HG_productcoefficientsentry. ff_h_pfp_associates_HG_productcoefficientsentry + S (pfc_value_associates_HG_productcoefficients) = S ((S (pfc_index_associates_HG_productcoefficients)) * pfgu_pc_associates_HG)) /\ exists ff_q_pfp_associates_HG_productcoefficientsentry. pfgu_pb_associates_HG = ff_q_pfp_associates_HG_productcoefficientsentry * S ((S (pfc_index_associates_HG_productcoefficients)) * pfgu_pc_associates_HG) + (pfc_value_associates_HG_productcoefficients))) /\ ((exists pfc_terms_code_associates_HG_productcoefficientscoefficient pfc_terms_scale_associates_HG_productcoefficientscoefficient pfc_natural_sum_associates_HG_productcoefficientscoefficient. ((forall pfc_index_associates_HG_productcoefficientscoefficientdiagonal. (exists pfa_gap_associates_HG_productcoefficientscoefficientdiagonalbound. pfa_gap_associates_HG_productcoefficientscoefficientdiagonalbound + S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal) = (S (pfc_index_associates_HG_productcoefficients))) -> exists pfc_value_associates_HG_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonalentry. ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonalentry + S (pfc_value_associates_HG_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_associates_HG_productcoefficientscoefficient)) /\ exists ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonalentry. pfc_terms_code_associates_HG_productcoefficientscoefficient = ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_associates_HG_productcoefficientscoefficient) + (pfc_value_associates_HG_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm. (((pfc_index_associates_HG_productcoefficientscoefficientdiagonal)+pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm=(pfc_index_associates_HG_productcoefficients)) /\ ((((((exists pfa_gap_associates_HG_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associates_HG_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal) = (pfgu_Q_associates_HG)) /\ ((((exists ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) * pfgu_qc_associates_HG)) /\ exists ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_associates_HG = ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) * pfgu_qc_associates_HG) + (pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associates_HG_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associates_HG_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_associates_HG)=(pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associates_HG_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associates_HG_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associates_HG_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associates_HG_productcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associates_HG_productcoefficientscoefficientdiagonal)=pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm*pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associates_HG_productcoefficientscoefficientsum fs_v_pfc_associates_HG_productcoefficientscoefficientsum. ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_start. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_start. fs_u_pfc_associates_HG_productcoefficientscoefficientsum = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associates_HG_productcoefficientscoefficient) = S ((S (S (pfc_index_associates_HG_productcoefficients))) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_associates_HG_productcoefficientscoefficientsum = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associates_HG_productcoefficients))) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum) + (pfc_natural_sum_associates_HG_productcoefficientscoefficient))) /\ forall fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps = S (pfc_index_associates_HG_productcoefficients)) -> exists fs_a_pfc_associates_HG_productcoefficientscoefficientsum_body_steps fs_r_pfc_associates_HG_productcoefficientscoefficientsum_body_steps fs_s_pfc_associates_HG_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associates_HG_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associates_HG_productcoefficientscoefficient)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associates_HG_productcoefficientscoefficient = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associates_HG_productcoefficientscoefficient) + (fs_a_pfc_associates_HG_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associates_HG_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associates_HG_productcoefficientscoefficientsum = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum) + (fs_r_pfc_associates_HG_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associates_HG_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associates_HG_productcoefficientscoefficientsum = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum) + (fs_s_pfc_associates_HG_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associates_HG_productcoefficientscoefficientsum_body_steps = fs_r_pfc_associates_HG_productcoefficientscoefficientsum_body_steps + fs_a_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associates_HG_productcoefficientscoefficientresiduebound. pfa_gap_associates_HG_productcoefficientscoefficientresiduebound + S (pfc_value_associates_HG_productcoefficients) = (p)) /\ ((exists pfa_offset_left_associates_HG_productcoefficientscoefficientresiduecongruence pfa_offset_right_associates_HG_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associates_HG_productcoefficientscoefficient) + (p) * pfa_offset_left_associates_HG_productcoefficientscoefficientresiduecongruence = (pfc_value_associates_HG_productcoefficients) + (p) * pfa_offset_right_associates_HG_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_associates_HG_target pfrep_left_associates_HG_target pfrep_right_associates_HG_target. ((exists pfrep_position_associates_HG_targetfirst. ((pfrep_position_associates_HG_targetfirst+S (pfrep_power_associates_HG_target)=(pfgu_P_associates_HG)) /\ ((((exists ff_h_pfp_associates_HG_targetfirstentry. ff_h_pfp_associates_HG_targetfirstentry + S (pfrep_left_associates_HG_target) = S ((S (pfrep_position_associates_HG_targetfirst)) * pfgu_pc_associates_HG)) /\ exists ff_q_pfp_associates_HG_targetfirstentry. pfgu_pb_associates_HG = ff_q_pfp_associates_HG_targetfirstentry * S ((S (pfrep_position_associates_HG_targetfirst)) * pfgu_pc_associates_HG) + (pfrep_left_associates_HG_target)))))) \/ (((exists pfrep_gap_associates_HG_targetfirstoutside. pfrep_gap_associates_HG_targetfirstoutside+(pfgu_P_associates_HG)=(pfrep_power_associates_HG_target)) /\ (((pfrep_left_associates_HG_target)=0))))) -> ((exists pfrep_position_associates_HG_targetsecond. ((pfrep_position_associates_HG_targetsecond+S (pfrep_power_associates_HG_target)=(G)) /\ ((((exists ff_h_pfp_associates_HG_targetsecondentry. ff_h_pfp_associates_HG_targetsecondentry + S (pfrep_right_associates_HG_target) = S ((S (pfrep_position_associates_HG_targetsecond)) * gc)) /\ exists ff_q_pfp_associates_HG_targetsecondentry. gb = ff_q_pfp_associates_HG_targetsecondentry * S ((S (pfrep_position_associates_HG_targetsecond)) * gc) + (pfrep_right_associates_HG_target)))))) \/ (((exists pfrep_gap_associates_HG_targetsecondoutside. pfrep_gap_associates_HG_targetsecondoutside+(G)=(pfrep_power_associates_HG_target)) /\ (((pfrep_right_associates_HG_target)=0))))) -> pfrep_left_associates_HG_target=pfrep_right_associates_HG_target))))))) -> (forall pfrep_power_associates_result pfrep_left_associates_result pfrep_right_associates_result. ((exists pfrep_position_associates_resultfirst. ((pfrep_position_associates_resultfirst+S (pfrep_power_associates_result)=(G)) /\ ((((exists ff_h_pfp_associates_resultfirstentry. ff_h_pfp_associates_resultfirstentry + S (pfrep_left_associates_result) = S ((S (pfrep_position_associates_resultfirst)) * gc)) /\ exists ff_q_pfp_associates_resultfirstentry. gb = ff_q_pfp_associates_resultfirstentry * S ((S (pfrep_position_associates_resultfirst)) * gc) + (pfrep_left_associates_result)))))) \/ (((exists pfrep_gap_associates_resultfirstoutside. pfrep_gap_associates_resultfirstoutside+(G)=(pfrep_power_associates_result)) /\ (((pfrep_left_associates_result)=0))))) -> ((exists pfrep_position_associates_resultsecond. ((pfrep_position_associates_resultsecond+S (pfrep_power_associates_result)=(H)) /\ ((((exists ff_h_pfp_associates_resultsecondentry. ff_h_pfp_associates_resultsecondentry + S (pfrep_right_associates_result) = S ((S (pfrep_position_associates_resultsecond)) * hc)) /\ exists ff_q_pfp_associates_resultsecondentry. hb = ff_q_pfp_associates_resultsecondentry * S ((S (pfrep_position_associates_resultsecond)) * hc) + (pfrep_right_associates_result)))))) \/ (((exists pfrep_gap_associates_resultsecondoutside. pfrep_gap_associates_resultsecondoutside+(H)=(pfrep_power_associates_result)) /\ (((pfrep_right_associates_result)=0))))) -> pfrep_left_associates_result=pfrep_right_associates_result)

Complete tactic proof in conservative notation

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

122 script commands · 30 reading checkpoints · 14 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 right divides represented degree boundprime field polynomial monic equal degree right divides 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
03Establish hgnL13–13

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

  1. L13
    have hgn : ~(G=0)
04Separate the logical casesL14–14

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

  1. L14
    cases hg
05Use earlier factsL15–15

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

  1. L15
    exact hg_left
06Establish hhnL16–16

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

  1. L16
    have hhn : ~(H=0)
07Separate the logical casesL17–17

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

  1. L17
    cases hh
08Use earlier factsL18–18

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

  1. L18
    exact hh_left
09Establish hglL19–22

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

  1. L19
    have hgl : exists d. G=S d
  2. L20
    specialize nonzero_is_succ (G)
  3. L21
    apply nonzero_is_succ
  4. L22
    exact hgn
10Separate the logical casesL23–23

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

  1. L23
    cases hgl
11Establish hhlL24–27

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

  1. L24
    have hhl : exists e. H=S e
  2. L25
    specialize nonzero_is_succ (H)
  3. L26
    apply nonzero_is_succ
  4. L27
    exact hhn
12Separate the logical casesL28–28

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

  1. L28
    cases hhl
13Establish hgdL29–37

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. L29
    have hgd : FpRepresentedDegree(p,gb,gc,G,x)Definitions: FpRepresentedDegree(p,gb,gc,G,x)Original native command in the exact edition
  2. L30
    specialize prime_field_polynomial_monic_represented_degree (p)
  3. L31
    specialize prime_field_polynomial_monic_represented_degree (gb)
  4. L32
    specialize prime_field_polynomial_monic_represented_degree (gc)
  5. L33
    specialize prime_field_polynomial_monic_represented_degree (G)
  6. L34
    specialize prime_field_polynomial_monic_represented_degree (x)
  7. L35
    apply prime_field_polynomial_monic_represented_degree
  8. L36
    exact hg
  9. L37
    exact hgl_witness
14Establish hhdL38–46

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. L38
    have hhd : FpRepresentedDegree(p,hb,hc,H,x1)Definitions: FpRepresentedDegree(p,hb,hc,H,x1)Original native command in the exact edition
  2. L39
    specialize prime_field_polynomial_monic_represented_degree (p)
  3. L40
    specialize prime_field_polynomial_monic_represented_degree (hb)
  4. L41
    specialize prime_field_polynomial_monic_represented_degree (hc)
  5. L42
    specialize prime_field_polynomial_monic_represented_degree (H)
  6. L43
    specialize prime_field_polynomial_monic_represented_degree (x1)
  7. L44
    apply prime_field_polynomial_monic_represented_degree
  8. L45
    exact hh
  9. L46
    exact hhl_witness
15Establish hdeL47–56

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

  1. L47
    have hde : x=x1
  2. L48
    specialize le_antisymm (x)
  3. L49
    specialize le_antisymm (x1)
  4. L50
    apply le_antisymm
  5. L51
    specialize prime_field_polynomial_right_divides_represented_degree_bound (p)
  6. L52
    specialize prime_field_polynomial_right_divides_represented_degree_bound (gb)
  7. L53
    specialize prime_field_polynomial_right_divides_represented_degree_bound (gc)
  8. L54
    specialize prime_field_polynomial_right_divides_represented_degree_bound (G)
  9. L55
    specialize prime_field_polynomial_right_divides_represented_degree_bound (x)
  10. L56
    specialize prime_field_polynomial_right_divides_represented_degree_bound (hb)
16Use earlier factsL57–66

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

  1. L57
    specialize prime_field_polynomial_right_divides_represented_degree_bound (hc)
  2. L58
    specialize prime_field_polynomial_right_divides_represented_degree_bound (H)
  3. L59
    specialize prime_field_polynomial_right_divides_represented_degree_bound (x1)
  4. L60
    apply prime_field_polynomial_right_divides_represented_degree_bound
  5. L61
    exact hp
  6. L62
    exact hgd
  7. L63
    exact hhd
  8. L64
    exact hgh
  9. L65
    specialize prime_field_polynomial_right_divides_represented_degree_bound (p)
  10. L66
    specialize prime_field_polynomial_right_divides_represented_degree_bound (hb)
17Use earlier factsL67–76

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

  1. L67
    specialize prime_field_polynomial_right_divides_represented_degree_bound (hc)
  2. L68
    specialize prime_field_polynomial_right_divides_represented_degree_bound (H)
  3. L69
    specialize prime_field_polynomial_right_divides_represented_degree_bound (x1)
  4. L70
    specialize prime_field_polynomial_right_divides_represented_degree_bound (gb)
  5. L71
    specialize prime_field_polynomial_right_divides_represented_degree_bound (gc)
  6. L72
    specialize prime_field_polynomial_right_divides_represented_degree_bound (G)
  7. L73
    specialize prime_field_polynomial_right_divides_represented_degree_bound (x)
  8. L74
    apply prime_field_polynomial_right_divides_represented_degree_bound
  9. L75
    exact hp
  10. L76
    exact hhd
18Use earlier factsL77–78

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

  1. L77
    exact hgd
  2. L78
    exact hhg
19Establish hsameL79–82

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

  1. L79
    have hsame : H=S x
  2. L80
    rewrite hhl_witness
  3. L81
    rewrite hde
  4. L82
    refl
20Establish hgeL83–83

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

  1. L83
    have hge : FpMonic(p,gb,gc,S x)Definitions: FpMonic(p,gb,gc,S x)Original native command in the exact edition
21Establish hcopyL84–88

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

  1. L84
    have hcopy : FpMonic(p,gb,gc,G)Definitions: FpMonic(p,gb,gc,G)Original native command in the exact edition
  2. L85
    exact hg
  3. L86
    rewrite hgl_witness at hcopy
  4. L87
    rewrite hgl_witness at hcopy
  5. L88
    exact hcopy
22Establish hheL89–89

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

  1. L89
    have hhe : FpMonic(p,hb,hc,S x)Definitions: FpMonic(p,hb,hc,S x)Original native command in the exact edition
23Establish hcopyL90–94

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

  1. L90
    have hcopy : FpMonic(p,hb,hc,H)Definitions: FpMonic(p,hb,hc,H)Original native command in the exact edition
  2. L91
    exact hh
  3. L92
    rewrite hsame at hcopy
  4. L93
    rewrite hsame at hcopy
  5. L94
    exact hcopy
24Establish hrL95–95

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

  1. L95
    have hr : FpPolynomialRightDivides(p,gb,gc,S x,hb,hc,S x)Definitions: FpPolynomialRightDivides(p,gb,gc,S x,hb,hc,S x)Original native command in the exact edition
25Establish hcopyL96–105

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

  1. L96
    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. L97
    exact hgh
  3. L98
    rewrite hgl_witness at hcopy
  4. L99
    rewrite hgl_witness at hcopy
  5. L100
    rewrite hgl_witness at hcopy
  6. L101
    rewrite hgl_witness at hcopy
  7. L102
    rewrite hgl_witness at hcopy
  8. L103
    rewrite hgl_witness at hcopy
  9. L104
    rewrite hsame at hcopy
  10. L105
    rewrite hsame at hcopy
26Calculate and transport equalitiesL106–106

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

  1. L106
    rewrite hsame at hcopy
27Use earlier factsL107–107

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

  1. L107
    exact hcopy
28Calculate and transport equalitiesL108–111

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

  1. L108
    rewrite hgl_witness
  2. L109
    rewrite hgl_witness
  3. L110
    rewrite hsame
  4. L111
    rewrite hsame
29Use earlier factsL112–121

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

  1. L112
    specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (p)
  2. L113
    specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (gb)
  3. L114
    specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (gc)
  4. L115
    specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (hb)
  5. L116
    specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (hc)
  6. L117
    specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (x)
  7. L118
    apply prime_field_polynomial_monic_equal_degree_right_divides_equivalent
  8. L119
    exact hp
  9. L120
    exact hge
  10. L121
    exact hhe
30Use earlier factsL122–122

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

  1. L122
    exact hr

Library-wide reading audit

Original defined command ledger · 122 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. 0013have hgn : ~(G=0)
  14. 0014cases hg
  15. 0015exact hg_left
  16. 0016have hhn : ~(H=0)
  17. 0017cases hh
  18. 0018exact hh_left
  19. 0019have hgl : exists d. G=S d
  20. 0020specialize nonzero_is_succ (G)
  21. 0021apply nonzero_is_succ
  22. 0022exact hgn
  23. 0023cases hgl
  24. 0024have hhl : exists e. H=S e
  25. 0025specialize nonzero_is_succ (H)
  26. 0026apply nonzero_is_succ
  27. 0027exact hhn
  28. 0028cases hhl
  29. 0029have hgd : FpRepresentedDegree(p,gb,gc,G,x)
  30. 0030specialize prime_field_polynomial_monic_represented_degree (p)
  31. 0031specialize prime_field_polynomial_monic_represented_degree (gb)
  32. 0032specialize prime_field_polynomial_monic_represented_degree (gc)
  33. 0033specialize prime_field_polynomial_monic_represented_degree (G)
  34. 0034specialize prime_field_polynomial_monic_represented_degree (x)
  35. 0035apply prime_field_polynomial_monic_represented_degree
  36. 0036exact hg
  37. 0037exact hgl_witness
  38. 0038have hhd : FpRepresentedDegree(p,hb,hc,H,x1)
  39. 0039specialize prime_field_polynomial_monic_represented_degree (p)
  40. 0040specialize prime_field_polynomial_monic_represented_degree (hb)
  41. 0041specialize prime_field_polynomial_monic_represented_degree (hc)
  42. 0042specialize prime_field_polynomial_monic_represented_degree (H)
  43. 0043specialize prime_field_polynomial_monic_represented_degree (x1)
  44. 0044apply prime_field_polynomial_monic_represented_degree
  45. 0045exact hh
  46. 0046exact hhl_witness
  47. 0047have hde : x=x1
  48. 0048specialize le_antisymm (x)
  49. 0049specialize le_antisymm (x1)
  50. 0050apply le_antisymm
  51. 0051specialize prime_field_polynomial_right_divides_represented_degree_bound (p)
  52. 0052specialize prime_field_polynomial_right_divides_represented_degree_bound (gb)
  53. 0053specialize prime_field_polynomial_right_divides_represented_degree_bound (gc)
  54. 0054specialize prime_field_polynomial_right_divides_represented_degree_bound (G)
  55. 0055specialize prime_field_polynomial_right_divides_represented_degree_bound (x)
  56. 0056specialize prime_field_polynomial_right_divides_represented_degree_bound (hb)
  57. 0057specialize prime_field_polynomial_right_divides_represented_degree_bound (hc)
  58. 0058specialize prime_field_polynomial_right_divides_represented_degree_bound (H)
  59. 0059specialize prime_field_polynomial_right_divides_represented_degree_bound (x1)
  60. 0060apply prime_field_polynomial_right_divides_represented_degree_bound
  61. 0061exact hp
  62. 0062exact hgd
  63. 0063exact hhd
  64. 0064exact hgh
  65. 0065specialize prime_field_polynomial_right_divides_represented_degree_bound (p)
  66. 0066specialize prime_field_polynomial_right_divides_represented_degree_bound (hb)
  67. 0067specialize prime_field_polynomial_right_divides_represented_degree_bound (hc)
  68. 0068specialize prime_field_polynomial_right_divides_represented_degree_bound (H)
  69. 0069specialize prime_field_polynomial_right_divides_represented_degree_bound (x1)
  70. 0070specialize prime_field_polynomial_right_divides_represented_degree_bound (gb)
  71. 0071specialize prime_field_polynomial_right_divides_represented_degree_bound (gc)
  72. 0072specialize prime_field_polynomial_right_divides_represented_degree_bound (G)
  73. 0073specialize prime_field_polynomial_right_divides_represented_degree_bound (x)
  74. 0074apply prime_field_polynomial_right_divides_represented_degree_bound
  75. 0075exact hp
  76. 0076exact hhd
  77. 0077exact hgd
  78. 0078exact hhg
  79. 0079have hsame : H=S x
  80. 0080rewrite hhl_witness
  81. 0081rewrite hde
  82. 0082refl
  83. 0083have hge : FpMonic(p,gb,gc,S x)
  84. 0084have hcopy : FpMonic(p,gb,gc,G)
  85. 0085exact hg
  86. 0086rewrite hgl_witness at hcopy
  87. 0087rewrite hgl_witness at hcopy
  88. 0088exact hcopy
  89. 0089have hhe : FpMonic(p,hb,hc,S x)
  90. 0090have hcopy : FpMonic(p,hb,hc,H)
  91. 0091exact hh
  92. 0092rewrite hsame at hcopy
  93. 0093rewrite hsame at hcopy
  94. 0094exact hcopy
  95. 0095have hr : FpPolynomialRightDivides(p,gb,gc,S x,hb,hc,S x)
  96. 0096have hcopy : FpPolynomialRightDivides(p,gb,gc,G,hb,hc,H)
  97. 0097exact hgh
  98. 0098rewrite hgl_witness at hcopy
  99. 0099rewrite hgl_witness at hcopy
  100. 0100rewrite hgl_witness at hcopy
  101. 0101rewrite hgl_witness at hcopy
  102. 0102rewrite hgl_witness at hcopy
  103. 0103rewrite hgl_witness at hcopy
  104. 0104rewrite hsame at hcopy
  105. 0105rewrite hsame at hcopy
  106. 0106rewrite hsame at hcopy
  107. 0107exact hcopy
  108. 0108rewrite hgl_witness
  109. 0109rewrite hgl_witness
  110. 0110rewrite hsame
  111. 0111rewrite hsame
  112. 0112specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (p)
  113. 0113specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (gb)
  114. 0114specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (gc)
  115. 0115specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (hb)
  116. 0116specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (hc)
  117. 0117specialize prime_field_polynomial_monic_equal_degree_right_divides_equivalent (x)
  118. 0118apply prime_field_polynomial_monic_equal_degree_right_divides_equivalent
  119. 0119exact hp
  120. 0120exact hge
  121. 0121exact hhe
  122. 0122exact hr