HL0021

beta_signed_horner_prime_power_hensel_lift_exists_unique

Full integer-coefficient simple-root Hensel lifting constructs the actual next power and its unique bounded root, with no bound on the original input and no supplied correction.

Alpha v34 checked-use · first admitted v27 · 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. Exact original first-admission records.

The derivative-nonzero criterion supplies no inverse or power witness: both are constructed. Roots may be arbitrary natural representatives of signed integer polynomials. Singular-root classification and p-adic completion are separate milestones.

Exact theorem in conservative defined notation

∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ a. ∀ l. ∀ vp. ∀ dp. ∀ vn. ∀ dn. ∀ p. ∀ k. ∀ m. ¬p = 0 → ¬k = 0 → Pow(p,k,m) → SignedHornerValueDerivative(pb,pc,nb,nc,a,l,vp,dp,vn,dn) → ModEq(m,vp,vn) → SignedDerivativeUnit(p,dp,dn) → ∃ x. Pow(p,S k,x) ∧ (∃ y. CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,x,y) ∧ (∀ z. CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,x,z) → z = y))

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

Definition DAG

SignedHornerValueDerivative(pb,pc,nb,nc,a,l,vp,dp,vn,dn) · 1SignedDerivativeUnit(p,dp,dn) · 1CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,M,r) · 2Dvd(d,n) · 1ModEq(m,a,b) · 1Pow(a,e,z) · 2

Actual proof prerequisites

