PG002F

polynomial_diagonal_left_unit_natural_sum

An actual unit-left antidiagonal sum equals its first coefficient: construct the one-term sum and use the proved zero-tail invariant on all remaining actual summands.

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

∀ ub. ∀ uc. ∀ ab. ∀ ac. ∀ L. ∀ i. ∀ a. ∀ db. ∀ dc. ∀ n. BetaAt(ub,uc,0,1) → Lt(i,L) → BetaAt(ab,ac,i,a) → PolynomialDiagonalPrefix(ub,uc,1,ab,ac,L,i,db,dc,S i) → Sum(db,dc,S i,n) → n = 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_unit_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 ub uc ab ac L i a db dc n. (((exists ff_h_pfp_unit_sum_unit. ff_h_pfp_unit_sum_unit + S (1) = S ((S (0)) * uc)) /\ exists ff_q_pfp_unit_sum_unit. ub = ff_q_pfp_unit_sum_unit * S ((S (0)) * uc) + (1))) -> (exists pfa_gap_unit_sum_index. pfa_gap_unit_sum_index + S (i) = (L)) -> (((exists ff_h_pfp_unit_sum_A. ff_h_pfp_unit_sum_A + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_unit_sum_A. ab = ff_q_pfp_unit_sum_A * S ((S (i)) * ac) + (a))) -> (forall pfc_index_unit_sum_diagonal. (exists pfa_gap_unit_sum_diagonalbound. pfa_gap_unit_sum_diagonalbound + S (pfc_index_unit_sum_diagonal) = (S i)) -> exists pfc_value_unit_sum_diagonal. ((((exists ff_h_pfp_unit_sum_diagonalentry. ff_h_pfp_unit_sum_diagonalentry + S (pfc_value_unit_sum_diagonal) = S ((S (pfc_index_unit_sum_diagonal)) * dc)) /\ exists ff_q_pfp_unit_sum_diagonalentry. db = ff_q_pfp_unit_sum_diagonalentry * S ((S (pfc_index_unit_sum_diagonal)) * dc) + (pfc_value_unit_sum_diagonal))) /\ ((exists pfc_complement_unit_sum_diagonalterm pfc_left_unit_sum_diagonalterm pfc_right_unit_sum_diagonalterm. (((pfc_index_unit_sum_diagonal)+pfc_complement_unit_sum_diagonalterm=(i)) /\ ((((((exists pfa_gap_unit_sum_diagonaltermleftinside. pfa_gap_unit_sum_diagonaltermleftinside + S (pfc_index_unit_sum_diagonal) = (1)) /\ ((((exists ff_h_pfp_unit_sum_diagonaltermleftentry. ff_h_pfp_unit_sum_diagonaltermleftentry + S (pfc_left_unit_sum_diagonalterm) = S ((S (pfc_index_unit_sum_diagonal)) * uc)) /\ exists ff_q_pfp_unit_sum_diagonaltermleftentry. ub = ff_q_pfp_unit_sum_diagonaltermleftentry * S ((S (pfc_index_unit_sum_diagonal)) * uc) + (pfc_left_unit_sum_diagonalterm)))))) \/ (((exists pfc_gap_unit_sum_diagonaltermleftoutside. pfc_gap_unit_sum_diagonaltermleftoutside+(1)=(pfc_index_unit_sum_diagonal)) /\ (((pfc_left_unit_sum_diagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_sum_diagonaltermrightinside. pfa_gap_unit_sum_diagonaltermrightinside + S (pfc_complement_unit_sum_diagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_sum_diagonaltermrightentry. ff_h_pfp_unit_sum_diagonaltermrightentry + S (pfc_right_unit_sum_diagonalterm) = S ((S (pfc_complement_unit_sum_diagonalterm)) * ac)) /\ exists ff_q_pfp_unit_sum_diagonaltermrightentry. ab = ff_q_pfp_unit_sum_diagonaltermrightentry * S ((S (pfc_complement_unit_sum_diagonalterm)) * ac) + (pfc_right_unit_sum_diagonalterm)))))) \/ (((exists pfc_gap_unit_sum_diagonaltermrightoutside. pfc_gap_unit_sum_diagonaltermrightoutside+(L)=(pfc_complement_unit_sum_diagonalterm)) /\ (((pfc_right_unit_sum_diagonalterm)=0))))) /\ (((pfc_value_unit_sum_diagonal)=pfc_left_unit_sum_diagonalterm*pfc_right_unit_sum_diagonalterm))))))))))) -> (exists fs_u_pfc_unit_sum_actual fs_v_pfc_unit_sum_actual. ((((exists fs_h_pfc_unit_sum_actual_body_start. fs_h_pfc_unit_sum_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_sum_actual)) /\ exists fs_q_pfc_unit_sum_actual_body_start. fs_u_pfc_unit_sum_actual = fs_q_pfc_unit_sum_actual_body_start * S ((S (0)) * fs_v_pfc_unit_sum_actual) + (0))) /\ ((((exists fs_h_pfc_unit_sum_actual_body_terminal. fs_h_pfc_unit_sum_actual_body_terminal + S (n) = S ((S (S i)) * fs_v_pfc_unit_sum_actual)) /\ exists fs_q_pfc_unit_sum_actual_body_terminal. fs_u_pfc_unit_sum_actual = fs_q_pfc_unit_sum_actual_body_terminal * S ((S (S i)) * fs_v_pfc_unit_sum_actual) + (n))) /\ forall fs_i_pfc_unit_sum_actual_body_steps. (exists fs_lt_pfc_unit_sum_actual_body_steps_bound. fs_lt_pfc_unit_sum_actual_body_steps_bound + S fs_i_pfc_unit_sum_actual_body_steps = S i) -> exists fs_a_pfc_unit_sum_actual_body_steps fs_r_pfc_unit_sum_actual_body_steps fs_s_pfc_unit_sum_actual_body_steps. ((((exists fs_h_pfc_unit_sum_actual_body_steps_summand. fs_h_pfc_unit_sum_actual_body_steps_summand + S (fs_a_pfc_unit_sum_actual_body_steps) = S ((S (fs_i_pfc_unit_sum_actual_body_steps)) * dc)) /\ exists fs_q_pfc_unit_sum_actual_body_steps_summand. db = fs_q_pfc_unit_sum_actual_body_steps_summand * S ((S (fs_i_pfc_unit_sum_actual_body_steps)) * dc) + (fs_a_pfc_unit_sum_actual_body_steps))) /\ ((((exists fs_h_pfc_unit_sum_actual_body_steps_partial. fs_h_pfc_unit_sum_actual_body_steps_partial + S (fs_r_pfc_unit_sum_actual_body_steps) = S ((S (fs_i_pfc_unit_sum_actual_body_steps)) * fs_v_pfc_unit_sum_actual)) /\ exists fs_q_pfc_unit_sum_actual_body_steps_partial. fs_u_pfc_unit_sum_actual = fs_q_pfc_unit_sum_actual_body_steps_partial * S ((S (fs_i_pfc_unit_sum_actual_body_steps)) * fs_v_pfc_unit_sum_actual) + (fs_r_pfc_unit_sum_actual_body_steps))) /\ ((((exists fs_h_pfc_unit_sum_actual_body_steps_successor. fs_h_pfc_unit_sum_actual_body_steps_successor + S (fs_s_pfc_unit_sum_actual_body_steps) = S ((S (S fs_i_pfc_unit_sum_actual_body_steps)) * fs_v_pfc_unit_sum_actual)) /\ exists fs_q_pfc_unit_sum_actual_body_steps_successor. fs_u_pfc_unit_sum_actual = fs_q_pfc_unit_sum_actual_body_steps_successor * S ((S (S fs_i_pfc_unit_sum_actual_body_steps)) * fs_v_pfc_unit_sum_actual) + (fs_s_pfc_unit_sum_actual_body_steps))) /\ fs_s_pfc_unit_sum_actual_body_steps = fs_r_pfc_unit_sum_actual_body_steps + fs_a_pfc_unit_sum_actual_body_steps)))))) -> (n=a)

