PG004E

polynomial_diagonal_left_constant_natural_sum

The actual finite natural sum equals k*a: construct its one-term sum and use the existing zero-tail invariant for every subsequent summand. The total need not itself be a canonical field coefficient.

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

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ k. ∀ kb. ∀ kc. ∀ ab. ∀ ac. ∀ L. ∀ i. ∀ a. ∀ db. ∀ dc. ∀ n. BetaAt(kb,kc,0,k) → Lt(i,L) → BetaAt(ab,ac,i,a) → PolynomialDiagonalPrefix(kb,kc,1,ab,ac,L,i,db,dc,S i) → Sum(db,dc,S i,n) → n = k · a

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

Definition DAG

PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) · 2PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 7Sum(b,c,l,z) · 3

Actual proof prerequisites

polynomial_diagonal_left_constant_first_termpolynomial_diagonal_left_unit_tail_termadd_succ_left · checked external prerequisitezero_add · checked external prerequisitesucc_le_succ · checked external prerequisitele_add_right · checked external prerequisitebeta_sum_exists · checked external prerequisitebeta_sum_succ_decompose · checked external prerequisitebeta_sum_zero · checked external prerequisitebeta_at_unique · checked external prerequisitepolynomial_zero_tail_natural_sum_invariant · checked external prerequisite
Original expanded first-order statement 
forall k kb kc ab ac L i a db dc n. (((exists ff_h_pfp_left_constant_sum_K. ff_h_pfp_left_constant_sum_K + S (k) = S ((S (0)) * kc)) /\ exists ff_q_pfp_left_constant_sum_K. kb = ff_q_pfp_left_constant_sum_K * S ((S (0)) * kc) + (k))) -> (exists pfa_gap_left_constant_sum_index. pfa_gap_left_constant_sum_index + S (i) = (L)) -> (((exists ff_h_pfp_left_constant_sum_A. ff_h_pfp_left_constant_sum_A + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_left_constant_sum_A. ab = ff_q_pfp_left_constant_sum_A * S ((S (i)) * ac) + (a))) -> (forall pfc_index_left_constant_sum_diagonal. (exists pfa_gap_left_constant_sum_diagonalbound. pfa_gap_left_constant_sum_diagonalbound + S (pfc_index_left_constant_sum_diagonal) = (S i)) -> exists pfc_value_left_constant_sum_diagonal. ((((exists ff_h_pfp_left_constant_sum_diagonalentry. ff_h_pfp_left_constant_sum_diagonalentry + S (pfc_value_left_constant_sum_diagonal) = S ((S (pfc_index_left_constant_sum_diagonal)) * dc)) /\ exists ff_q_pfp_left_constant_sum_diagonalentry. db = ff_q_pfp_left_constant_sum_diagonalentry * S ((S (pfc_index_left_constant_sum_diagonal)) * dc) + (pfc_value_left_constant_sum_diagonal))) /\ ((exists pfc_complement_left_constant_sum_diagonalterm pfc_left_left_constant_sum_diagonalterm pfc_right_left_constant_sum_diagonalterm. (((pfc_index_left_constant_sum_diagonal)+pfc_complement_left_constant_sum_diagonalterm=(i)) /\ ((((((exists pfa_gap_left_constant_sum_diagonaltermleftinside. pfa_gap_left_constant_sum_diagonaltermleftinside + S (pfc_index_left_constant_sum_diagonal) = (1)) /\ ((((exists ff_h_pfp_left_constant_sum_diagonaltermleftentry. ff_h_pfp_left_constant_sum_diagonaltermleftentry + S (pfc_left_left_constant_sum_diagonalterm) = S ((S (pfc_index_left_constant_sum_diagonal)) * kc)) /\ exists ff_q_pfp_left_constant_sum_diagonaltermleftentry. kb = ff_q_pfp_left_constant_sum_diagonaltermleftentry * S ((S (pfc_index_left_constant_sum_diagonal)) * kc) + (pfc_left_left_constant_sum_diagonalterm)))))) \/ (((exists pfc_gap_left_constant_sum_diagonaltermleftoutside. pfc_gap_left_constant_sum_diagonaltermleftoutside+(1)=(pfc_index_left_constant_sum_diagonal)) /\ (((pfc_left_left_constant_sum_diagonalterm)=0))))) /\ ((((((exists pfa_gap_left_constant_sum_diagonaltermrightinside. pfa_gap_left_constant_sum_diagonaltermrightinside + S (pfc_complement_left_constant_sum_diagonalterm) = (L)) /\ ((((exists ff_h_pfp_left_constant_sum_diagonaltermrightentry. ff_h_pfp_left_constant_sum_diagonaltermrightentry + S (pfc_right_left_constant_sum_diagonalterm) = S ((S (pfc_complement_left_constant_sum_diagonalterm)) * ac)) /\ exists ff_q_pfp_left_constant_sum_diagonaltermrightentry. ab = ff_q_pfp_left_constant_sum_diagonaltermrightentry * S ((S (pfc_complement_left_constant_sum_diagonalterm)) * ac) + (pfc_right_left_constant_sum_diagonalterm)))))) \/ (((exists pfc_gap_left_constant_sum_diagonaltermrightoutside. pfc_gap_left_constant_sum_diagonaltermrightoutside+(L)=(pfc_complement_left_constant_sum_diagonalterm)) /\ (((pfc_right_left_constant_sum_diagonalterm)=0))))) /\ (((pfc_value_left_constant_sum_diagonal)=pfc_left_left_constant_sum_diagonalterm*pfc_right_left_constant_sum_diagonalterm))))))))))) -> (exists fs_u_pfc_left_constant_sum_actual fs_v_pfc_left_constant_sum_actual. ((((exists fs_h_pfc_left_constant_sum_actual_body_start. fs_h_pfc_left_constant_sum_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_constant_sum_actual)) /\ exists fs_q_pfc_left_constant_sum_actual_body_start. fs_u_pfc_left_constant_sum_actual = fs_q_pfc_left_constant_sum_actual_body_start * S ((S (0)) * fs_v_pfc_left_constant_sum_actual) + (0))) /\ ((((exists fs_h_pfc_left_constant_sum_actual_body_terminal. fs_h_pfc_left_constant_sum_actual_body_terminal + S (n) = S ((S (S i)) * fs_v_pfc_left_constant_sum_actual)) /\ exists fs_q_pfc_left_constant_sum_actual_body_terminal. fs_u_pfc_left_constant_sum_actual = fs_q_pfc_left_constant_sum_actual_body_terminal * S ((S (S i)) * fs_v_pfc_left_constant_sum_actual) + (n))) /\ forall fs_i_pfc_left_constant_sum_actual_body_steps. (exists fs_lt_pfc_left_constant_sum_actual_body_steps_bound. fs_lt_pfc_left_constant_sum_actual_body_steps_bound + S fs_i_pfc_left_constant_sum_actual_body_steps = S i) -> exists fs_a_pfc_left_constant_sum_actual_body_steps fs_r_pfc_left_constant_sum_actual_body_steps fs_s_pfc_left_constant_sum_actual_body_steps. ((((exists fs_h_pfc_left_constant_sum_actual_body_steps_summand. fs_h_pfc_left_constant_sum_actual_body_steps_summand + S (fs_a_pfc_left_constant_sum_actual_body_steps) = S ((S (fs_i_pfc_left_constant_sum_actual_body_steps)) * dc)) /\ exists fs_q_pfc_left_constant_sum_actual_body_steps_summand. db = fs_q_pfc_left_constant_sum_actual_body_steps_summand * S ((S (fs_i_pfc_left_constant_sum_actual_body_steps)) * dc) + (fs_a_pfc_left_constant_sum_actual_body_steps))) /\ ((((exists fs_h_pfc_left_constant_sum_actual_body_steps_partial. fs_h_pfc_left_constant_sum_actual_body_steps_partial + S (fs_r_pfc_left_constant_sum_actual_body_steps) = S ((S (fs_i_pfc_left_constant_sum_actual_body_steps)) * fs_v_pfc_left_constant_sum_actual)) /\ exists fs_q_pfc_left_constant_sum_actual_body_steps_partial. fs_u_pfc_left_constant_sum_actual = fs_q_pfc_left_constant_sum_actual_body_steps_partial * S ((S (fs_i_pfc_left_constant_sum_actual_body_steps)) * fs_v_pfc_left_constant_sum_actual) + (fs_r_pfc_left_constant_sum_actual_body_steps))) /\ ((((exists fs_h_pfc_left_constant_sum_actual_body_steps_successor. fs_h_pfc_left_constant_sum_actual_body_steps_successor + S (fs_s_pfc_left_constant_sum_actual_body_steps) = S ((S (S fs_i_pfc_left_constant_sum_actual_body_steps)) * fs_v_pfc_left_constant_sum_actual)) /\ exists fs_q_pfc_left_constant_sum_actual_body_steps_successor. fs_u_pfc_left_constant_sum_actual = fs_q_pfc_left_constant_sum_actual_body_steps_successor * S ((S (S fs_i_pfc_left_constant_sum_actual_body_steps)) * fs_v_pfc_left_constant_sum_actual) + (fs_s_pfc_left_constant_sum_actual_body_steps))) /\ fs_s_pfc_left_constant_sum_actual_body_steps = fs_r_pfc_left_constant_sum_actual_body_steps + fs_a_pfc_left_constant_sum_actual_body_steps)))))) -> (n=k*a)

