HL0023

integer_polynomial_prime_power_hensel_lift_exists_unique

G095: every integer-polynomial simple root at any natural representative modulo a positive prime power has one and only one canonical lift modulo the next actual power.

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. ∀ p. ∀ k. ∀ m. Prime(p) → ¬k = 0 → Pow(p,k,m) → SignedSimpleHornerRoot(pb,pc,nb,nc,a,l,m,p) → ∃ 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

SignedSimpleHornerRoot(pb,pc,nb,nc,a,l,m,p) · 1CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,M,r) · 2Prime(p) · 1Pow(a,e,z) · 2

Actual proof prerequisites

prime_nonzero · checked external prerequisitebeta_signed_horner_prime_power_hensel_lift_exists_unique
Original expanded first-order statement 
forall pb pc nb nc a l p k m. ((~(p = 1) /\ forall frp_prime_left_sph_hensel_prime frp_prime_right_sph_hensel_prime. p = frp_prime_left_sph_hensel_prime * frp_prime_right_sph_hensel_prime -> frp_prime_left_sph_hensel_prime = 1 \/ frp_prime_right_sph_hensel_prime = 1)) -> ~(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 sph_vp_simple sph_dp_simple sph_vn_simple sph_dn_simple. ((((exists ff_u_hd_hpl_sph_simple_positive ff_v_hd_hpl_sph_simple_positive ff_d_hd_hpl_sph_simple_positive ff_e_hd_hpl_sph_simple_positive. ((((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_start. fs_h_ph_hd_hpl_sph_simple_positive_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_start. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_value_start * S ((S (0)) * ff_v_hd_hpl_sph_simple_positive) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_terminal. fs_h_ph_hd_hpl_sph_simple_positive_body_value_terminal + S (sph_vp_simple) = S ((S (l)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_terminal. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_sph_simple_positive) + (sph_vp_simple))) /\ forall ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps. (exists ph_bound_hd_hpl_sph_simple_positive_body_value_steps. ph_bound_hd_hpl_sph_simple_positive_body_value_steps + S ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_simple_positive_body_value_steps ff_previous_ph_hd_hpl_sph_simple_positive_body_value_steps ff_current_ph_hd_hpl_sph_simple_positive_body_value_steps. ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_coefficient. fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_simple_positive_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * pc)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_coefficient. pb = fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * pc) + (ff_coefficient_ph_hd_hpl_sph_simple_positive_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_before. fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_before + S (ff_previous_ph_hd_hpl_sph_simple_positive_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_before. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * ff_v_hd_hpl_sph_simple_positive) + (ff_previous_ph_hd_hpl_sph_simple_positive_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_after. fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_after + S (ff_current_ph_hd_hpl_sph_simple_positive_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_after. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * ff_v_hd_hpl_sph_simple_positive) + (ff_current_ph_hd_hpl_sph_simple_positive_body_value_steps))) /\ ff_current_ph_hd_hpl_sph_simple_positive_body_value_steps = ff_previous_ph_hd_hpl_sph_simple_positive_body_value_steps * a + ff_coefficient_ph_hd_hpl_sph_simple_positive_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_start. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_start. ff_d_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_sph_simple_positive) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_terminal. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_terminal + S (sph_dp_simple) = S ((S (l)) * ff_e_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_terminal. ff_d_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_sph_simple_positive) + (sph_dp_simple))) /\ forall ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps. (exists ph_bound_hd_hpl_sph_simple_positive_body_derivative_steps. ph_bound_hd_hpl_sph_simple_positive_body_derivative_steps + S ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_simple_positive_body_derivative_steps ff_previous_ph_hd_hpl_sph_simple_positive_body_derivative_steps ff_current_ph_hd_hpl_sph_simple_positive_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_simple_positive_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_coefficient. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_v_hd_hpl_sph_simple_positive) + (ff_coefficient_ph_hd_hpl_sph_simple_positive_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_before. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_sph_simple_positive_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_before. ff_d_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_positive) + (ff_previous_ph_hd_hpl_sph_simple_positive_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_after. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_after + S (ff_current_ph_hd_hpl_sph_simple_positive_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_after. ff_d_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_positive) + (ff_current_ph_hd_hpl_sph_simple_positive_body_derivative_steps))) /\ ff_current_ph_hd_hpl_sph_simple_positive_body_derivative_steps = ff_previous_ph_hd_hpl_sph_simple_positive_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_sph_simple_positive_body_derivative_steps)))))))) /\ (exists ff_u_hd_hpl_sph_simple_negative ff_v_hd_hpl_sph_simple_negative ff_d_hd_hpl_sph_simple_negative ff_e_hd_hpl_sph_simple_negative. ((((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_start. fs_h_ph_hd_hpl_sph_simple_negative_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_start. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_value_start * S ((S (0)) * ff_v_hd_hpl_sph_simple_negative) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_terminal. fs_h_ph_hd_hpl_sph_simple_negative_body_value_terminal + S (sph_vn_simple) = S ((S (l)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_terminal. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_sph_simple_negative) + (sph_vn_simple))) /\ forall ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps. (exists ph_bound_hd_hpl_sph_simple_negative_body_value_steps. ph_bound_hd_hpl_sph_simple_negative_body_value_steps + S ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_simple_negative_body_value_steps ff_previous_ph_hd_hpl_sph_simple_negative_body_value_steps ff_current_ph_hd_hpl_sph_simple_negative_body_value_steps. ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_coefficient. fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_simple_negative_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * nc)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_coefficient. nb = fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * nc) + (ff_coefficient_ph_hd_hpl_sph_simple_negative_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_before. fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_before + S (ff_previous_ph_hd_hpl_sph_simple_negative_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_before. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * ff_v_hd_hpl_sph_simple_negative) + (ff_previous_ph_hd_hpl_sph_simple_negative_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_after. fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_after + S (ff_current_ph_hd_hpl_sph_simple_negative_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_after. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * ff_v_hd_hpl_sph_simple_negative) + (ff_current_ph_hd_hpl_sph_simple_negative_body_value_steps))) /\ ff_current_ph_hd_hpl_sph_simple_negative_body_value_steps = ff_previous_ph_hd_hpl_sph_simple_negative_body_value_steps * a + ff_coefficient_ph_hd_hpl_sph_simple_negative_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_start. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_start. ff_d_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_sph_simple_negative) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_terminal. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_terminal + S (sph_dn_simple) = S ((S (l)) * ff_e_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_terminal. ff_d_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_sph_simple_negative) + (sph_dn_simple))) /\ forall ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps. (exists ph_bound_hd_hpl_sph_simple_negative_body_derivative_steps. ph_bound_hd_hpl_sph_simple_negative_body_derivative_steps + S ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_simple_negative_body_derivative_steps ff_previous_ph_hd_hpl_sph_simple_negative_body_derivative_steps ff_current_ph_hd_hpl_sph_simple_negative_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_simple_negative_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_coefficient. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_v_hd_hpl_sph_simple_negative) + (ff_coefficient_ph_hd_hpl_sph_simple_negative_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_before. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_sph_simple_negative_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_before. ff_d_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_negative) + (ff_previous_ph_hd_hpl_sph_simple_negative_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_after. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_after + S (ff_current_ph_hd_hpl_sph_simple_negative_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_after. ff_d_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_negative) + (ff_current_ph_hd_hpl_sph_simple_negative_body_derivative_steps))) /\ ff_current_ph_hd_hpl_sph_simple_negative_body_derivative_steps = ff_previous_ph_hd_hpl_sph_simple_negative_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_sph_simple_negative_body_derivative_steps)))))))))) /\ ((exists hgcrt_mod_left_hpl_simple hgcrt_mod_right_hpl_simple. sph_vp_simple + m * hgcrt_mod_left_hpl_simple = sph_vn_simple + m * hgcrt_mod_right_hpl_simple) /\ (exists sph_inverse_simple. ((exists hpl_gap_simple. hpl_gap_simple + S (sph_inverse_simple) = (p)) /\ (exists hgcrt_mod_left_hpl_simple hgcrt_mod_right_hpl_simple. (sph_dp_simple * sph_inverse_simple) + p * hgcrt_mod_left_hpl_simple = (1 + sph_dn_simple * sph_inverse_simple) + p * hgcrt_mod_right_hpl_simple)))))) -> 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 43 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