Complete tactic proof in conservative notation

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

135 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 unit 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 ub
  2. L2
    intro uc
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro L
  6. L6
    intro i
  7. L7
    intro a
  8. L8
    intro db
  9. L9
    intro dc
  10. L10
    intro n
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hu
  2. L12
    intro hi
  3. L13
    intro ha
  4. L14
    intro hd
  5. L15
    intro hs
03Establish hheadL16–16

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

  1. L16
    have hhead : BetaAt(db,dc,0,a)Definitions: BetaAt(db,dc,0,a)Original native command in the exact edition
04Establish hvL17–19

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

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

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

  1. L20
    exists i
06Calculate and transport equalitiesL21–21

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

  1. L21
    simp
07Separate the logical casesL22–23

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

  1. L22
    cases hv
  2. L23
    cases hv_witness
08Establish heqL24–33

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

  1. L24
    have heq : x=a
  2. L25
    specialize polynomial_diagonal_left_unit_first_term (ub)
  3. L26
    specialize polynomial_diagonal_left_unit_first_term (uc)
  4. L27
    specialize polynomial_diagonal_left_unit_first_term (ab)
  5. L28
    specialize polynomial_diagonal_left_unit_first_term (ac)
  6. L29
    specialize polynomial_diagonal_left_unit_first_term (L)
  7. L30
    specialize polynomial_diagonal_left_unit_first_term (i)
  8. L31
    specialize polynomial_diagonal_left_unit_first_term (a)
  9. L32
    specialize polynomial_diagonal_left_unit_first_term (x)
  10. L33
    apply polynomial_diagonal_left_unit_first_term
09Use earlier factsL34–37

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

  1. L34
    exact hu
  2. L35
    exact hi
  3. L36
    exact ha
  4. L37
    exact hv_witness_right
10Calculate and transport equalitiesL38–39

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

  1. L38
    rewrite heq at hv_witness_left
  2. L39
    rewrite heq at hv_witness_left