Complete tactic proof in conservative notation

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

137 script commands · 30 reading checkpoints · 13 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)
polynomial diagonal left constant first termpolynomial diagonal left unit tail term
01Fix variables and assumptionsL1–10

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

  1. L1
    intro k
  2. L2
    intro kb
  3. L3
    intro kc
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro L
  7. L7
    intro i
  8. L8
    intro a
  9. L9
    intro db
  10. L10
    intro dc
02Fix variables and assumptionsL11–16

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

  1. L11
    intro n
  2. L12
    intro hk
  3. L13
    intro hi
  4. L14
    intro ha
  5. L15
    intro hd
  6. L16
    intro hs
03Establish hheadL17–17

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

  1. L17
    have hhead : BetaAt(db,dc,0,k · a)Definitions: BetaAt(db,dc,0,k · a)Original native command in the exact edition
04Establish hvL18–20

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

  1. L18
    have hv : ∃ t. BetaAt(db,dc,0,t) ∧ PolynomialDiagonalTerm(kb,kc,1,ab,ac,L,i,0,t)Definitions: BetaAt(db,dc,0,t)PolynomialDiagonalTerm(kb,kc,1,ab,ac,L,i,0,t)Original native command in the exact edition
  2. L19
    specialize hd (0)
  3. L20
    apply hd
