HD000F

beta_horner_derivative_linear

A genuine two-coefficient polynomial a*t+k has the exact decoded formal derivative a.

Alpha v34 checked-use · first admitted v24 · 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.

Historical partial components only: this chapter proves arbitrary natural polynomial values and unique formal derivatives. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical lifts, and every positive prime power. Full G095 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ t. ∀ n. ∀ z. HornerDerivative(b,c,t,2,n,z) → ∃ x. ∃ y. Beta(b,c,0,x) ∧ (Beta(b,c,1,y) ∧ (n = x · t + y ∧ z = x))

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

Definition DAG

Beta(b,c,i,x) · 2HornerDerivative(b,c,t,l,n,z) · 1

Actual proof prerequisites

beta_horner_derivative_successor_decomposebeta_horner_derivative_constantmul_zero_left · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall b c t n z. (exists ff_u_hd_linear ff_v_hd_linear ff_d_hd_linear ff_e_hd_linear. ((((((exists fs_h_ph_hd_linear_body_value_start. fs_h_ph_hd_linear_body_value_start + S (0) = S ((S (0)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_value_start. ff_u_hd_linear = fs_q_ph_hd_linear_body_value_start * S ((S (0)) * ff_v_hd_linear) + (0))) /\ ((((exists fs_h_ph_hd_linear_body_value_terminal. fs_h_ph_hd_linear_body_value_terminal + S (n) = S ((S (S S 0)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_value_terminal. ff_u_hd_linear = fs_q_ph_hd_linear_body_value_terminal * S ((S (S S 0)) * ff_v_hd_linear) + (n))) /\ forall ff_i_ph_hd_linear_body_value_steps. (exists ph_bound_hd_linear_body_value_steps. ph_bound_hd_linear_body_value_steps + S ff_i_ph_hd_linear_body_value_steps = S S 0) -> exists ff_coefficient_ph_hd_linear_body_value_steps ff_previous_ph_hd_linear_body_value_steps ff_current_ph_hd_linear_body_value_steps. ((((exists fs_h_ph_hd_linear_body_value_steps_coefficient. fs_h_ph_hd_linear_body_value_steps_coefficient + S (ff_coefficient_ph_hd_linear_body_value_steps) = S ((S (ff_i_ph_hd_linear_body_value_steps)) * c)) /\ exists fs_q_ph_hd_linear_body_value_steps_coefficient. b = fs_q_ph_hd_linear_body_value_steps_coefficient * S ((S (ff_i_ph_hd_linear_body_value_steps)) * c) + (ff_coefficient_ph_hd_linear_body_value_steps))) /\ ((((exists fs_h_ph_hd_linear_body_value_steps_before. fs_h_ph_hd_linear_body_value_steps_before + S (ff_previous_ph_hd_linear_body_value_steps) = S ((S (ff_i_ph_hd_linear_body_value_steps)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_value_steps_before. ff_u_hd_linear = fs_q_ph_hd_linear_body_value_steps_before * S ((S (ff_i_ph_hd_linear_body_value_steps)) * ff_v_hd_linear) + (ff_previous_ph_hd_linear_body_value_steps))) /\ ((((exists fs_h_ph_hd_linear_body_value_steps_after. fs_h_ph_hd_linear_body_value_steps_after + S (ff_current_ph_hd_linear_body_value_steps) = S ((S (S ff_i_ph_hd_linear_body_value_steps)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_value_steps_after. ff_u_hd_linear = fs_q_ph_hd_linear_body_value_steps_after * S ((S (S ff_i_ph_hd_linear_body_value_steps)) * ff_v_hd_linear) + (ff_current_ph_hd_linear_body_value_steps))) /\ ff_current_ph_hd_linear_body_value_steps = ff_previous_ph_hd_linear_body_value_steps * t + ff_coefficient_ph_hd_linear_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_linear_body_derivative_start. fs_h_ph_hd_linear_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_start. ff_d_hd_linear = fs_q_ph_hd_linear_body_derivative_start * S ((S (0)) * ff_e_hd_linear) + (0))) /\ ((((exists fs_h_ph_hd_linear_body_derivative_terminal. fs_h_ph_hd_linear_body_derivative_terminal + S (z) = S ((S (S S 0)) * ff_e_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_terminal. ff_d_hd_linear = fs_q_ph_hd_linear_body_derivative_terminal * S ((S (S S 0)) * ff_e_hd_linear) + (z))) /\ forall ff_i_ph_hd_linear_body_derivative_steps. (exists ph_bound_hd_linear_body_derivative_steps. ph_bound_hd_linear_body_derivative_steps + S ff_i_ph_hd_linear_body_derivative_steps = S S 0) -> exists ff_coefficient_ph_hd_linear_body_derivative_steps ff_previous_ph_hd_linear_body_derivative_steps ff_current_ph_hd_linear_body_derivative_steps. ((((exists fs_h_ph_hd_linear_body_derivative_steps_coefficient. fs_h_ph_hd_linear_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_linear_body_derivative_steps) = S ((S (ff_i_ph_hd_linear_body_derivative_steps)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_steps_coefficient. ff_u_hd_linear = fs_q_ph_hd_linear_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_linear_body_derivative_steps)) * ff_v_hd_linear) + (ff_coefficient_ph_hd_linear_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_linear_body_derivative_steps_before. fs_h_ph_hd_linear_body_derivative_steps_before + S (ff_previous_ph_hd_linear_body_derivative_steps) = S ((S (ff_i_ph_hd_linear_body_derivative_steps)) * ff_e_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_steps_before. ff_d_hd_linear = fs_q_ph_hd_linear_body_derivative_steps_before * S ((S (ff_i_ph_hd_linear_body_derivative_steps)) * ff_e_hd_linear) + (ff_previous_ph_hd_linear_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_linear_body_derivative_steps_after. fs_h_ph_hd_linear_body_derivative_steps_after + S (ff_current_ph_hd_linear_body_derivative_steps) = S ((S (S ff_i_ph_hd_linear_body_derivative_steps)) * ff_e_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_steps_after. ff_d_hd_linear = fs_q_ph_hd_linear_body_derivative_steps_after * S ((S (S ff_i_ph_hd_linear_body_derivative_steps)) * ff_e_hd_linear) + (ff_current_ph_hd_linear_body_derivative_steps))) /\ ff_current_ph_hd_linear_body_derivative_steps = ff_previous_ph_hd_linear_body_derivative_steps * t + ff_coefficient_ph_hd_linear_body_derivative_steps)))))))) -> exists a k. ((((exists fs_h_hd_linear_leading. fs_h_hd_linear_leading + S (a) = S ((S (0)) * c)) /\ exists fs_q_hd_linear_leading. b = fs_q_hd_linear_leading * S ((S (0)) * c) + (a))) /\ ((((exists fs_h_hd_linear_constant. fs_h_hd_linear_constant + S (k) = S ((S (S 0)) * c)) /\ exists fs_q_hd_linear_constant. b = fs_q_hd_linear_constant * S ((S (S 0)) * c) + (k))) /\ ((n = a * t + k) /\ z = a)))

Complete unchanged native tactic proof

All 51 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

51 script commands · 19 reading checkpoints · 2 local claims

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

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

Named ingredients (2)
beta horner derivative successor decomposebeta horner derivative constant

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–6

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro t
  4. L4
    intro n
  5. L5
    intro z
  6. L6
    intro hpair
02Establish hdecompositionL7–15

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

  1. L7
    have hdecomposition : ∃ a. ∃ r. ∃ q. Beta(b,c,1,a) ∧ (HornerDerivative(b,c,t,1,r,q) ∧ (n = r · t + a ∧ z = q · t + r))Definitions: BetaHornerDerivativeOriginal native command in the exact edition
  2. L8
    specialize beta_horner_derivative_successor_decompose b
  3. L9
    specialize beta_horner_derivative_successor_decompose c
  4. L10
    specialize beta_horner_derivative_successor_decompose t
  5. L11
    specialize beta_horner_derivative_successor_decompose (S 0)
  6. L12
    specialize beta_horner_derivative_successor_decompose n
  7. L13
    specialize beta_horner_derivative_successor_decompose z
  8. L14
    apply beta_horner_derivative_successor_decompose
  9. L15
    exact hpair
03Separate the logical casesL16–21

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

  1. L16
    cases hdecomposition
  2. L17
    cases hdecomposition_witness
  3. L18
    cases hdecomposition_witness_witness
  4. L19
    cases hdecomposition_witness_witness_witness
  5. L20
    cases hdecomposition_witness_witness_witness_right
  6. L21
    cases hdecomposition_witness_witness_witness_right_right
04Establish hconstantL22–29

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

  1. L22
    have hconstant : exists a. ((((exists fs_h_hd_linear_prefix_coefficient. fs_h_hd_linear_prefix_coefficient + S (a) = S ((S (0)) * c)) /\ exists fs_q_hd_linear_prefix_coefficient. b = fs_q_hd_linear_prefix_coefficient * S ((S (0)) * c) + (a))) /\ ((x1 = a) /\ x2 = 0))
  2. L23
    specialize beta_horner_derivative_constant b
  3. L24
    specialize beta_horner_derivative_constant c
  4. L25
    specialize beta_horner_derivative_constant t
  5. L26
    specialize beta_horner_derivative_constant x1
  6. L27
    specialize beta_horner_derivative_constant x2
  7. L28
    apply beta_horner_derivative_constant
  8. L29
    exact hdecomposition_witness_witness_witness_right_left
05Separate the logical casesL30–32

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

  1. L30
    cases hconstant
  2. L31
    cases hconstant_witness
  3. L32
    cases hconstant_witness_right
06Construct an explicit witnessL33–34

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

  1. L33
    exists x3
  2. L34
    exists x
07Separate the logical casesL35–35

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

  1. L35
    split
08Use earlier factsL36–36

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

  1. L36
    exact hconstant_witness_left
09Separate the logical casesL37–37

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

  1. L37
    split
10Use earlier factsL38–38

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

  1. L38
    exact hdecomposition_witness_witness_witness_left
11Separate the logical casesL39–39

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

  1. L39
    split
12Calculate and transport equalitiesL40–40

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

  1. L40
    trans x1 * t + x
13Use earlier factsL41–41

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

  1. L41
    exact hdecomposition_witness_witness_witness_right_right_left
14Calculate and transport equalitiesL42–44

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

  1. L42
    rewrite hconstant_witness_right_left
  2. L43
    refl
  3. L44
    trans x2 * t + x1
15Use earlier factsL45–45

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

  1. L45
    exact hdecomposition_witness_witness_witness_right_right_right
16Calculate and transport equalitiesL46–47

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

  1. L46
    rewrite hconstant_witness_right_right
  2. L47
    rewrite hconstant_witness_right_left
17Use earlier factsL48–48

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

  1. L48
    specialize mul_zero_left t
18Calculate and transport equalitiesL49–49

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

  1. L49
    rewrite mul_zero_left
19Use earlier factsL50–51

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

  1. L50
    specialize zero_add x3
  2. L51
    exact zero_add

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro n
  5. 0005intro z
  6. 0006intro hpair
  7. 0007have hdecomposition : exists a r q. ((((exists fs_h_hd_linear_step. fs_h_hd_linear_step + S (a) = S ((S (S 0)) * c)) /\ exists fs_q_hd_linear_step. b = fs_q_hd_linear_step * S ((S (S 0)) * c) + (a))) /\ ((exists ff_u_hd_linear_prefix ff_v_hd_linear_prefix ff_d_hd_linear_prefix ff_e_hd_linear_prefix. ((((((exists fs_h_ph_hd_linear_prefix_body_value_start. fs_h_ph_hd_linear_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_value_start. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_value_start * S ((S (0)) * ff_v_hd_linear_prefix) + (0))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_value_terminal. fs_h_ph_hd_linear_prefix_body_value_terminal + S (r) = S ((S (S 0)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_value_terminal. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_value_terminal * S ((S (S 0)) * ff_v_hd_linear_prefix) + (r))) /\ forall ff_i_ph_hd_linear_prefix_body_value_steps. (exists ph_bound_hd_linear_prefix_body_value_steps. ph_bound_hd_linear_prefix_body_value_steps + S ff_i_ph_hd_linear_prefix_body_value_steps = S 0) -> exists ff_coefficient_ph_hd_linear_prefix_body_value_steps ff_previous_ph_hd_linear_prefix_body_value_steps ff_current_ph_hd_linear_prefix_body_value_steps. ((((exists fs_h_ph_hd_linear_prefix_body_value_steps_coefficient. fs_h_ph_hd_linear_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_linear_prefix_body_value_steps) = S ((S (ff_i_ph_hd_linear_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_linear_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_linear_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_linear_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_linear_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_value_steps_before. fs_h_ph_hd_linear_prefix_body_value_steps_before + S (ff_previous_ph_hd_linear_prefix_body_value_steps) = S ((S (ff_i_ph_hd_linear_prefix_body_value_steps)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_value_steps_before. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_linear_prefix_body_value_steps)) * ff_v_hd_linear_prefix) + (ff_previous_ph_hd_linear_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_value_steps_after. fs_h_ph_hd_linear_prefix_body_value_steps_after + S (ff_current_ph_hd_linear_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_linear_prefix_body_value_steps)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_value_steps_after. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_linear_prefix_body_value_steps)) * ff_v_hd_linear_prefix) + (ff_current_ph_hd_linear_prefix_body_value_steps))) /\ ff_current_ph_hd_linear_prefix_body_value_steps = ff_previous_ph_hd_linear_prefix_body_value_steps * t + ff_coefficient_ph_hd_linear_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_linear_prefix_body_derivative_start. fs_h_ph_hd_linear_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_start. ff_d_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_linear_prefix) + (0))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_derivative_terminal. fs_h_ph_hd_linear_prefix_body_derivative_terminal + S (q) = S ((S (S 0)) * ff_e_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_terminal. ff_d_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_terminal * S ((S (S 0)) * ff_e_hd_linear_prefix) + (q))) /\ forall ff_i_ph_hd_linear_prefix_body_derivative_steps. (exists ph_bound_hd_linear_prefix_body_derivative_steps. ph_bound_hd_linear_prefix_body_derivative_steps + S ff_i_ph_hd_linear_prefix_body_derivative_steps = S 0) -> exists ff_coefficient_ph_hd_linear_prefix_body_derivative_steps ff_previous_ph_hd_linear_prefix_body_derivative_steps ff_current_ph_hd_linear_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_linear_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_linear_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_linear_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_steps_coefficient. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_v_hd_linear_prefix) + (ff_coefficient_ph_hd_linear_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_derivative_steps_before. fs_h_ph_hd_linear_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_linear_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_e_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_steps_before. ff_d_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_e_hd_linear_prefix) + (ff_previous_ph_hd_linear_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_derivative_steps_after. fs_h_ph_hd_linear_prefix_body_derivative_steps_after + S (ff_current_ph_hd_linear_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_e_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_steps_after. ff_d_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_e_hd_linear_prefix) + (ff_current_ph_hd_linear_prefix_body_derivative_steps))) /\ ff_current_ph_hd_linear_prefix_body_derivative_steps = ff_previous_ph_hd_linear_prefix_body_derivative_steps * t + ff_coefficient_ph_hd_linear_prefix_body_derivative_steps)))))))) /\ ((n = r * t + a) /\ z = q * t + r)))
  8. 0008specialize beta_horner_derivative_successor_decompose b
  9. 0009specialize beta_horner_derivative_successor_decompose c
  10. 0010specialize beta_horner_derivative_successor_decompose t
  11. 0011specialize beta_horner_derivative_successor_decompose (S 0)
  12. 0012specialize beta_horner_derivative_successor_decompose n
  13. 0013specialize beta_horner_derivative_successor_decompose z
  14. 0014apply beta_horner_derivative_successor_decompose
  15. 0015exact hpair
  16. 0016cases hdecomposition
  17. 0017cases hdecomposition_witness
  18. 0018cases hdecomposition_witness_witness
  19. 0019cases hdecomposition_witness_witness_witness
  20. 0020cases hdecomposition_witness_witness_witness_right
  21. 0021cases hdecomposition_witness_witness_witness_right_right
  22. 0022have hconstant : exists a. ((((exists fs_h_hd_linear_prefix_coefficient. fs_h_hd_linear_prefix_coefficient + S (a) = S ((S (0)) * c)) /\ exists fs_q_hd_linear_prefix_coefficient. b = fs_q_hd_linear_prefix_coefficient * S ((S (0)) * c) + (a))) /\ ((x1 = a) /\ x2 = 0))
  23. 0023specialize beta_horner_derivative_constant b
  24. 0024specialize beta_horner_derivative_constant c
  25. 0025specialize beta_horner_derivative_constant t
  26. 0026specialize beta_horner_derivative_constant x1
  27. 0027specialize beta_horner_derivative_constant x2
  28. 0028apply beta_horner_derivative_constant
  29. 0029exact hdecomposition_witness_witness_witness_right_left
  30. 0030cases hconstant
  31. 0031cases hconstant_witness
  32. 0032cases hconstant_witness_right
  33. 0033exists x3
  34. 0034exists x
  35. 0035split
  36. 0036exact hconstant_witness_left
  37. 0037split
  38. 0038exact hdecomposition_witness_witness_witness_left
  39. 0039split
  40. 0040trans x1 * t + x
  41. 0041exact hdecomposition_witness_witness_witness_right_right_left
  42. 0042rewrite hconstant_witness_right_left
  43. 0043refl
  44. 0044trans x2 * t + x1
  45. 0045exact hdecomposition_witness_witness_witness_right_right_right
  46. 0046rewrite hconstant_witness_right_right
  47. 0047rewrite hconstant_witness_right_left
  48. 0048specialize mul_zero_left t
  49. 0049rewrite mul_zero_left
  50. 0050specialize zero_add x3
  51. 0051exact zero_add