43 script commands · 7 reading checkpoints · 0 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 (1)
beta signed horner prime power 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 p
  8. L8
    intro k
  9. L9
    intro m
  10. L10
    intro hprime
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hk
  2. L12
    intro hpower
  3. L13
    intro hsimple
03Separate the logical casesL14–19

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

  1. L14
    cases hsimple
  2. L15
    cases hsimple_witness
  3. L16
    cases hsimple_witness_witness
  4. L17
    cases hsimple_witness_witness_witness
  5. L18
    cases hsimple_witness_witness_witness_witness
  6. L19
    cases hsimple_witness_witness_witness_witness_right
04Use earlier factsL20–29

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

  1. L20
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique pb
  2. L21
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique pc
  3. L22
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique nb
  4. L23
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique nc
  5. L24
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique a
  6. L25
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique l
  7. L26
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique x
  8. L27
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique x1
  9. L28
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique x2
  10. L29
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique x3
05Use earlier factsL30–33

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

  1. L30
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique p
  2. L31
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique k
  3. L32
    specialize beta_signed_horner_prime_power_hensel_lift_exists_unique m
  4. L33
    apply beta_signed_horner_prime_power_hensel_lift_exists_unique
06Fix variables and assumptionsL34–34

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

  1. L34
    intro hzero