05Construct an explicit witnessL21–21

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

  1. L21
    exists i
06Calculate and transport equalitiesL22–22

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

  1. L22
    simp
07Separate the logical casesL23–24

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

  1. L23
    cases hv
  2. L24
    cases hv_witness
08Establish heqL25–34

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

  1. L25
    have heq : x=k*a
  2. L26
    specialize polynomial_diagonal_left_constant_first_term (k)
  3. L27
    specialize polynomial_diagonal_left_constant_first_term (kb)
  4. L28
    specialize polynomial_diagonal_left_constant_first_term (kc)
  5. L29
    specialize polynomial_diagonal_left_constant_first_term (ab)
  6. L30
    specialize polynomial_diagonal_left_constant_first_term (ac)
  7. L31
    specialize polynomial_diagonal_left_constant_first_term (L)
  8. L32
    specialize polynomial_diagonal_left_constant_first_term (i)
  9. L33
    specialize polynomial_diagonal_left_constant_first_term (a)
  10. L34
    specialize polynomial_diagonal_left_constant_first_term (x)
09Use earlier factsL35–39

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

  1. L35
    apply polynomial_diagonal_left_constant_first_term
  2. L36
    exact hk
  3. L37
    exact hi
  4. L38
    exact ha
  5. L39
    exact hv_witness_right
10Calculate and transport equalitiesL40–41

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

  1. L40
    rewrite heq at hv_witness_left
  2. L41
    rewrite heq at hv_witness_left
11Use earlier factsL42–42

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

  1. L42
    exact hv_witness_left
12Establish htailL43–45

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

  1. L43
    have htail : ∀ pfpad_tail_index_left_constant_sum_tail. Lt(pfpad_tail_index_left_constant_sum_tail,i) → BetaAt(db,dc,1 + pfpad_tail_index_left_constant_sum_tail,0)Definitions: Lt(pfpad_tail_index_left_constant_sum_tail,i)BetaAt(db,dc,1 + pfpad_tail_index_left_constant_sum_tail,0)Original native command in the exact edition
  2. L44
    intro j
  3. L45
    intro hj
13Establish hvL46–48

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

  1. L46
    have hv : ∃ t. BetaAt(db,dc,1 + j,t) ∧ PolynomialDiagonalTerm(kb,kc,1,ab,ac,L,i,1 + j,t)Definitions: BetaAt(db,dc,1 + j,t)PolynomialDiagonalTerm(kb,kc,1,ab,ac,L,i,1 + j,t)Original native command in the exact edition
  2. L47
    specialize hd (1+j)
  3. L48
    apply hd
