HL0024

integer_polynomial_prime_power_hensel_iterated_exists_unique

For arbitrary finite j, an integer-polynomial simple root modulo p^k has a unique canonical lift modulo the actually constructed p^(k+j), retaining its full original residue class.

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. ∀ j. ∀ m. Prime(p) → ¬k = 0 → Pow(p,k,m) → SignedSimpleHornerRoot(pb,pc,nb,nc,a,l,m,p) → ∃ x. Pow(p,k + j,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_iterated_lifts_exists_unique
Original expanded first-order statement 
forall pb pc nb nc a l p k j m. ((~(p = 1) /\ forall frp_prime_left_sph_iterated_prime frp_prime_right_sph_iterated_prime. p = frp_prime_left_sph_iterated_prime * frp_prime_right_sph_iterated_prime -> frp_prime_left_sph_iterated_prime = 1 \/ frp_prime_right_sph_iterated_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 = k + j) -> (((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 + j)) * 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 + j)) * 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 + j) -> 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 45 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

45 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 iterated lifts 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 j
  10. L10
    intro m
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hprime
  2. L12
    intro hk
  3. L13
    intro hpower
  4. L14
    intro hsimple
03Separate the logical casesL15–20

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

  1. L15
    cases hsimple
  2. L16
    cases hsimple_witness
  3. L17
    cases hsimple_witness_witness
  4. L18
    cases hsimple_witness_witness_witness
  5. L19
    cases hsimple_witness_witness_witness_witness
  6. L20
    cases hsimple_witness_witness_witness_witness_right
04Use earlier factsL21–30

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

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

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

  1. L31
    specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique p
  2. L32
    specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique k
  3. L33
    specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique j
  4. L34
    specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique m
  5. L35
    apply beta_signed_horner_prime_power_iterated_lifts_exists_unique
06Fix variables and assumptionsL36–36

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

  1. L36
    intro hzero
07Use earlier factsL37–45

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

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

Library-wide reading audit

Original defined command ledger · 45 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 j
  10. 0010intro m
  11. 0011intro hprime
  12. 0012intro hk
  13. 0013intro hpower
  14. 0014intro hsimple
  15. 0015cases hsimple
  16. 0016cases hsimple_witness
  17. 0017cases hsimple_witness_witness
  18. 0018cases hsimple_witness_witness_witness
  19. 0019cases hsimple_witness_witness_witness_witness
  20. 0020cases hsimple_witness_witness_witness_witness_right
  21. 0021specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique pb
  22. 0022specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique pc
  23. 0023specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique nb
  24. 0024specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique nc
  25. 0025specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique a
  26. 0026specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique l
  27. 0027specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique x
  28. 0028specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique x1
  29. 0029specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique x2
  30. 0030specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique x3
  31. 0031specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique p
  32. 0032specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique k
  33. 0033specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique j
  34. 0034specialize beta_signed_horner_prime_power_iterated_lifts_exists_unique m
  35. 0035apply beta_signed_horner_prime_power_iterated_lifts_exists_unique
  36. 0036intro hzero
  37. 0037specialize prime_nonzero p
  38. 0038apply prime_nonzero
  39. 0039exact hprime
  40. 0040exact hzero
  41. 0041exact hk
  42. 0042exact hpower
  43. 0043exact hsimple_witness_witness_witness_witness_left
  44. 0044exact hsimple_witness_witness_witness_witness_right_left
  45. 0045exact hsimple_witness_witness_witness_witness_right_right