hensel_positive_power_factorpow_successor_compose · checked external prerequisitebeta_signed_horner_simple_root_hensel_lift_exists_unique
Original expanded first-order statement 
forall pb pc nb nc a l vp dp vn dn p k m. ~(p = 0) -> ~(k = 0) -> (exists pa_b_hpl_power pa_c_hpl_power. ((forall pa_i_hpl_power_repeat. (exists pa_lt_hpl_power_repeat_bound. pa_lt_hpl_power_repeat_bound + S pa_i_hpl_power_repeat = k) -> (((exists pa_h_hpl_power_repeat_decoded. pa_h_hpl_power_repeat_decoded + S (p) = S ((S (pa_i_hpl_power_repeat)) * pa_c_hpl_power)) /\ exists pa_q_hpl_power_repeat_decoded. pa_b_hpl_power = pa_q_hpl_power_repeat_decoded * S ((S (pa_i_hpl_power_repeat)) * pa_c_hpl_power) + (p)))) /\ (exists pa_u_hpl_power_product pa_v_hpl_power_product. ((((exists pa_h_hpl_power_product_start. pa_h_hpl_power_product_start + S (1) = S ((S (0)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_start. pa_u_hpl_power_product = pa_q_hpl_power_product_start * S ((S (0)) * pa_v_hpl_power_product) + (1))) /\ ((((exists pa_h_hpl_power_product_terminal. pa_h_hpl_power_product_terminal + S (m) = S ((S (k)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_terminal. pa_u_hpl_power_product = pa_q_hpl_power_product_terminal * S ((S (k)) * pa_v_hpl_power_product) + (m))) /\ forall pa_i_hpl_power_product. (exists pa_lt_hpl_power_product_bound. pa_lt_hpl_power_product_bound + S pa_i_hpl_power_product = k) -> exists pa_p_hpl_power_product pa_r_hpl_power_product pa_s_hpl_power_product. ((((exists pa_h_hpl_power_product_factor. pa_h_hpl_power_product_factor + S (pa_p_hpl_power_product) = S ((S (pa_i_hpl_power_product)) * pa_c_hpl_power)) /\ exists pa_q_hpl_power_product_factor. pa_b_hpl_power = pa_q_hpl_power_product_factor * S ((S (pa_i_hpl_power_product)) * pa_c_hpl_power) + (pa_p_hpl_power_product))) /\ ((((exists pa_h_hpl_power_product_partial. pa_h_hpl_power_product_partial + S (pa_r_hpl_power_product) = S ((S (pa_i_hpl_power_product)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_partial. pa_u_hpl_power_product = pa_q_hpl_power_product_partial * S ((S (pa_i_hpl_power_product)) * pa_v_hpl_power_product) + (pa_r_hpl_power_product))) /\ ((((exists pa_h_hpl_power_product_successor. pa_h_hpl_power_product_successor + S (pa_s_hpl_power_product) = S ((S (S pa_i_hpl_power_product)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_successor. pa_u_hpl_power_product = pa_q_hpl_power_product_successor * S ((S (S pa_i_hpl_power_product)) * pa_v_hpl_power_product) + (pa_s_hpl_power_product))) /\ pa_s_hpl_power_product = pa_r_hpl_power_product * pa_p_hpl_power_product)))))))) -> (((exists ff_u_hd_hpl_sph_pair_positive ff_v_hd_hpl_sph_pair_positive ff_d_hd_hpl_sph_pair_positive ff_e_hd_hpl_sph_pair_positive. ((((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_start. fs_h_ph_hd_hpl_sph_pair_positive_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_start. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_value_start * S ((S (0)) * ff_v_hd_hpl_sph_pair_positive) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_terminal. fs_h_ph_hd_hpl_sph_pair_positive_body_value_terminal + S (vp) = S ((S (l)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_terminal. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_sph_pair_positive) + (vp))) /\ forall ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps. (exists ph_bound_hd_hpl_sph_pair_positive_body_value_steps. ph_bound_hd_hpl_sph_pair_positive_body_value_steps + S ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_pair_positive_body_value_steps ff_previous_ph_hd_hpl_sph_pair_positive_body_value_steps ff_current_ph_hd_hpl_sph_pair_positive_body_value_steps. ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_coefficient. fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_pair_positive_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * pc)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_coefficient. pb = fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * pc) + (ff_coefficient_ph_hd_hpl_sph_pair_positive_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_before. fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_before + S (ff_previous_ph_hd_hpl_sph_pair_positive_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_before. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * ff_v_hd_hpl_sph_pair_positive) + (ff_previous_ph_hd_hpl_sph_pair_positive_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_after. fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_after + S (ff_current_ph_hd_hpl_sph_pair_positive_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_after. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * ff_v_hd_hpl_sph_pair_positive) + (ff_current_ph_hd_hpl_sph_pair_positive_body_value_steps))) /\ ff_current_ph_hd_hpl_sph_pair_positive_body_value_steps = ff_previous_ph_hd_hpl_sph_pair_positive_body_value_steps * a + ff_coefficient_ph_hd_hpl_sph_pair_positive_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_start. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_start. ff_d_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_sph_pair_positive) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_terminal. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_terminal + S (dp) = S ((S (l)) * ff_e_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_terminal. ff_d_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_sph_pair_positive) + (dp))) /\ forall ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps. (exists ph_bound_hd_hpl_sph_pair_positive_body_derivative_steps. ph_bound_hd_hpl_sph_pair_positive_body_derivative_steps + S ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_pair_positive_body_derivative_steps ff_previous_ph_hd_hpl_sph_pair_positive_body_derivative_steps ff_current_ph_hd_hpl_sph_pair_positive_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_pair_positive_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_coefficient. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_v_hd_hpl_sph_pair_positive) + (ff_coefficient_ph_hd_hpl_sph_pair_positive_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_before. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_sph_pair_positive_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_before. ff_d_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_positive) + (ff_previous_ph_hd_hpl_sph_pair_positive_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_after. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_after + S (ff_current_ph_hd_hpl_sph_pair_positive_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_after. ff_d_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_positive) + (ff_current_ph_hd_hpl_sph_pair_positive_body_derivative_steps))) /\ ff_current_ph_hd_hpl_sph_pair_positive_body_derivative_steps = ff_previous_ph_hd_hpl_sph_pair_positive_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_sph_pair_positive_body_derivative_steps)))))))) /\ (exists ff_u_hd_hpl_sph_pair_negative ff_v_hd_hpl_sph_pair_negative ff_d_hd_hpl_sph_pair_negative ff_e_hd_hpl_sph_pair_negative. ((((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_start. fs_h_ph_hd_hpl_sph_pair_negative_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_start. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_value_start * S ((S (0)) * ff_v_hd_hpl_sph_pair_negative) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_terminal. fs_h_ph_hd_hpl_sph_pair_negative_body_value_terminal + S (vn) = S ((S (l)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_terminal. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_sph_pair_negative) + (vn))) /\ forall ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps. (exists ph_bound_hd_hpl_sph_pair_negative_body_value_steps. ph_bound_hd_hpl_sph_pair_negative_body_value_steps + S ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_pair_negative_body_value_steps ff_previous_ph_hd_hpl_sph_pair_negative_body_value_steps ff_current_ph_hd_hpl_sph_pair_negative_body_value_steps. ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_coefficient. fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_pair_negative_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * nc)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_coefficient. nb = fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * nc) + (ff_coefficient_ph_hd_hpl_sph_pair_negative_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_before. fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_before + S (ff_previous_ph_hd_hpl_sph_pair_negative_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_before. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * ff_v_hd_hpl_sph_pair_negative) + (ff_previous_ph_hd_hpl_sph_pair_negative_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_after. fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_after + S (ff_current_ph_hd_hpl_sph_pair_negative_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_after. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * ff_v_hd_hpl_sph_pair_negative) + (ff_current_ph_hd_hpl_sph_pair_negative_body_value_steps))) /\ ff_current_ph_hd_hpl_sph_pair_negative_body_value_steps = ff_previous_ph_hd_hpl_sph_pair_negative_body_value_steps * a + ff_coefficient_ph_hd_hpl_sph_pair_negative_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_start. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_start. ff_d_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_sph_pair_negative) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_terminal. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_terminal + S (dn) = S ((S (l)) * ff_e_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_terminal. ff_d_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_sph_pair_negative) + (dn))) /\ forall ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps. (exists ph_bound_hd_hpl_sph_pair_negative_body_derivative_steps. ph_bound_hd_hpl_sph_pair_negative_body_derivative_steps + S ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_pair_negative_body_derivative_steps ff_previous_ph_hd_hpl_sph_pair_negative_body_derivative_steps ff_current_ph_hd_hpl_sph_pair_negative_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_pair_negative_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_coefficient. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_v_hd_hpl_sph_pair_negative) + (ff_coefficient_ph_hd_hpl_sph_pair_negative_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_before. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_sph_pair_negative_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_before. ff_d_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_negative) + (ff_previous_ph_hd_hpl_sph_pair_negative_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_after. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_after + S (ff_current_ph_hd_hpl_sph_pair_negative_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_after. ff_d_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_negative) + (ff_current_ph_hd_hpl_sph_pair_negative_body_derivative_steps))) /\ ff_current_ph_hd_hpl_sph_pair_negative_body_derivative_steps = ff_previous_ph_hd_hpl_sph_pair_negative_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_sph_pair_negative_body_derivative_steps)))))))))) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. vp + m * hgcrt_mod_left_hpl_mod = vn + m * hgcrt_mod_right_hpl_mod) -> (exists sph_inverse_unit. ((exists hpl_gap_unit. hpl_gap_unit + S (sph_inverse_unit) = (p)) /\ (exists hgcrt_mod_left_hpl_unit hgcrt_mod_right_hpl_unit. (dp * sph_inverse_unit) + p * hgcrt_mod_left_hpl_unit = (1 + dn * sph_inverse_unit) + p * hgcrt_mod_right_hpl_unit))) -> exists M. ((exists pa_b_hpl_power pa_c_hpl_power. ((forall pa_i_hpl_power_repeat. (exists pa_lt_hpl_power_repeat_bound. pa_lt_hpl_power_repeat_bound + S pa_i_hpl_power_repeat = S k) -> (((exists pa_h_hpl_power_repeat_decoded. pa_h_hpl_power_repeat_decoded + S (p) = S ((S (pa_i_hpl_power_repeat)) * pa_c_hpl_power)) /\ exists pa_q_hpl_power_repeat_decoded. pa_b_hpl_power = pa_q_hpl_power_repeat_decoded * S ((S (pa_i_hpl_power_repeat)) * pa_c_hpl_power) + (p)))) /\ (exists pa_u_hpl_power_product pa_v_hpl_power_product. ((((exists pa_h_hpl_power_product_start. pa_h_hpl_power_product_start + S (1) = S ((S (0)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_start. pa_u_hpl_power_product = pa_q_hpl_power_product_start * S ((S (0)) * pa_v_hpl_power_product) + (1))) /\ ((((exists pa_h_hpl_power_product_terminal. pa_h_hpl_power_product_terminal + S (M) = S ((S (S k)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_terminal. pa_u_hpl_power_product = pa_q_hpl_power_product_terminal * S ((S (S k)) * pa_v_hpl_power_product) + (M))) /\ forall pa_i_hpl_power_product. (exists pa_lt_hpl_power_product_bound. pa_lt_hpl_power_product_bound + S pa_i_hpl_power_product = S k) -> exists pa_p_hpl_power_product pa_r_hpl_power_product pa_s_hpl_power_product. ((((exists pa_h_hpl_power_product_factor. pa_h_hpl_power_product_factor + S (pa_p_hpl_power_product) = S ((S (pa_i_hpl_power_product)) * pa_c_hpl_power)) /\ exists pa_q_hpl_power_product_factor. pa_b_hpl_power = pa_q_hpl_power_product_factor * S ((S (pa_i_hpl_power_product)) * pa_c_hpl_power) + (pa_p_hpl_power_product))) /\ ((((exists pa_h_hpl_power_product_partial. pa_h_hpl_power_product_partial + S (pa_r_hpl_power_product) = S ((S (pa_i_hpl_power_product)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_partial. pa_u_hpl_power_product = pa_q_hpl_power_product_partial * S ((S (pa_i_hpl_power_product)) * pa_v_hpl_power_product) + (pa_r_hpl_power_product))) /\ ((((exists pa_h_hpl_power_product_successor. pa_h_hpl_power_product_successor + S (pa_s_hpl_power_product) = S ((S (S pa_i_hpl_power_product)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_successor. pa_u_hpl_power_product = pa_q_hpl_power_product_successor * S ((S (S pa_i_hpl_power_product)) * pa_v_hpl_power_product) + (pa_s_hpl_power_product))) /\ pa_s_hpl_power_product = pa_r_hpl_power_product * pa_p_hpl_power_product)))))))) /\ exists r. ((((exists hpl_gap_lift. hpl_gap_lift + S (r) = (M)) /\ ((exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. r + m * hgcrt_mod_left_hpl_lift = a + m * hgcrt_mod_right_hpl_lift) /\ (exists sph_positive_lift sph_negative_lift. ((exists ff_u_ph_hpl_sph_lift_positive ff_v_ph_hpl_sph_lift_positive. ((((exists fs_h_ph_hpl_sph_lift_positive_body_start. fs_h_ph_hpl_sph_lift_positive_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_start. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_start * S ((S (0)) * ff_v_ph_hpl_sph_lift_positive) + (0))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_terminal. fs_h_ph_hpl_sph_lift_positive_body_terminal + S (sph_positive_lift) = S ((S (l)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_terminal. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_lift_positive) + (sph_positive_lift))) /\ forall ff_i_ph_hpl_sph_lift_positive_body_steps. (exists ph_bound_hpl_sph_lift_positive_body_steps. ph_bound_hpl_sph_lift_positive_body_steps + S ff_i_ph_hpl_sph_lift_positive_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_lift_positive_body_steps ff_previous_ph_hpl_sph_lift_positive_body_steps ff_current_ph_hpl_sph_lift_positive_body_steps. ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_coefficient. fs_h_ph_hpl_sph_lift_positive_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_lift_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * pc)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_coefficient. pb = fs_q_ph_hpl_sph_lift_positive_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * pc) + (ff_coefficient_ph_hpl_sph_lift_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_before. fs_h_ph_hpl_sph_lift_positive_body_steps_before + S (ff_previous_ph_hpl_sph_lift_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_before. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_steps_before * S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive) + (ff_previous_ph_hpl_sph_lift_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_after. fs_h_ph_hpl_sph_lift_positive_body_steps_after + S (ff_current_ph_hpl_sph_lift_positive_body_steps) = S ((S (S ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_after. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_steps_after * S ((S (S ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive) + (ff_current_ph_hpl_sph_lift_positive_body_steps))) /\ ff_current_ph_hpl_sph_lift_positive_body_steps = ff_previous_ph_hpl_sph_lift_positive_body_steps * r + ff_coefficient_ph_hpl_sph_lift_positive_body_steps)))))) /\ ((exists ff_u_ph_hpl_sph_lift_negative ff_v_ph_hpl_sph_lift_negative. ((((exists fs_h_ph_hpl_sph_lift_negative_body_start. fs_h_ph_hpl_sph_lift_negative_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_start. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_start * S ((S (0)) * ff_v_ph_hpl_sph_lift_negative) + (0))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_terminal. fs_h_ph_hpl_sph_lift_negative_body_terminal + S (sph_negative_lift) = S ((S (l)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_terminal. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_lift_negative) + (sph_negative_lift))) /\ forall ff_i_ph_hpl_sph_lift_negative_body_steps. (exists ph_bound_hpl_sph_lift_negative_body_steps. ph_bound_hpl_sph_lift_negative_body_steps + S ff_i_ph_hpl_sph_lift_negative_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_lift_negative_body_steps ff_previous_ph_hpl_sph_lift_negative_body_steps ff_current_ph_hpl_sph_lift_negative_body_steps. ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_coefficient. fs_h_ph_hpl_sph_lift_negative_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_lift_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * nc)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_coefficient. nb = fs_q_ph_hpl_sph_lift_negative_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * nc) + (ff_coefficient_ph_hpl_sph_lift_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_before. fs_h_ph_hpl_sph_lift_negative_body_steps_before + S (ff_previous_ph_hpl_sph_lift_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_before. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_steps_before * S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative) + (ff_previous_ph_hpl_sph_lift_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_after. fs_h_ph_hpl_sph_lift_negative_body_steps_after + S (ff_current_ph_hpl_sph_lift_negative_body_steps) = S ((S (S ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_after. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_steps_after * S ((S (S ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative) + (ff_current_ph_hpl_sph_lift_negative_body_steps))) /\ ff_current_ph_hpl_sph_lift_negative_body_steps = ff_previous_ph_hpl_sph_lift_negative_body_steps * r + ff_coefficient_ph_hpl_sph_lift_negative_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. sph_positive_lift + M * hgcrt_mod_left_hpl_lift = sph_negative_lift + M * hgcrt_mod_right_hpl_lift))))))) /\ forall z. (((exists hpl_gap_lift. hpl_gap_lift + S (z) = (M)) /\ ((exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. z + m * hgcrt_mod_left_hpl_lift = a + m * hgcrt_mod_right_hpl_lift) /\ (exists sph_positive_lift sph_negative_lift. ((exists ff_u_ph_hpl_sph_lift_positive ff_v_ph_hpl_sph_lift_positive. ((((exists fs_h_ph_hpl_sph_lift_positive_body_start. fs_h_ph_hpl_sph_lift_positive_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_start. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_start * S ((S (0)) * ff_v_ph_hpl_sph_lift_positive) + (0))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_terminal. fs_h_ph_hpl_sph_lift_positive_body_terminal + S (sph_positive_lift) = S ((S (l)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_terminal. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_lift_positive) + (sph_positive_lift))) /\ forall ff_i_ph_hpl_sph_lift_positive_body_steps. (exists ph_bound_hpl_sph_lift_positive_body_steps. ph_bound_hpl_sph_lift_positive_body_steps + S ff_i_ph_hpl_sph_lift_positive_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_lift_positive_body_steps ff_previous_ph_hpl_sph_lift_positive_body_steps ff_current_ph_hpl_sph_lift_positive_body_steps. ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_coefficient. fs_h_ph_hpl_sph_lift_positive_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_lift_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * pc)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_coefficient. pb = fs_q_ph_hpl_sph_lift_positive_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * pc) + (ff_coefficient_ph_hpl_sph_lift_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_before. fs_h_ph_hpl_sph_lift_positive_body_steps_before + S (ff_previous_ph_hpl_sph_lift_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_before. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_steps_before * S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive) + (ff_previous_ph_hpl_sph_lift_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_after. fs_h_ph_hpl_sph_lift_positive_body_steps_after + S (ff_current_ph_hpl_sph_lift_positive_body_steps) = S ((S (S ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_after. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_steps_after * S ((S (S ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive) + (ff_current_ph_hpl_sph_lift_positive_body_steps))) /\ ff_current_ph_hpl_sph_lift_positive_body_steps = ff_previous_ph_hpl_sph_lift_positive_body_steps * z + ff_coefficient_ph_hpl_sph_lift_positive_body_steps)))))) /\ ((exists ff_u_ph_hpl_sph_lift_negative ff_v_ph_hpl_sph_lift_negative. ((((exists fs_h_ph_hpl_sph_lift_negative_body_start. fs_h_ph_hpl_sph_lift_negative_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_start. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_start * S ((S (0)) * ff_v_ph_hpl_sph_lift_negative) + (0))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_terminal. fs_h_ph_hpl_sph_lift_negative_body_terminal + S (sph_negative_lift) = S ((S (l)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_terminal. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_lift_negative) + (sph_negative_lift))) /\ forall ff_i_ph_hpl_sph_lift_negative_body_steps. (exists ph_bound_hpl_sph_lift_negative_body_steps. ph_bound_hpl_sph_lift_negative_body_steps + S ff_i_ph_hpl_sph_lift_negative_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_lift_negative_body_steps ff_previous_ph_hpl_sph_lift_negative_body_steps ff_current_ph_hpl_sph_lift_negative_body_steps. ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_coefficient. fs_h_ph_hpl_sph_lift_negative_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_lift_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * nc)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_coefficient. nb = fs_q_ph_hpl_sph_lift_negative_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * nc) + (ff_coefficient_ph_hpl_sph_lift_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_before. fs_h_ph_hpl_sph_lift_negative_body_steps_before + S (ff_previous_ph_hpl_sph_lift_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_before. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_steps_before * S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative) + (ff_previous_ph_hpl_sph_lift_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_after. fs_h_ph_hpl_sph_lift_negative_body_steps_after + S (ff_current_ph_hpl_sph_lift_negative_body_steps) = S ((S (S ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_after. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_steps_after * S ((S (S ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative) + (ff_current_ph_hpl_sph_lift_negative_body_steps))) /\ ff_current_ph_hpl_sph_lift_negative_body_steps = ff_previous_ph_hpl_sph_lift_negative_body_steps * z + ff_coefficient_ph_hpl_sph_lift_negative_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. sph_positive_lift + M * hgcrt_mod_left_hpl_lift = sph_negative_lift + M * hgcrt_mod_right_hpl_lift))))))) -> z = r))

Complete tactic proof in conservative notation

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

58 script commands · 10 reading checkpoints · 1 local claims

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

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

Named ingredients (2)
hensel positive power factorbeta signed horner simple root hensel lift exists unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro a
  6. L6
    intro l
  7. L7
    intro vp
  8. L8
    intro dp
  9. L9
    intro vn
  10. L10
    intro dn
02Fix variables and assumptionsL11–19

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

  1. L11
    intro p
  2. L12
    intro k
  3. L13
    intro m
  4. L14
    intro hp
  5. L15
    intro hk
  6. L16
    intro hpower
  7. L17
    intro hpair
  8. L18
    intro hroot
  9. L19
    intro hunit
03Establish hfactorL20–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hensel positive power factor.

  1. L20
    have hfactor : ¬m = 0 ∧ Dvd(p,m)Definitions: Dvd(p,m)Original native command in the exact edition
  2. L21
    specialize hensel_positive_power_factor p
  3. L22
    specialize hensel_positive_power_factor k
  4. L23
    specialize hensel_positive_power_factor m
  5. L24
    apply hensel_positive_power_factor
  6. L25
    exact hp
  7. L26
    exact hk
  8. L27
    exact hpower
04Separate the logical casesL28–29

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

  1. L28
    cases hfactor
  2. L29
    cases hfactor_right
05Construct an explicit witnessL30–30

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

  1. L30
    exists m * p
06Separate the logical casesL31–31

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

  1. L31
    split
07Use earlier factsL32–37

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

  1. L32
    specialize pow_successor_compose p
  2. L33
    specialize pow_successor_compose k
  3. L34
    specialize pow_successor_compose m
  4. L35
    specialize pow_successor_compose (m * p)
  5. L36
    apply pow_successor_compose
  6. L37
    exact hpower
08Calculate and transport equalitiesL38–38

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

  1. L38
    refl
09Use earlier factsL39–48

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

  1. L39
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique pb
  2. L40
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique pc
  3. L41
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique nb
  4. L42
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique nc
  5. L43
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique a
  6. L44
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique l
  7. L45
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique vp
  8. L46
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique dp
  9. L47
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique vn
  10. L48
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique dn
10Use earlier factsL49–58

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

  1. L49
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique m
  2. L50
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique p
  3. L51
    specialize beta_signed_horner_simple_root_hensel_lift_exists_unique x
  4. L52
    apply beta_signed_horner_simple_root_hensel_lift_exists_unique
  5. L53
    exact hp
  6. L54
    exact hfactor_left
  7. L55
    exact hfactor_right_witness
  8. L56
    exact hpair
  9. L57
    exact hroot
  10. L58
    exact hunit

Library-wide reading audit

Original defined command ledger · 58 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro a
  6. 0006intro l
  7. 0007intro vp
  8. 0008intro dp
  9. 0009intro vn
  10. 0010intro dn
  11. 0011intro p
  12. 0012intro k
  13. 0013intro m
  14. 0014intro hp
  15. 0015intro hk
  16. 0016intro hpower
  17. 0017intro hpair
  18. 0018intro hroot
  19. 0019intro hunit
  20. 0020have hfactor : ¬m = 0 ∧ Dvd(p,m)
  21. 0021specialize hensel_positive_power_factor p
  22. 0022specialize hensel_positive_power_factor k
  23. 0023specialize hensel_positive_power_factor m
  24. 0024apply hensel_positive_power_factor
  25. 0025exact hp
  26. 0026exact hk
  27. 0027exact hpower
  28. 0028cases hfactor
  29. 0029cases hfactor_right
  30. 0030exists m * p
  31. 0031split
  32. 0032specialize pow_successor_compose p
  33. 0033specialize pow_successor_compose k
  34. 0034specialize pow_successor_compose m
  35. 0035specialize pow_successor_compose (m * p)
  36. 0036apply pow_successor_compose
  37. 0037exact hpower
  38. 0038refl
  39. 0039specialize beta_signed_horner_simple_root_hensel_lift_exists_unique pb
  40. 0040specialize beta_signed_horner_simple_root_hensel_lift_exists_unique pc
  41. 0041specialize beta_signed_horner_simple_root_hensel_lift_exists_unique nb
  42. 0042specialize beta_signed_horner_simple_root_hensel_lift_exists_unique nc
  43. 0043specialize beta_signed_horner_simple_root_hensel_lift_exists_unique a
  44. 0044specialize beta_signed_horner_simple_root_hensel_lift_exists_unique l
  45. 0045specialize beta_signed_horner_simple_root_hensel_lift_exists_unique vp
  46. 0046specialize beta_signed_horner_simple_root_hensel_lift_exists_unique dp
  47. 0047specialize beta_signed_horner_simple_root_hensel_lift_exists_unique vn
  48. 0048specialize beta_signed_horner_simple_root_hensel_lift_exists_unique dn
  49. 0049specialize beta_signed_horner_simple_root_hensel_lift_exists_unique m
  50. 0050specialize beta_signed_horner_simple_root_hensel_lift_exists_unique p
  51. 0051specialize beta_signed_horner_simple_root_hensel_lift_exists_unique x
  52. 0052apply beta_signed_horner_simple_root_hensel_lift_exists_unique
  53. 0053exact hp
  54. 0054exact hfactor_left
  55. 0055exact hfactor_right_witness
  56. 0056exact hpair
  57. 0057exact hroot
  58. 0058exact hunit