14Establish hindexL49–55

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

  1. L49
    have hindex : 1+j=S j
  2. L50
    simp [add_succ_left,zero_add]
  3. L51
    rewrite hindex
  4. L52
    specialize succ_le_succ (S j)
  5. L53
    specialize succ_le_succ (i)
  6. L54
    apply succ_le_succ
  7. L55
    exact hj
15Separate the logical casesL56–57

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

  1. L56
    cases hv
  2. L57
    cases hv_witness
16Establish heqL58–67

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial diagonal left unit tail term.

  1. L58
    have heq : x=0
  2. L59
    specialize polynomial_diagonal_left_unit_tail_term (kb)
  3. L60
    specialize polynomial_diagonal_left_unit_tail_term (kc)
  4. L61
    specialize polynomial_diagonal_left_unit_tail_term (ab)
  5. L62
    specialize polynomial_diagonal_left_unit_tail_term (ac)
  6. L63
    specialize polynomial_diagonal_left_unit_tail_term (L)
  7. L64
    specialize polynomial_diagonal_left_unit_tail_term (i)
  8. L65
    specialize polynomial_diagonal_left_unit_tail_term (1+j)
  9. L66
    specialize polynomial_diagonal_left_unit_tail_term (x)
  10. L67
    apply polynomial_diagonal_left_unit_tail_term
17Use earlier factsL68–71

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

  1. L68
    specialize le_add_right (1)
  2. L69
    specialize le_add_right (j)
  3. L70
    apply le_add_right
  4. L71
    exact hv_witness_right
18Calculate and transport equalitiesL72–73

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

  1. L72
    rewrite heq at hv_witness_left
  2. L73
    rewrite heq at hv_witness_left
19Use earlier factsL74–74

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

  1. L74
    exact hv_witness_left
20Establish hsingleL75–79

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

  1. L75
    have hsingle : ∃ m. Sum(db,dc,1,m)Definitions: Sum(db,dc,1,m)Original native command in the exact edition
  2. L76
    specialize beta_sum_exists (db)
  3. L77
    specialize beta_sum_exists (dc)
  4. L78
    specialize beta_sum_exists (1)
  5. L79
    apply beta_sum_exists
21Separate the logical casesL80–80

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

  1. L80
    cases hsingle
22Establish hdecompL81–87

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

  1. L81
    have hdecomp : ∃ t. ∃ s. BetaAt(db,dc,0,t) ∧ (Sum(db,dc,0,s) ∧ x = s + t)Definitions: BetaAt(db,dc,0,t)Sum(db,dc,0,s)Original native command in the exact edition
  2. L82
    specialize beta_sum_succ_decompose (db)
  3. L83
    specialize beta_sum_succ_decompose (dc)
  4. L84
    specialize beta_sum_succ_decompose (0)
  5. L85
    specialize beta_sum_succ_decompose (x)
  6. L86
    apply beta_sum_succ_decompose
  7. L87
    exact hsingle_witness
23Separate the logical casesL88–91

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

  1. L88
    cases hdecomp
  2. L89
    cases hdecomp_witness
  3. L90
    cases hdecomp_witness_witness
  4. L91
    cases hdecomp_witness_witness_right
24Establish hzeroL92–97

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

  1. L92
    have hzero : x2=0
  2. L93
    specialize beta_sum_zero (db)
  3. L94
    specialize beta_sum_zero (dc)
  4. L95
    specialize beta_sum_zero (x2)
  5. L96
    apply beta_sum_zero
  6. L97
    exact hdecomp_witness_witness_right_left
25Establish hentryL98–106

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

  1. L98
    have hentry : x1=k*a
  2. L99
    specialize beta_at_unique (db)
  3. L100
    specialize beta_at_unique (dc)
  4. L101
    specialize beta_at_unique (0)
  5. L102
    specialize beta_at_unique (x1)
  6. L103
    specialize beta_at_unique (k*a)
  7. L104
    apply beta_at_unique
  8. L105
    exact hdecomp_witness_witness_left
  9. L106
    exact hhead
