HL0012

beta_horner_hensel_iterated_exists_unique

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

HA induction constructs unique canonical simple-root lifts through every finite number of prime-power steps, including iteration zero, and proves uniqueness among all roots in the original residue class.

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.

Exact expanded first-order arithmetic statement

forall b c a l n d m p s. ~(p = 0) -> ~(m = 0) -> (exists ff_u_hd_hpl_pair ff_v_hd_hpl_pair ff_d_hd_hpl_pair ff_e_hd_hpl_pair. ((((((exists fs_h_ph_hd_hpl_pair_body_value_start. fs_h_ph_hd_hpl_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_start. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_start * S ((S (0)) * ff_v_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_terminal. fs_h_ph_hd_hpl_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_terminal. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_pair) + (n))) /\ forall ff_i_ph_hd_hpl_pair_body_value_steps. (exists ph_bound_hd_hpl_pair_body_value_steps. ph_bound_hd_hpl_pair_body_value_steps + S ff_i_ph_hd_hpl_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_value_steps ff_previous_ph_hd_hpl_pair_body_value_steps ff_current_ph_hd_hpl_pair_body_value_steps. ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_coefficient. fs_h_ph_hd_hpl_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_coefficient. b = fs_q_ph_hd_hpl_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_before. fs_h_ph_hd_hpl_pair_body_value_steps_before + S (ff_previous_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_before. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_after. fs_h_ph_hd_hpl_pair_body_value_steps_after + S (ff_current_ph_hd_hpl_pair_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_after. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_value_steps))) /\ ff_current_ph_hd_hpl_pair_body_value_steps = ff_previous_ph_hd_hpl_pair_body_value_steps * a + ff_coefficient_ph_hd_hpl_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_pair_body_derivative_start. fs_h_ph_hd_hpl_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_start. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_terminal. fs_h_ph_hd_hpl_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_terminal. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_pair) + (d))) /\ forall ff_i_ph_hd_hpl_pair_body_derivative_steps. (exists ph_bound_hd_hpl_pair_body_derivative_steps. ph_bound_hd_hpl_pair_body_derivative_steps + S ff_i_ph_hd_hpl_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_derivative_steps ff_previous_ph_hd_hpl_pair_body_derivative_steps ff_current_ph_hd_hpl_pair_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair) + (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_before. fs_h_ph_hd_hpl_pair_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_before. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_after. fs_h_ph_hd_hpl_pair_body_derivative_steps_after + S (ff_current_ph_hd_hpl_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_after. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_derivative_steps))) /\ ff_current_ph_hd_hpl_pair_body_derivative_steps = ff_previous_ph_hd_hpl_pair_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_pair_body_derivative_steps)))))))) -> m = p * s -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. n + m * hgcrt_mod_left_hpl_mod = 0 + m * hgcrt_mod_right_hpl_mod) -> (forall hmi_divisor_hpl_coprime. (exists hmi_left_factor_hpl_coprime. d = hmi_divisor_hpl_coprime * hmi_left_factor_hpl_coprime) -> (exists hmi_right_factor_hpl_coprime. p = hmi_divisor_hpl_coprime * hmi_right_factor_hpl_coprime) -> hmi_divisor_hpl_coprime = 1) -> forall j q. (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 = 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 (q) = S ((S (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 (j)) * pa_v_hpl_power_product) + (q))) /\ 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 = 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 * q)) /\ ((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 hpl_value_lift. ((exists ff_u_ph_hpl_lift ff_v_ph_hpl_lift. ((((exists fs_h_ph_hpl_lift_body_start. fs_h_ph_hpl_lift_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_start. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_start * S ((S (0)) * ff_v_ph_hpl_lift) + (0))) /\ ((((exists fs_h_ph_hpl_lift_body_terminal. fs_h_ph_hpl_lift_body_terminal + S (hpl_value_lift) = S ((S (l)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_terminal. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_terminal * S ((S (l)) * ff_v_ph_hpl_lift) + (hpl_value_lift))) /\ forall ff_i_ph_hpl_lift_body_steps. (exists ph_bound_hpl_lift_body_steps. ph_bound_hpl_lift_body_steps + S ff_i_ph_hpl_lift_body_steps = l) -> exists ff_coefficient_ph_hpl_lift_body_steps ff_previous_ph_hpl_lift_body_steps ff_current_ph_hpl_lift_body_steps. ((((exists fs_h_ph_hpl_lift_body_steps_coefficient. fs_h_ph_hpl_lift_body_steps_coefficient + S (ff_coefficient_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * c)) /\ exists fs_q_ph_hpl_lift_body_steps_coefficient. b = fs_q_ph_hpl_lift_body_steps_coefficient * S ((S (ff_i_ph_hpl_lift_body_steps)) * c) + (ff_coefficient_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_before. fs_h_ph_hpl_lift_body_steps_before + S (ff_previous_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_before. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_before * S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_previous_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_after. fs_h_ph_hpl_lift_body_steps_after + S (ff_current_ph_hpl_lift_body_steps) = S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_after. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_after * S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_current_ph_hpl_lift_body_steps))) /\ ff_current_ph_hpl_lift_body_steps = ff_previous_ph_hpl_lift_body_steps * r + ff_coefficient_ph_hpl_lift_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. hpl_value_lift + (m * q) * hgcrt_mod_left_hpl_lift = 0 + (m * q) * hgcrt_mod_right_hpl_lift)))))) /\ forall z. (((exists hpl_gap_lift. hpl_gap_lift + S (z) = (m * q)) /\ ((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 hpl_value_lift. ((exists ff_u_ph_hpl_lift ff_v_ph_hpl_lift. ((((exists fs_h_ph_hpl_lift_body_start. fs_h_ph_hpl_lift_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_start. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_start * S ((S (0)) * ff_v_ph_hpl_lift) + (0))) /\ ((((exists fs_h_ph_hpl_lift_body_terminal. fs_h_ph_hpl_lift_body_terminal + S (hpl_value_lift) = S ((S (l)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_terminal. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_terminal * S ((S (l)) * ff_v_ph_hpl_lift) + (hpl_value_lift))) /\ forall ff_i_ph_hpl_lift_body_steps. (exists ph_bound_hpl_lift_body_steps. ph_bound_hpl_lift_body_steps + S ff_i_ph_hpl_lift_body_steps = l) -> exists ff_coefficient_ph_hpl_lift_body_steps ff_previous_ph_hpl_lift_body_steps ff_current_ph_hpl_lift_body_steps. ((((exists fs_h_ph_hpl_lift_body_steps_coefficient. fs_h_ph_hpl_lift_body_steps_coefficient + S (ff_coefficient_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * c)) /\ exists fs_q_ph_hpl_lift_body_steps_coefficient. b = fs_q_ph_hpl_lift_body_steps_coefficient * S ((S (ff_i_ph_hpl_lift_body_steps)) * c) + (ff_coefficient_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_before. fs_h_ph_hpl_lift_body_steps_before + S (ff_previous_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_before. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_before * S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_previous_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_after. fs_h_ph_hpl_lift_body_steps_after + S (ff_current_ph_hpl_lift_body_steps) = S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_after. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_after * S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_current_ph_hpl_lift_body_steps))) /\ ff_current_ph_hpl_lift_body_steps = ff_previous_ph_hpl_lift_body_steps * z + ff_coefficient_ph_hpl_lift_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. hpl_value_lift + (m * q) * hgcrt_mod_left_hpl_lift = 0 + (m * q) * hgcrt_mod_right_hpl_lift)))))) -> z = r)

Constructive proof overview

Generated structural guide

HA induction constructs unique canonical simple-root lifts through every finite number of prime-power steps, including iteration zero, and proves uniqueness among all roots in the original residue class.

The unchanged tactic script uses 18 declared prerequisites and contains 234 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

pow_zero Stable theorem; checked-use authorized pow_successor_decompose Stable theorem; checked-use authorized pow_nonzero_of_one_le Alpha theorem; checked-use authorized one_le_of_ne_zero Stable theorem; checked-use authorized mul_ne_zero Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized HL000E hensel_canonical_horner_root_exists_unique beta_horner_derivative_value_projection Alpha theorem; checked-use authorized HL0011 beta_horner_simple_lift_preserves_simplicity HL000A beta_horner_simple_root_hensel_lift_exists_unique mod_eq_trans Stable theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized mod_eq_of_mod_eq_multiple Stable theorem; checked-use authorized HL0003 hensel_canonical_residue_exists HL000C beta_horner_root_mod_weaken HL000B beta_horner_root_mod_transport

Direct dependents

HL0013 beta_horner_prime_power_iterated_lifts_exists_unique HL001F beta_signed_horner_hensel_iterated_exists_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

234 script commands · 55 reading checkpoints · 14 local claims

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

Named ingredients (6)
hensel canonical horner root exists uniquebeta horner simple lift preserves simplicitybeta horner simple root hensel lift exists uniquehensel canonical residue existsbeta horner root mod weakenbeta horner root mod transport

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro a
  4. L4
    intro l
  5. L5
    intro n
  6. L6
    intro d
  7. L7
    intro m
  8. L8
    intro p
  9. L9
    intro s
  10. L10
    intro hp
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hm
  2. L12
    intro hpair
  3. L13
    intro hfactor
  4. L14
    intro hroot
  5. L15
    intro hcop
03Induction on jL16–18

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L16
    induction j
  2. L17
    intro q
  3. L18
    intro hpower
04Establish hqL19–25

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

  1. L19
    have hq : q = 1
  2. L20
    specialize pow_zero p
  3. L21
    specialize pow_zero 0
  4. L22
    specialize pow_zero q
  5. L23
    apply pow_zero
  6. L24
    refl
  7. L25
    exact hpower
05Establish hML26–35

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

  1. L26
    have hM : m * q = m
  2. L27
    rewrite hq
  3. L28
    apply mul_one
  4. L29
    rewrite hM
  5. L30
    rewrite hM
  6. L31
    rewrite hM
  7. L32
    rewrite hM
  8. L33
    rewrite hM
  9. L34
    rewrite hM
  10. L35
    specialize hensel_canonical_horner_root_exists_unique b
06Use earlier factsL36–41

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

  1. L36
    specialize hensel_canonical_horner_root_exists_unique c
  2. L37
    specialize hensel_canonical_horner_root_exists_unique a
  3. L38
    specialize hensel_canonical_horner_root_exists_unique l
  4. L39
    specialize hensel_canonical_horner_root_exists_unique m
  5. L40
    apply hensel_canonical_horner_root_exists_unique
  6. L41
    exact hm
07Construct an explicit witnessL42–42

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

  1. L42
    exists n
08Separate the logical casesL43–43

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

  1. L43
    split
09Use earlier factsL44–52

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

  1. L44
    specialize beta_horner_derivative_value_projection b
  2. L45
    specialize beta_horner_derivative_value_projection c
  3. L46
    specialize beta_horner_derivative_value_projection a
  4. L47
    specialize beta_horner_derivative_value_projection l
  5. L48
    specialize beta_horner_derivative_value_projection n
  6. L49
    specialize beta_horner_derivative_value_projection d
  7. L50
    apply beta_horner_derivative_value_projection
  8. L51
    exact hpair
  9. L52
    exact hroot
10Fix variables and assumptionsL53–54

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

  1. L53
    intro q
  2. L54
    intro hpower
11Establish hprevious_powerL55–62

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor decompose.

  1. L55
    have hprevious_power : ∃ u. Pow(p,j,u) ∧ q = u · pDefinitions: Pow
  2. L56
    specialize pow_successor_decompose p
  3. L57
    specialize pow_successor_decompose j
  4. L58
    specialize pow_successor_decompose (S j)
  5. L59
    specialize pow_successor_decompose q
  6. L60
    apply pow_successor_decompose
  7. L61
    refl
  8. L62
    exact hpower
12Separate the logical casesL63–64

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

  1. L63
    cases hprevious_power
  2. L64
    cases hprevious_power_witness
13Establish hxL65–74

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

  1. L65
    have hx : ~(x = 0)
  2. L66
    intro hzero
  3. L67
    specialize pow_nonzero_of_one_le p
  4. L68
    specialize pow_nonzero_of_one_le j
  5. L69
    specialize pow_nonzero_of_one_le x
  6. L70
    apply pow_nonzero_of_one_le
  7. L71
    specialize one_le_of_ne_zero p
  8. L72
    apply one_le_of_ne_zero
  9. L73
    exact hp
  10. L74
    exact hprevious_power_witness_left
14Use earlier factsL75–75

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

  1. L75
    exact hzero
15Establish hnonzeroL76–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul ne zero.

  1. L76
    have hnonzero : ~(m * x = 0)
  2. L77
    intro hzero
  3. L78
    specialize mul_ne_zero m
  4. L79
    specialize mul_ne_zero x
  5. L80
    apply mul_ne_zero
  6. L81
    exact hm
  7. L82
    exact hx
  8. L83
    exact hzero
16Establish hcurrent_factorL84–86

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

  1. L84
    have hcurrent_factor : m * x = p * (s * x)
  2. L85
    rewrite hfactor
  3. L86
    apply mul_assoc
17Establish hML87–96

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

  1. L87
    have hM : m * q = p * (m * x)
  2. L88
    rewrite hprevious_power_witness_right
  3. L89
    trans (m * x) * p
  4. L90
    symm
  5. L91
    apply mul_assoc
  6. L92
    apply mul_comm
  7. L93
    rewrite hM
  8. L94
    rewrite hM
  9. L95
    rewrite hM
  10. L96
    rewrite hM
18Calculate and transport equalitiesL97–98

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

  1. L97
    rewrite hM
  2. L98
    rewrite hM
19Establish hpreviousL99–102

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

  1. L99
    have hprevious : ∃ r. CanonicalHornerLift(b,c,l,m,a,m · x,r) ∧ (∀ y. CanonicalHornerLift(b,c,l,m,a,m · x,y) → y = r)Definitions: CanonicalHornerLift
  2. L100
    specialize IH x
  3. L101
    apply IH
  4. L102
    exact hprevious_power_witness_left
20Separate the logical casesL103–104

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

  1. L103
    cases hprevious
  2. L104
    cases hprevious_witness
21Establish hsimpleL105–114

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

  1. L105
    have hsimple : SimpleHornerRoot(b,c,x1,l,m · x,p)Definitions: SimpleHornerRoot
  2. L106
    specialize beta_horner_simple_lift_preserves_simplicity b
  3. L107
    specialize beta_horner_simple_lift_preserves_simplicity c
  4. L108
    specialize beta_horner_simple_lift_preserves_simplicity a
  5. L109
    specialize beta_horner_simple_lift_preserves_simplicity l
  6. L110
    specialize beta_horner_simple_lift_preserves_simplicity n
  7. L111
    specialize beta_horner_simple_lift_preserves_simplicity d
  8. L112
    specialize beta_horner_simple_lift_preserves_simplicity m
  9. L113
    specialize beta_horner_simple_lift_preserves_simplicity p
  10. L114
    specialize beta_horner_simple_lift_preserves_simplicity s
22Use earlier factsL115–122

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

  1. L115
    specialize beta_horner_simple_lift_preserves_simplicity (m * x)
  2. L116
    specialize beta_horner_simple_lift_preserves_simplicity x1
  3. L117
    apply beta_horner_simple_lift_preserves_simplicity
  4. L118
    exact hp
  5. L119
    exact hpair
  6. L120
    exact hcop
  7. L121
    exact hfactor
  8. L122
    exact hprevious_witness_left
23Separate the logical casesL123–126

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

  1. L123
    cases hsimple
  2. L124
    cases hsimple_witness
  3. L125
    cases hsimple_witness_witness
  4. L126
    cases hsimple_witness_witness_right
24Establish hnextL127–136

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

  1. L127
    have hnext : ∃ r. CanonicalHornerLift(b,c,l,m · x,x1,p · (m · x),r) ∧ (∀ y. CanonicalHornerLift(b,c,l,m · x,x1,p · (m · x),y) → y = r)Definitions: CanonicalHornerLift
  2. L128
    specialize beta_horner_simple_root_hensel_lift_exists_unique b
  3. L129
    specialize beta_horner_simple_root_hensel_lift_exists_unique c
  4. L130
    specialize beta_horner_simple_root_hensel_lift_exists_unique x1
  5. L131
    specialize beta_horner_simple_root_hensel_lift_exists_unique l
  6. L132
    specialize beta_horner_simple_root_hensel_lift_exists_unique x2
  7. L133
    specialize beta_horner_simple_root_hensel_lift_exists_unique x3
  8. L134
    specialize beta_horner_simple_root_hensel_lift_exists_unique (m * x)
  9. L135
    specialize beta_horner_simple_root_hensel_lift_exists_unique p
  10. L136
    specialize beta_horner_simple_root_hensel_lift_exists_unique (s * x)
25Use earlier factsL137–143

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

  1. L137
    apply beta_horner_simple_root_hensel_lift_exists_unique
  2. L138
    exact hp
  3. L139
    exact hnonzero
  4. L140
    exact hsimple_witness_witness_left
  5. L141
    exact hcurrent_factor
  6. L142
    exact hsimple_witness_witness_right_left
  7. L143
    exact hsimple_witness_witness_right_right
26Separate the logical casesL144–149

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

  1. L144
    cases hnext
  2. L145
    cases hnext_witness
  3. L146
    cases hnext_witness_left
  4. L147
    cases hnext_witness_left_right
  5. L148
    cases hprevious_witness_left
  6. L149
    cases hprevious_witness_left_right
27Construct an explicit witnessL150–150

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

  1. L150
    exists x4
28Separate the logical casesL151–152

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

  1. L151
    split
  2. L152
    split
29Use earlier factsL153–153

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

  1. L153
    exact hnext_witness_left_left
30Separate the logical casesL154–154

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

  1. L154
    split
31Use earlier factsL155–164

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

  1. L155
    specialize mod_eq_trans m
  2. L156
    specialize mod_eq_trans x4
  3. L157
    specialize mod_eq_trans x1
  4. L158
    specialize mod_eq_trans a
  5. L159
    apply mod_eq_trans
  6. L160
    specialize mod_eq_of_mod_eq_multiple m
  7. L161
    specialize mod_eq_of_mod_eq_multiple (m * x)
  8. L162
    specialize mod_eq_of_mod_eq_multiple x4
  9. L163
    specialize mod_eq_of_mod_eq_multiple x1
  10. L164
    apply mod_eq_of_mod_eq_multiple
32Construct an explicit witnessL165–165

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

  1. L165
    exists x
33Calculate and transport equalitiesL166–166

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

  1. L166
    refl
34Use earlier factsL167–169

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

  1. L167
    exact hnext_witness_left_right_left
  2. L168
    exact hprevious_witness_left_right_left
  3. L169
    exact hnext_witness_left_right_right
35Fix variables and assumptionsL170–171

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

  1. L170
    intro z
  2. L171
    intro hz
36Separate the logical casesL172–173

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

  1. L172
    cases hz
  2. L173
    cases hz_right
37Establish hresidueL174–178

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hensel canonical residue exists.

  1. L174
    have hresidue : exists r. ((exists hpl_gap_bound. hpl_gap_bound + S (r) = (m * x)) /\ (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. z + (m * x) * hgcrt_mod_left_hpl_mod = r + (m * x) * hgcrt_mod_right_hpl_mod))
  2. L175
    specialize hensel_canonical_residue_exists (m * x)
  3. L176
    specialize hensel_canonical_residue_exists z
  4. L177
    apply hensel_canonical_residue_exists
  5. L178
    exact hnonzero
38Separate the logical casesL179–180

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

  1. L179
    cases hresidue
  2. L180
    cases hresidue_witness
39Establish hroot_previousL181–188

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner root mod weaken.

  1. L181
    have hroot_previous : HornerRootModulo(b,c,z,l,m · x)Definitions: HornerRootModulo
  2. L182
    specialize beta_horner_root_mod_weaken b
  3. L183
    specialize beta_horner_root_mod_weaken c
  4. L184
    specialize beta_horner_root_mod_weaken z
  5. L185
    specialize beta_horner_root_mod_weaken l
  6. L186
    specialize beta_horner_root_mod_weaken (m * x)
  7. L187
    specialize beta_horner_root_mod_weaken (p * (m * x))
  8. L188
    apply beta_horner_root_mod_weaken
40Construct an explicit witnessL189–189

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

  1. L189
    exists p
41Use earlier factsL190–191

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

  1. L190
    apply mul_comm
  2. L191
    exact hz_right_right
42Establish hroot_representativeL192–201

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner root mod transport.

  1. L192
    have hroot_representative : HornerRootModulo(b,c,x5,l,m · x)Definitions: HornerRootModulo
  2. L193
    specialize beta_horner_root_mod_transport b
  3. L194
    specialize beta_horner_root_mod_transport c
  4. L195
    specialize beta_horner_root_mod_transport z
  5. L196
    specialize beta_horner_root_mod_transport x5
  6. L197
    specialize beta_horner_root_mod_transport l
  7. L198
    specialize beta_horner_root_mod_transport (m * x)
  8. L199
    apply beta_horner_root_mod_transport
  9. L200
    exact hresidue_witness_right
  10. L201
    exact hroot_previous
43Establish hsame_previousL202–204

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprevious witness right.

  1. L202
    have hsame_previous : x5 = x1
  2. L203
    specialize hprevious_witness_right x5
  3. L204
    apply hprevious_witness_right
44Separate the logical casesL205–205

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

  1. L205
    split
45Use earlier factsL206–206

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

  1. L206
    exact hresidue_witness_left
46Separate the logical casesL207–207

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

  1. L207
    split
47Use earlier factsL208–217

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

  1. L208
    specialize mod_eq_trans m
  2. L209
    specialize mod_eq_trans x5
  3. L210
    specialize mod_eq_trans z
  4. L211
    specialize mod_eq_trans a
  5. L212
    apply mod_eq_trans
  6. L213
    specialize mod_eq_of_mod_eq_multiple m
  7. L214
    specialize mod_eq_of_mod_eq_multiple (m * x)
  8. L215
    specialize mod_eq_of_mod_eq_multiple x5
  9. L216
    specialize mod_eq_of_mod_eq_multiple z
  10. L217
    apply mod_eq_of_mod_eq_multiple
48Construct an explicit witnessL218–218

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

  1. L218
    exists x
49Calculate and transport equalitiesL219–219

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

  1. L219
    refl
50Use earlier factsL220–228

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

  1. L220
    specialize mod_eq_symm (m * x)
  2. L221
    specialize mod_eq_symm z
  3. L222
    specialize mod_eq_symm x5
  4. L223
    apply mod_eq_symm
  5. L224
    exact hresidue_witness_right
  6. L225
    exact hz_right_left
  7. L226
    exact hroot_representative
  8. L227
    specialize hnext_witness_right z
  9. L228
    apply hnext_witness_right
51Separate the logical casesL229–229

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

  1. L229
    split
52Use earlier factsL230–230

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

  1. L230
    exact hz_left
53Separate the logical casesL231–231

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

  1. L231
    split
54Calculate and transport equalitiesL232–232

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

  1. L232
    rewrite <- hsame_previous
55Use earlier factsL233–234

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

  1. L233
    exact hresidue_witness_right
  2. L234
    exact hz_right_right

Library-wide reading audit

Original exact command ledger · 234 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro l
  5. 0005intro n
  6. 0006intro d
  7. 0007intro m
  8. 0008intro p
  9. 0009intro s
  10. 0010intro hp
  11. 0011intro hm
  12. 0012intro hpair
  13. 0013intro hfactor
  14. 0014intro hroot
  15. 0015intro hcop
  16. 0016induction j
  17. 0017intro q
  18. 0018intro hpower
  19. 0019have hq : q = 1
  20. 0020specialize pow_zero p
  21. 0021specialize pow_zero 0
  22. 0022specialize pow_zero q
  23. 0023apply pow_zero
  24. 0024refl
  25. 0025exact hpower
  26. 0026have hM : m * q = m
  27. 0027rewrite hq
  28. 0028apply mul_one
  29. 0029rewrite hM
  30. 0030rewrite hM
  31. 0031rewrite hM
  32. 0032rewrite hM
  33. 0033rewrite hM
  34. 0034rewrite hM
  35. 0035specialize hensel_canonical_horner_root_exists_unique b
  36. 0036specialize hensel_canonical_horner_root_exists_unique c
  37. 0037specialize hensel_canonical_horner_root_exists_unique a
  38. 0038specialize hensel_canonical_horner_root_exists_unique l
  39. 0039specialize hensel_canonical_horner_root_exists_unique m
  40. 0040apply hensel_canonical_horner_root_exists_unique
  41. 0041exact hm
  42. 0042exists n
  43. 0043split
  44. 0044specialize beta_horner_derivative_value_projection b
  45. 0045specialize beta_horner_derivative_value_projection c
  46. 0046specialize beta_horner_derivative_value_projection a
  47. 0047specialize beta_horner_derivative_value_projection l
  48. 0048specialize beta_horner_derivative_value_projection n
  49. 0049specialize beta_horner_derivative_value_projection d
  50. 0050apply beta_horner_derivative_value_projection
  51. 0051exact hpair
  52. 0052exact hroot
  53. 0053intro q
  54. 0054intro hpower
  55. 0055have hprevious_power : exists u. (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 = 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 (u) = S ((S (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 (j)) * pa_v_hpl_power_product) + (u))) /\ 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 = 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)))))))) /\ q = u * p
  56. 0056specialize pow_successor_decompose p
  57. 0057specialize pow_successor_decompose j
  58. 0058specialize pow_successor_decompose (S j)
  59. 0059specialize pow_successor_decompose q
  60. 0060apply pow_successor_decompose
  61. 0061refl
  62. 0062exact hpower
  63. 0063cases hprevious_power
  64. 0064cases hprevious_power_witness
  65. 0065have hx : ~(x = 0)
  66. 0066intro hzero
  67. 0067specialize pow_nonzero_of_one_le p
  68. 0068specialize pow_nonzero_of_one_le j
  69. 0069specialize pow_nonzero_of_one_le x
  70. 0070apply pow_nonzero_of_one_le
  71. 0071specialize one_le_of_ne_zero p
  72. 0072apply one_le_of_ne_zero
  73. 0073exact hp
  74. 0074exact hprevious_power_witness_left
  75. 0075exact hzero
  76. 0076have hnonzero : ~(m * x = 0)
  77. 0077intro hzero
  78. 0078specialize mul_ne_zero m
  79. 0079specialize mul_ne_zero x
  80. 0080apply mul_ne_zero
  81. 0081exact hm
  82. 0082exact hx
  83. 0083exact hzero
  84. 0084have hcurrent_factor : m * x = p * (s * x)
  85. 0085rewrite hfactor
  86. 0086apply mul_assoc
  87. 0087have hM : m * q = p * (m * x)
  88. 0088rewrite hprevious_power_witness_right
  89. 0089trans (m * x) * p
  90. 0090symm
  91. 0091apply mul_assoc
  92. 0092apply mul_comm
  93. 0093rewrite hM
  94. 0094rewrite hM
  95. 0095rewrite hM
  96. 0096rewrite hM
  97. 0097rewrite hM
  98. 0098rewrite hM
  99. 0099have hprevious : exists r. ((((exists hpl_gap_lift. hpl_gap_lift + S (r) = (m * x)) /\ ((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 hpl_value_lift. ((exists ff_u_ph_hpl_lift ff_v_ph_hpl_lift. ((((exists fs_h_ph_hpl_lift_body_start. fs_h_ph_hpl_lift_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_start. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_start * S ((S (0)) * ff_v_ph_hpl_lift) + (0))) /\ ((((exists fs_h_ph_hpl_lift_body_terminal. fs_h_ph_hpl_lift_body_terminal + S (hpl_value_lift) = S ((S (l)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_terminal. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_terminal * S ((S (l)) * ff_v_ph_hpl_lift) + (hpl_value_lift))) /\ forall ff_i_ph_hpl_lift_body_steps. (exists ph_bound_hpl_lift_body_steps. ph_bound_hpl_lift_body_steps + S ff_i_ph_hpl_lift_body_steps = l) -> exists ff_coefficient_ph_hpl_lift_body_steps ff_previous_ph_hpl_lift_body_steps ff_current_ph_hpl_lift_body_steps. ((((exists fs_h_ph_hpl_lift_body_steps_coefficient. fs_h_ph_hpl_lift_body_steps_coefficient + S (ff_coefficient_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * c)) /\ exists fs_q_ph_hpl_lift_body_steps_coefficient. b = fs_q_ph_hpl_lift_body_steps_coefficient * S ((S (ff_i_ph_hpl_lift_body_steps)) * c) + (ff_coefficient_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_before. fs_h_ph_hpl_lift_body_steps_before + S (ff_previous_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_before. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_before * S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_previous_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_after. fs_h_ph_hpl_lift_body_steps_after + S (ff_current_ph_hpl_lift_body_steps) = S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_after. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_after * S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_current_ph_hpl_lift_body_steps))) /\ ff_current_ph_hpl_lift_body_steps = ff_previous_ph_hpl_lift_body_steps * r + ff_coefficient_ph_hpl_lift_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. hpl_value_lift + (m * x) * hgcrt_mod_left_hpl_lift = 0 + (m * x) * hgcrt_mod_right_hpl_lift)))))) /\ forall z. (((exists hpl_gap_lift. hpl_gap_lift + S (z) = (m * x)) /\ ((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 hpl_value_lift. ((exists ff_u_ph_hpl_lift ff_v_ph_hpl_lift. ((((exists fs_h_ph_hpl_lift_body_start. fs_h_ph_hpl_lift_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_start. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_start * S ((S (0)) * ff_v_ph_hpl_lift) + (0))) /\ ((((exists fs_h_ph_hpl_lift_body_terminal. fs_h_ph_hpl_lift_body_terminal + S (hpl_value_lift) = S ((S (l)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_terminal. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_terminal * S ((S (l)) * ff_v_ph_hpl_lift) + (hpl_value_lift))) /\ forall ff_i_ph_hpl_lift_body_steps. (exists ph_bound_hpl_lift_body_steps. ph_bound_hpl_lift_body_steps + S ff_i_ph_hpl_lift_body_steps = l) -> exists ff_coefficient_ph_hpl_lift_body_steps ff_previous_ph_hpl_lift_body_steps ff_current_ph_hpl_lift_body_steps. ((((exists fs_h_ph_hpl_lift_body_steps_coefficient. fs_h_ph_hpl_lift_body_steps_coefficient + S (ff_coefficient_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * c)) /\ exists fs_q_ph_hpl_lift_body_steps_coefficient. b = fs_q_ph_hpl_lift_body_steps_coefficient * S ((S (ff_i_ph_hpl_lift_body_steps)) * c) + (ff_coefficient_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_before. fs_h_ph_hpl_lift_body_steps_before + S (ff_previous_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_before. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_before * S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_previous_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_after. fs_h_ph_hpl_lift_body_steps_after + S (ff_current_ph_hpl_lift_body_steps) = S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_after. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_after * S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_current_ph_hpl_lift_body_steps))) /\ ff_current_ph_hpl_lift_body_steps = ff_previous_ph_hpl_lift_body_steps * z + ff_coefficient_ph_hpl_lift_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. hpl_value_lift + (m * x) * hgcrt_mod_left_hpl_lift = 0 + (m * x) * hgcrt_mod_right_hpl_lift)))))) -> z = r)
  100. 0100specialize IH x
  101. 0101apply IH
  102. 0102exact hprevious_power_witness_left
  103. 0103cases hprevious
  104. 0104cases hprevious_witness
  105. 0105have hsimple : exists hpl_value_simple hpl_derivative_simple. ((exists ff_u_hd_hpl_simple ff_v_hd_hpl_simple ff_d_hd_hpl_simple ff_e_hd_hpl_simple. ((((((exists fs_h_ph_hd_hpl_simple_body_value_start. fs_h_ph_hd_hpl_simple_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_value_start. ff_u_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_value_start * S ((S (0)) * ff_v_hd_hpl_simple) + (0))) /\ ((((exists fs_h_ph_hd_hpl_simple_body_value_terminal. fs_h_ph_hd_hpl_simple_body_value_terminal + S (hpl_value_simple) = S ((S (l)) * ff_v_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_value_terminal. ff_u_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_simple) + (hpl_value_simple))) /\ forall ff_i_ph_hd_hpl_simple_body_value_steps. (exists ph_bound_hd_hpl_simple_body_value_steps. ph_bound_hd_hpl_simple_body_value_steps + S ff_i_ph_hd_hpl_simple_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_simple_body_value_steps ff_previous_ph_hd_hpl_simple_body_value_steps ff_current_ph_hd_hpl_simple_body_value_steps. ((((exists fs_h_ph_hd_hpl_simple_body_value_steps_coefficient. fs_h_ph_hd_hpl_simple_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_simple_body_value_steps) = S ((S (ff_i_ph_hd_hpl_simple_body_value_steps)) * c)) /\ exists fs_q_ph_hd_hpl_simple_body_value_steps_coefficient. b = fs_q_ph_hd_hpl_simple_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_simple_body_value_steps)) * c) + (ff_coefficient_ph_hd_hpl_simple_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_simple_body_value_steps_before. fs_h_ph_hd_hpl_simple_body_value_steps_before + S (ff_previous_ph_hd_hpl_simple_body_value_steps) = S ((S (ff_i_ph_hd_hpl_simple_body_value_steps)) * ff_v_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_value_steps_before. ff_u_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_simple_body_value_steps)) * ff_v_hd_hpl_simple) + (ff_previous_ph_hd_hpl_simple_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_simple_body_value_steps_after. fs_h_ph_hd_hpl_simple_body_value_steps_after + S (ff_current_ph_hd_hpl_simple_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_simple_body_value_steps)) * ff_v_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_value_steps_after. ff_u_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_simple_body_value_steps)) * ff_v_hd_hpl_simple) + (ff_current_ph_hd_hpl_simple_body_value_steps))) /\ ff_current_ph_hd_hpl_simple_body_value_steps = ff_previous_ph_hd_hpl_simple_body_value_steps * x1 + ff_coefficient_ph_hd_hpl_simple_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_simple_body_derivative_start. fs_h_ph_hd_hpl_simple_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_derivative_start. ff_d_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_simple) + (0))) /\ ((((exists fs_h_ph_hd_hpl_simple_body_derivative_terminal. fs_h_ph_hd_hpl_simple_body_derivative_terminal + S (hpl_derivative_simple) = S ((S (l)) * ff_e_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_derivative_terminal. ff_d_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_simple) + (hpl_derivative_simple))) /\ forall ff_i_ph_hd_hpl_simple_body_derivative_steps. (exists ph_bound_hd_hpl_simple_body_derivative_steps. ph_bound_hd_hpl_simple_body_derivative_steps + S ff_i_ph_hd_hpl_simple_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_simple_body_derivative_steps ff_previous_ph_hd_hpl_simple_body_derivative_steps ff_current_ph_hd_hpl_simple_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_simple_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_simple_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_simple_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_simple_body_derivative_steps)) * ff_v_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_derivative_steps_coefficient. ff_u_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_simple_body_derivative_steps)) * ff_v_hd_hpl_simple) + (ff_coefficient_ph_hd_hpl_simple_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_simple_body_derivative_steps_before. fs_h_ph_hd_hpl_simple_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_simple_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_simple_body_derivative_steps)) * ff_e_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_derivative_steps_before. ff_d_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_simple_body_derivative_steps)) * ff_e_hd_hpl_simple) + (ff_previous_ph_hd_hpl_simple_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_simple_body_derivative_steps_after. fs_h_ph_hd_hpl_simple_body_derivative_steps_after + S (ff_current_ph_hd_hpl_simple_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_simple_body_derivative_steps)) * ff_e_hd_hpl_simple)) /\ exists fs_q_ph_hd_hpl_simple_body_derivative_steps_after. ff_d_hd_hpl_simple = fs_q_ph_hd_hpl_simple_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_simple_body_derivative_steps)) * ff_e_hd_hpl_simple) + (ff_current_ph_hd_hpl_simple_body_derivative_steps))) /\ ff_current_ph_hd_hpl_simple_body_derivative_steps = ff_previous_ph_hd_hpl_simple_body_derivative_steps * x1 + ff_coefficient_ph_hd_hpl_simple_body_derivative_steps)))))))) /\ ((exists hgcrt_mod_left_hpl_simple hgcrt_mod_right_hpl_simple. hpl_value_simple + (m * x) * hgcrt_mod_left_hpl_simple = 0 + (m * x) * hgcrt_mod_right_hpl_simple) /\ (forall hmi_divisor_hpl_simple. (exists hmi_left_factor_hpl_simple. hpl_derivative_simple = hmi_divisor_hpl_simple * hmi_left_factor_hpl_simple) -> (exists hmi_right_factor_hpl_simple. p = hmi_divisor_hpl_simple * hmi_right_factor_hpl_simple) -> hmi_divisor_hpl_simple = 1)))
  106. 0106specialize beta_horner_simple_lift_preserves_simplicity b
  107. 0107specialize beta_horner_simple_lift_preserves_simplicity c
  108. 0108specialize beta_horner_simple_lift_preserves_simplicity a
  109. 0109specialize beta_horner_simple_lift_preserves_simplicity l
  110. 0110specialize beta_horner_simple_lift_preserves_simplicity n
  111. 0111specialize beta_horner_simple_lift_preserves_simplicity d
  112. 0112specialize beta_horner_simple_lift_preserves_simplicity m
  113. 0113specialize beta_horner_simple_lift_preserves_simplicity p
  114. 0114specialize beta_horner_simple_lift_preserves_simplicity s
  115. 0115specialize beta_horner_simple_lift_preserves_simplicity (m * x)
  116. 0116specialize beta_horner_simple_lift_preserves_simplicity x1
  117. 0117apply beta_horner_simple_lift_preserves_simplicity
  118. 0118exact hp
  119. 0119exact hpair
  120. 0120exact hcop
  121. 0121exact hfactor
  122. 0122exact hprevious_witness_left
  123. 0123cases hsimple
  124. 0124cases hsimple_witness
  125. 0125cases hsimple_witness_witness
  126. 0126cases hsimple_witness_witness_right
  127. 0127have hnext : exists r. ((((exists hpl_gap_lift. hpl_gap_lift + S (r) = (p * (m * x))) /\ ((exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. r + (m * x) * hgcrt_mod_left_hpl_lift = x1 + (m * x) * hgcrt_mod_right_hpl_lift) /\ (exists hpl_value_lift. ((exists ff_u_ph_hpl_lift ff_v_ph_hpl_lift. ((((exists fs_h_ph_hpl_lift_body_start. fs_h_ph_hpl_lift_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_start. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_start * S ((S (0)) * ff_v_ph_hpl_lift) + (0))) /\ ((((exists fs_h_ph_hpl_lift_body_terminal. fs_h_ph_hpl_lift_body_terminal + S (hpl_value_lift) = S ((S (l)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_terminal. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_terminal * S ((S (l)) * ff_v_ph_hpl_lift) + (hpl_value_lift))) /\ forall ff_i_ph_hpl_lift_body_steps. (exists ph_bound_hpl_lift_body_steps. ph_bound_hpl_lift_body_steps + S ff_i_ph_hpl_lift_body_steps = l) -> exists ff_coefficient_ph_hpl_lift_body_steps ff_previous_ph_hpl_lift_body_steps ff_current_ph_hpl_lift_body_steps. ((((exists fs_h_ph_hpl_lift_body_steps_coefficient. fs_h_ph_hpl_lift_body_steps_coefficient + S (ff_coefficient_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * c)) /\ exists fs_q_ph_hpl_lift_body_steps_coefficient. b = fs_q_ph_hpl_lift_body_steps_coefficient * S ((S (ff_i_ph_hpl_lift_body_steps)) * c) + (ff_coefficient_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_before. fs_h_ph_hpl_lift_body_steps_before + S (ff_previous_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_before. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_before * S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_previous_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_after. fs_h_ph_hpl_lift_body_steps_after + S (ff_current_ph_hpl_lift_body_steps) = S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_after. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_after * S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_current_ph_hpl_lift_body_steps))) /\ ff_current_ph_hpl_lift_body_steps = ff_previous_ph_hpl_lift_body_steps * r + ff_coefficient_ph_hpl_lift_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. hpl_value_lift + (p * (m * x)) * hgcrt_mod_left_hpl_lift = 0 + (p * (m * x)) * hgcrt_mod_right_hpl_lift)))))) /\ forall z. (((exists hpl_gap_lift. hpl_gap_lift + S (z) = (p * (m * x))) /\ ((exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. z + (m * x) * hgcrt_mod_left_hpl_lift = x1 + (m * x) * hgcrt_mod_right_hpl_lift) /\ (exists hpl_value_lift. ((exists ff_u_ph_hpl_lift ff_v_ph_hpl_lift. ((((exists fs_h_ph_hpl_lift_body_start. fs_h_ph_hpl_lift_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_start. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_start * S ((S (0)) * ff_v_ph_hpl_lift) + (0))) /\ ((((exists fs_h_ph_hpl_lift_body_terminal. fs_h_ph_hpl_lift_body_terminal + S (hpl_value_lift) = S ((S (l)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_terminal. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_terminal * S ((S (l)) * ff_v_ph_hpl_lift) + (hpl_value_lift))) /\ forall ff_i_ph_hpl_lift_body_steps. (exists ph_bound_hpl_lift_body_steps. ph_bound_hpl_lift_body_steps + S ff_i_ph_hpl_lift_body_steps = l) -> exists ff_coefficient_ph_hpl_lift_body_steps ff_previous_ph_hpl_lift_body_steps ff_current_ph_hpl_lift_body_steps. ((((exists fs_h_ph_hpl_lift_body_steps_coefficient. fs_h_ph_hpl_lift_body_steps_coefficient + S (ff_coefficient_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * c)) /\ exists fs_q_ph_hpl_lift_body_steps_coefficient. b = fs_q_ph_hpl_lift_body_steps_coefficient * S ((S (ff_i_ph_hpl_lift_body_steps)) * c) + (ff_coefficient_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_before. fs_h_ph_hpl_lift_body_steps_before + S (ff_previous_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_before. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_before * S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_previous_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_after. fs_h_ph_hpl_lift_body_steps_after + S (ff_current_ph_hpl_lift_body_steps) = S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_after. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_after * S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_current_ph_hpl_lift_body_steps))) /\ ff_current_ph_hpl_lift_body_steps = ff_previous_ph_hpl_lift_body_steps * z + ff_coefficient_ph_hpl_lift_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. hpl_value_lift + (p * (m * x)) * hgcrt_mod_left_hpl_lift = 0 + (p * (m * x)) * hgcrt_mod_right_hpl_lift)))))) -> z = r)
  128. 0128specialize beta_horner_simple_root_hensel_lift_exists_unique b
  129. 0129specialize beta_horner_simple_root_hensel_lift_exists_unique c
  130. 0130specialize beta_horner_simple_root_hensel_lift_exists_unique x1
  131. 0131specialize beta_horner_simple_root_hensel_lift_exists_unique l
  132. 0132specialize beta_horner_simple_root_hensel_lift_exists_unique x2
  133. 0133specialize beta_horner_simple_root_hensel_lift_exists_unique x3
  134. 0134specialize beta_horner_simple_root_hensel_lift_exists_unique (m * x)
  135. 0135specialize beta_horner_simple_root_hensel_lift_exists_unique p
  136. 0136specialize beta_horner_simple_root_hensel_lift_exists_unique (s * x)
  137. 0137apply beta_horner_simple_root_hensel_lift_exists_unique
  138. 0138exact hp
  139. 0139exact hnonzero
  140. 0140exact hsimple_witness_witness_left
  141. 0141exact hcurrent_factor
  142. 0142exact hsimple_witness_witness_right_left
  143. 0143exact hsimple_witness_witness_right_right
  144. 0144cases hnext
  145. 0145cases hnext_witness
  146. 0146cases hnext_witness_left
  147. 0147cases hnext_witness_left_right
  148. 0148cases hprevious_witness_left
  149. 0149cases hprevious_witness_left_right
  150. 0150exists x4
  151. 0151split
  152. 0152split
  153. 0153exact hnext_witness_left_left
  154. 0154split
  155. 0155specialize mod_eq_trans m
  156. 0156specialize mod_eq_trans x4
  157. 0157specialize mod_eq_trans x1
  158. 0158specialize mod_eq_trans a
  159. 0159apply mod_eq_trans
  160. 0160specialize mod_eq_of_mod_eq_multiple m
  161. 0161specialize mod_eq_of_mod_eq_multiple (m * x)
  162. 0162specialize mod_eq_of_mod_eq_multiple x4
  163. 0163specialize mod_eq_of_mod_eq_multiple x1
  164. 0164apply mod_eq_of_mod_eq_multiple
  165. 0165exists x
  166. 0166refl
  167. 0167exact hnext_witness_left_right_left
  168. 0168exact hprevious_witness_left_right_left
  169. 0169exact hnext_witness_left_right_right
  170. 0170intro z
  171. 0171intro hz
  172. 0172cases hz
  173. 0173cases hz_right
  174. 0174have hresidue : exists r. ((exists hpl_gap_bound. hpl_gap_bound + S (r) = (m * x)) /\ (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. z + (m * x) * hgcrt_mod_left_hpl_mod = r + (m * x) * hgcrt_mod_right_hpl_mod))
  175. 0175specialize hensel_canonical_residue_exists (m * x)
  176. 0176specialize hensel_canonical_residue_exists z
  177. 0177apply hensel_canonical_residue_exists
  178. 0178exact hnonzero
  179. 0179cases hresidue
  180. 0180cases hresidue_witness
  181. 0181have hroot_previous : exists hpl_value_root. ((exists ff_u_ph_hpl_root ff_v_ph_hpl_root. ((((exists fs_h_ph_hpl_root_body_start. fs_h_ph_hpl_root_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_start. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_start * S ((S (0)) * ff_v_ph_hpl_root) + (0))) /\ ((((exists fs_h_ph_hpl_root_body_terminal. fs_h_ph_hpl_root_body_terminal + S (hpl_value_root) = S ((S (l)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_terminal. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_terminal * S ((S (l)) * ff_v_ph_hpl_root) + (hpl_value_root))) /\ forall ff_i_ph_hpl_root_body_steps. (exists ph_bound_hpl_root_body_steps. ph_bound_hpl_root_body_steps + S ff_i_ph_hpl_root_body_steps = l) -> exists ff_coefficient_ph_hpl_root_body_steps ff_previous_ph_hpl_root_body_steps ff_current_ph_hpl_root_body_steps. ((((exists fs_h_ph_hpl_root_body_steps_coefficient. fs_h_ph_hpl_root_body_steps_coefficient + S (ff_coefficient_ph_hpl_root_body_steps) = S ((S (ff_i_ph_hpl_root_body_steps)) * c)) /\ exists fs_q_ph_hpl_root_body_steps_coefficient. b = fs_q_ph_hpl_root_body_steps_coefficient * S ((S (ff_i_ph_hpl_root_body_steps)) * c) + (ff_coefficient_ph_hpl_root_body_steps))) /\ ((((exists fs_h_ph_hpl_root_body_steps_before. fs_h_ph_hpl_root_body_steps_before + S (ff_previous_ph_hpl_root_body_steps) = S ((S (ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_steps_before. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_steps_before * S ((S (ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root) + (ff_previous_ph_hpl_root_body_steps))) /\ ((((exists fs_h_ph_hpl_root_body_steps_after. fs_h_ph_hpl_root_body_steps_after + S (ff_current_ph_hpl_root_body_steps) = S ((S (S ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_steps_after. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_steps_after * S ((S (S ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root) + (ff_current_ph_hpl_root_body_steps))) /\ ff_current_ph_hpl_root_body_steps = ff_previous_ph_hpl_root_body_steps * z + ff_coefficient_ph_hpl_root_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_root hgcrt_mod_right_hpl_root. hpl_value_root + (m * x) * hgcrt_mod_left_hpl_root = 0 + (m * x) * hgcrt_mod_right_hpl_root))
  182. 0182specialize beta_horner_root_mod_weaken b
  183. 0183specialize beta_horner_root_mod_weaken c
  184. 0184specialize beta_horner_root_mod_weaken z
  185. 0185specialize beta_horner_root_mod_weaken l
  186. 0186specialize beta_horner_root_mod_weaken (m * x)
  187. 0187specialize beta_horner_root_mod_weaken (p * (m * x))
  188. 0188apply beta_horner_root_mod_weaken
  189. 0189exists p
  190. 0190apply mul_comm
  191. 0191exact hz_right_right
  192. 0192have hroot_representative : exists hpl_value_root. ((exists ff_u_ph_hpl_root ff_v_ph_hpl_root. ((((exists fs_h_ph_hpl_root_body_start. fs_h_ph_hpl_root_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_start. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_start * S ((S (0)) * ff_v_ph_hpl_root) + (0))) /\ ((((exists fs_h_ph_hpl_root_body_terminal. fs_h_ph_hpl_root_body_terminal + S (hpl_value_root) = S ((S (l)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_terminal. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_terminal * S ((S (l)) * ff_v_ph_hpl_root) + (hpl_value_root))) /\ forall ff_i_ph_hpl_root_body_steps. (exists ph_bound_hpl_root_body_steps. ph_bound_hpl_root_body_steps + S ff_i_ph_hpl_root_body_steps = l) -> exists ff_coefficient_ph_hpl_root_body_steps ff_previous_ph_hpl_root_body_steps ff_current_ph_hpl_root_body_steps. ((((exists fs_h_ph_hpl_root_body_steps_coefficient. fs_h_ph_hpl_root_body_steps_coefficient + S (ff_coefficient_ph_hpl_root_body_steps) = S ((S (ff_i_ph_hpl_root_body_steps)) * c)) /\ exists fs_q_ph_hpl_root_body_steps_coefficient. b = fs_q_ph_hpl_root_body_steps_coefficient * S ((S (ff_i_ph_hpl_root_body_steps)) * c) + (ff_coefficient_ph_hpl_root_body_steps))) /\ ((((exists fs_h_ph_hpl_root_body_steps_before. fs_h_ph_hpl_root_body_steps_before + S (ff_previous_ph_hpl_root_body_steps) = S ((S (ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_steps_before. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_steps_before * S ((S (ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root) + (ff_previous_ph_hpl_root_body_steps))) /\ ((((exists fs_h_ph_hpl_root_body_steps_after. fs_h_ph_hpl_root_body_steps_after + S (ff_current_ph_hpl_root_body_steps) = S ((S (S ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_steps_after. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_steps_after * S ((S (S ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root) + (ff_current_ph_hpl_root_body_steps))) /\ ff_current_ph_hpl_root_body_steps = ff_previous_ph_hpl_root_body_steps * x5 + ff_coefficient_ph_hpl_root_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_root hgcrt_mod_right_hpl_root. hpl_value_root + (m * x) * hgcrt_mod_left_hpl_root = 0 + (m * x) * hgcrt_mod_right_hpl_root))
  193. 0193specialize beta_horner_root_mod_transport b
  194. 0194specialize beta_horner_root_mod_transport c
  195. 0195specialize beta_horner_root_mod_transport z
  196. 0196specialize beta_horner_root_mod_transport x5
  197. 0197specialize beta_horner_root_mod_transport l
  198. 0198specialize beta_horner_root_mod_transport (m * x)
  199. 0199apply beta_horner_root_mod_transport
  200. 0200exact hresidue_witness_right
  201. 0201exact hroot_previous
  202. 0202have hsame_previous : x5 = x1
  203. 0203specialize hprevious_witness_right x5
  204. 0204apply hprevious_witness_right
  205. 0205split
  206. 0206exact hresidue_witness_left
  207. 0207split
  208. 0208specialize mod_eq_trans m
  209. 0209specialize mod_eq_trans x5
  210. 0210specialize mod_eq_trans z
  211. 0211specialize mod_eq_trans a
  212. 0212apply mod_eq_trans
  213. 0213specialize mod_eq_of_mod_eq_multiple m
  214. 0214specialize mod_eq_of_mod_eq_multiple (m * x)
  215. 0215specialize mod_eq_of_mod_eq_multiple x5
  216. 0216specialize mod_eq_of_mod_eq_multiple z
  217. 0217apply mod_eq_of_mod_eq_multiple
  218. 0218exists x
  219. 0219refl
  220. 0220specialize mod_eq_symm (m * x)
  221. 0221specialize mod_eq_symm z
  222. 0222specialize mod_eq_symm x5
  223. 0223apply mod_eq_symm
  224. 0224exact hresidue_witness_right
  225. 0225exact hz_right_left
  226. 0226exact hroot_representative
  227. 0227specialize hnext_witness_right z
  228. 0228apply hnext_witness_right
  229. 0229split
  230. 0230exact hz_left
  231. 0231split
  232. 0232rewrite <- hsame_previous
  233. 0233exact hresidue_witness_right
  234. 0234exact hz_right_right