07Use earlier factsL35–43

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

  1. L35
    specialize prime_nonzero p
  2. L36
    apply prime_nonzero
  3. L37
    exact hprime
  4. L38
    exact hzero
  5. L39
    exact hk
  6. L40
    exact hpower
  7. L41
    exact hsimple_witness_witness_witness_witness_left
  8. L42
    exact hsimple_witness_witness_witness_witness_right_left
  9. L43
    exact hsimple_witness_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro a
  6. 0006intro l
  7. 0007intro p
  8. 0008intro k
  9. 0009intro m
  10. 0010intro hprime
  11. 0011intro hk
  12. 0012intro hpower
  13. 0013intro hsimple
  14. 0014cases hsimple
  15. 0015cases hsimple_witness
  16. 0016cases hsimple_witness_witness
  17. 0017cases hsimple_witness_witness_witness
  18. 0018cases hsimple_witness_witness_witness_witness
  19. 0019cases hsimple_witness_witness_witness_witness_right
  20. 0020specialize beta_signed_horner_prime_power_hensel_lift_exists_unique pb
  21. 0021specialize beta_signed_horner_prime_power_hensel_lift_exists_unique pc
  22. 0022specialize beta_signed_horner_prime_power_hensel_lift_exists_unique nb
  23. 0023specialize beta_signed_horner_prime_power_hensel_lift_exists_unique nc
  24. 0024specialize beta_signed_horner_prime_power_hensel_lift_exists_unique a
  25. 0025specialize beta_signed_horner_prime_power_hensel_lift_exists_unique l
  26. 0026specialize beta_signed_horner_prime_power_hensel_lift_exists_unique x
  27. 0027specialize beta_signed_horner_prime_power_hensel_lift_exists_unique x1
  28. 0028specialize beta_signed_horner_prime_power_hensel_lift_exists_unique x2
  29. 0029specialize beta_signed_horner_prime_power_hensel_lift_exists_unique x3
  30. 0030specialize beta_signed_horner_prime_power_hensel_lift_exists_unique p
  31. 0031specialize beta_signed_horner_prime_power_hensel_lift_exists_unique k
  32. 0032specialize beta_signed_horner_prime_power_hensel_lift_exists_unique m
  33. 0033apply beta_signed_horner_prime_power_hensel_lift_exists_unique
  34. 0034intro hzero
  35. 0035specialize prime_nonzero p
  36. 0036apply prime_nonzero
  37. 0037exact hprime
  38. 0038exact hzero
  39. 0039exact hk
  40. 0040exact hpower
  41. 0041exact hsimple_witness_witness_witness_witness_left
  42. 0042exact hsimple_witness_witness_witness_witness_right_left
  43. 0043exact hsimple_witness_witness_witness_witness_right_right