26Establish hvalueL107–116

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

  1. L107
    have hvalue : x=k*a
  2. L108
    trans x2+x1
  3. L109
    exact hdecomp_witness_witness_right_right
  4. L110
    rewrite hzero
  5. L111
    trans x1
  6. L112
    apply zero_add
  7. L113
    exact hentry
  8. L114
    trans x
  9. L115
    specialize polynomial_zero_tail_natural_sum_invariant (db)
  10. L116
    specialize polynomial_zero_tail_natural_sum_invariant (dc)
27Use earlier factsL117–123

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

  1. L117
    specialize polynomial_zero_tail_natural_sum_invariant (db)
  2. L118
    specialize polynomial_zero_tail_natural_sum_invariant (dc)
  3. L119
    specialize polynomial_zero_tail_natural_sum_invariant (1)
  4. L120
    specialize polynomial_zero_tail_natural_sum_invariant (i)
  5. L121
    specialize polynomial_zero_tail_natural_sum_invariant (x)
  6. L122
    specialize polynomial_zero_tail_natural_sum_invariant (n)
  7. L123
    apply polynomial_zero_tail_natural_sum_invariant
28Fix variables and assumptionsL124–127

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

  1. L124
    intro j0
  2. L125
    intro v0
  3. L126
    intro hj0
  4. L127
    intro hv0
29Use earlier factsL128–130

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

  1. L128
    exact hv0
  2. L129
    exact htail
  3. L130
    exact hsingle_witness
30Establish hlengthL131–137

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

  1. L131
    have hlength : 1+i=S i
  2. L132
    simp [add_succ_left,zero_add]
  3. L133
    rewrite hlength
  4. L134
    rewrite hlength
  5. L135
    rewrite hlength
  6. L136
    exact hs
  7. L137
    exact hvalue

Library-wide reading audit