11Use earlier factsL40–40

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

  1. L40
    exact hv_witness_left
12Establish htailL41–43

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

  1. L41
    have htail : ∀ pfpad_tail_index_unit_sum_tail. Lt(pfpad_tail_index_unit_sum_tail,i) → BetaAt(db,dc,1 + pfpad_tail_index_unit_sum_tail,0)Definitions: Lt(pfpad_tail_index_unit_sum_tail,i)BetaAt(db,dc,1 + pfpad_tail_index_unit_sum_tail,0)Original native command in the exact edition
  2. L42
    intro j
  3. L43
    intro hj
13Establish hvL44–46

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

  1. L44
    have hv : ∃ t. BetaAt(db,dc,1 + j,t) ∧ PolynomialDiagonalTerm(ub,uc,1,ab,ac,L,i,1 + j,t)Definitions: BetaAt(db,dc,1 + j,t)PolynomialDiagonalTerm(ub,uc,1,ab,ac,L,i,1 + j,t)Original native command in the exact edition
  2. L45
    specialize hd (1+j)
  3. L46
    apply hd
14Establish hindexL47–53

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

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

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

  1. L54
    cases hv
  2. L55
    cases hv_witness
16Establish heqL56–65

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. L56
    have heq : x=0
  2. L57
    specialize polynomial_diagonal_left_unit_tail_term (ub)
  3. L58
    specialize polynomial_diagonal_left_unit_tail_term (uc)
  4. L59
    specialize polynomial_diagonal_left_unit_tail_term (ab)
  5. L60
    specialize polynomial_diagonal_left_unit_tail_term (ac)
  6. L61
    specialize polynomial_diagonal_left_unit_tail_term (L)
  7. L62
    specialize polynomial_diagonal_left_unit_tail_term (i)
  8. L63
    specialize polynomial_diagonal_left_unit_tail_term (1+j)
  9. L64
    specialize polynomial_diagonal_left_unit_tail_term (x)
  10. L65
    apply polynomial_diagonal_left_unit_tail_term
17Use earlier factsL66–69

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

  1. L66
    specialize le_add_right (1)
  2. L67
    specialize le_add_right (j)
  3. L68
    apply le_add_right
  4. L69
    exact hv_witness_right
18Calculate and transport equalitiesL70–71

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

  1. L70
    rewrite heq at hv_witness_left
  2. L71
    rewrite heq at hv_witness_left
19Use earlier factsL72–72

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

  1. L72
    exact hv_witness_left
20Establish hsingleL73–77

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

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

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

  1. L78
    cases hsingle
22Establish hdecompL79–85

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

  1. L79
    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. L80
    specialize beta_sum_succ_decompose (db)
  3. L81
    specialize beta_sum_succ_decompose (dc)
  4. L82
    specialize beta_sum_succ_decompose (0)
  5. L83
    specialize beta_sum_succ_decompose (x)
  6. L84
    apply beta_sum_succ_decompose
  7. L85
    exact hsingle_witness
23Separate the logical casesL86–89

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

  1. L86
    cases hdecomp
  2. L87
    cases hdecomp_witness
  3. L88
    cases hdecomp_witness_witness
  4. L89
    cases hdecomp_witness_witness_right
24Establish hzeroL90–95

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

  1. L90
    have hzero : x2=0
  2. L91
    specialize beta_sum_zero (db)
  3. L92
    specialize beta_sum_zero (dc)
  4. L93
    specialize beta_sum_zero (x2)
  5. L94
    apply beta_sum_zero
  6. L95
    exact hdecomp_witness_witness_right_left
25Establish hentryL96–104

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

  1. L96
    have hentry : x1=a
  2. L97
    specialize beta_at_unique (db)
  3. L98
    specialize beta_at_unique (dc)
  4. L99
    specialize beta_at_unique (0)
  5. L100
    specialize beta_at_unique (x1)
  6. L101
    specialize beta_at_unique (a)
  7. L102
    apply beta_at_unique
  8. L103
    exact hdecomp_witness_witness_left
  9. L104
    exact hhead
26Establish hvalueL105–114

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

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

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

  1. L115
    specialize polynomial_zero_tail_natural_sum_invariant (db)
  2. L116
    specialize polynomial_zero_tail_natural_sum_invariant (dc)
  3. L117
    specialize polynomial_zero_tail_natural_sum_invariant (1)
  4. L118
    specialize polynomial_zero_tail_natural_sum_invariant (i)
  5. L119
    specialize polynomial_zero_tail_natural_sum_invariant (x)
  6. L120
    specialize polynomial_zero_tail_natural_sum_invariant (n)
  7. L121
    apply polynomial_zero_tail_natural_sum_invariant
28Fix variables and assumptionsL122–125

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

  1. L122
    intro k
  2. L123
    intro v
  3. L124
    intro hk
  4. L125
    intro hv
29Use earlier factsL126–128

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

  1. L126
    exact hv
  2. L127
    exact htail
  3. L128
    exact hsingle_witness
30Establish hlengthL129–135

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

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

Library-wide reading audit

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