Original defined command ledger · 137 lines
  1. 0001intro k
  2. 0002intro kb
  3. 0003intro kc
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro L
  7. 0007intro i
  8. 0008intro a
  9. 0009intro db
  10. 0010intro dc
  11. 0011intro n
  12. 0012intro hk
  13. 0013intro hi
  14. 0014intro ha
  15. 0015intro hd
  16. 0016intro hs
  17. 0017have hhead : BetaAt(db,dc,0,k · a)
  18. 0018have hv : ∃ t. BetaAt(db,dc,0,t) ∧ PolynomialDiagonalTerm(kb,kc,1,ab,ac,L,i,0,t)
  19. 0019specialize hd (0)
  20. 0020apply hd
  21. 0021exists i
  22. 0022simp
  23. 0023cases hv
  24. 0024cases hv_witness
  25. 0025have heq : x=k*a
  26. 0026specialize polynomial_diagonal_left_constant_first_term (k)
  27. 0027specialize polynomial_diagonal_left_constant_first_term (kb)
  28. 0028specialize polynomial_diagonal_left_constant_first_term (kc)
  29. 0029specialize polynomial_diagonal_left_constant_first_term (ab)
  30. 0030specialize polynomial_diagonal_left_constant_first_term (ac)
  31. 0031specialize polynomial_diagonal_left_constant_first_term (L)
  32. 0032specialize polynomial_diagonal_left_constant_first_term (i)
  33. 0033specialize polynomial_diagonal_left_constant_first_term (a)
  34. 0034specialize polynomial_diagonal_left_constant_first_term (x)
  35. 0035apply polynomial_diagonal_left_constant_first_term
  36. 0036exact hk
  37. 0037exact hi
  38. 0038exact ha
  39. 0039exact hv_witness_right
  40. 0040rewrite heq at hv_witness_left
  41. 0041rewrite heq at hv_witness_left
  42. 0042exact hv_witness_left
  43. 0043have htail : ∀ pfpad_tail_index_left_constant_sum_tail. Lt(pfpad_tail_index_left_constant_sum_tail,i) → BetaAt(db,dc,1 + pfpad_tail_index_left_constant_sum_tail,0)
  44. 0044intro j
  45. 0045intro hj
  46. 0046have hv : ∃ t. BetaAt(db,dc,1 + j,t) ∧ PolynomialDiagonalTerm(kb,kc,1,ab,ac,L,i,1 + j,t)
  47. 0047specialize hd (1+j)
  48. 0048apply hd
  49. 0049have hindex : 1+j=S j
  50. 0050simp [add_succ_left,zero_add]
  51. 0051rewrite hindex
  52. 0052specialize succ_le_succ (S j)
  53. 0053specialize succ_le_succ (i)
  54. 0054apply succ_le_succ
  55. 0055exact hj
  56. 0056cases hv
  57. 0057cases hv_witness
  58. 0058have heq : x=0
  59. 0059specialize polynomial_diagonal_left_unit_tail_term (kb)
  60. 0060specialize polynomial_diagonal_left_unit_tail_term (kc)
  61. 0061specialize polynomial_diagonal_left_unit_tail_term (ab)
  62. 0062specialize polynomial_diagonal_left_unit_tail_term (ac)
  63. 0063specialize polynomial_diagonal_left_unit_tail_term (L)
  64. 0064specialize polynomial_diagonal_left_unit_tail_term (i)
  65. 0065specialize polynomial_diagonal_left_unit_tail_term (1+j)
  66. 0066specialize polynomial_diagonal_left_unit_tail_term (x)
  67. 0067apply polynomial_diagonal_left_unit_tail_term
  68. 0068specialize le_add_right (1)
  69. 0069specialize le_add_right (j)
  70. 0070apply le_add_right
  71. 0071exact hv_witness_right
  72. 0072rewrite heq at hv_witness_left
  73. 0073rewrite heq at hv_witness_left
  74. 0074exact hv_witness_left
  75. 0075have hsingle : ∃ m. Sum(db,dc,1,m)
  76. 0076specialize beta_sum_exists (db)
  77. 0077specialize beta_sum_exists (dc)
  78. 0078specialize beta_sum_exists (1)
  79. 0079apply beta_sum_exists
  80. 0080cases hsingle
  81. 0081have hdecomp : ∃ t. ∃ s. BetaAt(db,dc,0,t) ∧ (Sum(db,dc,0,s) ∧ x = s + t)
  82. 0082specialize beta_sum_succ_decompose (db)
  83. 0083specialize beta_sum_succ_decompose (dc)
  84. 0084specialize beta_sum_succ_decompose (0)
  85. 0085specialize beta_sum_succ_decompose (x)
  86. 0086apply beta_sum_succ_decompose
  87. 0087exact hsingle_witness
  88. 0088cases hdecomp
  89. 0089cases hdecomp_witness
  90. 0090cases hdecomp_witness_witness
  91. 0091cases hdecomp_witness_witness_right
  92. 0092have hzero : x2=0
  93. 0093specialize beta_sum_zero (db)
  94. 0094specialize beta_sum_zero (dc)
  95. 0095specialize beta_sum_zero (x2)
  96. 0096apply beta_sum_zero
  97. 0097exact hdecomp_witness_witness_right_left
  98. 0098have hentry : x1=k*a
  99. 0099specialize beta_at_unique (db)
  100. 0100specialize beta_at_unique (dc)
  101. 0101specialize beta_at_unique (0)
  102. 0102specialize beta_at_unique (x1)
  103. 0103specialize beta_at_unique (k*a)
  104. 0104apply beta_at_unique
  105. 0105exact hdecomp_witness_witness_left
  106. 0106exact hhead
  107. 0107have hvalue : x=k*a
  108. 0108trans x2+x1
  109. 0109exact hdecomp_witness_witness_right_right
  110. 0110rewrite hzero
  111. 0111trans x1
  112. 0112apply zero_add
  113. 0113exact hentry
  114. 0114trans x
  115. 0115specialize polynomial_zero_tail_natural_sum_invariant (db)
  116. 0116specialize polynomial_zero_tail_natural_sum_invariant (dc)
  117. 0117specialize polynomial_zero_tail_natural_sum_invariant (db)
  118. 0118specialize polynomial_zero_tail_natural_sum_invariant (dc)
  119. 0119specialize polynomial_zero_tail_natural_sum_invariant (1)
  120. 0120specialize polynomial_zero_tail_natural_sum_invariant (i)
  121. 0121specialize polynomial_zero_tail_natural_sum_invariant (x)
  122. 0122specialize polynomial_zero_tail_natural_sum_invariant (n)
  123. 0123apply polynomial_zero_tail_natural_sum_invariant
  124. 0124intro j0
  125. 0125intro v0
  126. 0126intro hj0
  127. 0127intro hv0
  128. 0128exact hv0
  129. 0129exact htail
  130. 0130exact hsingle_witness
  131. 0131have hlength : 1+i=S i
  132. 0132simp [add_succ_left,zero_add]
  133. 0133rewrite hlength
  134. 0134rewrite hlength
  135. 0135rewrite hlength
  136. 0136exact hs
  137. 0137exact hvalue