PX0064

polynomial_diagonal_left_padding_left

The two actual antidiagonal tables differ by a proved leading zero block and exact copied natural summands.

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

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ AB. ∀ AC. ∀ t. ∀ i. ∀ db. ∀ dc. ∀ eb. ∀ ec. PolynomialLeftPad(ab,ac,L,t,AB,AC) → PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,S i) → PolynomialDiagonalPrefix(AB,AC,t + L,bb,bc,M,t + i,eb,ec,S (t + i)) → PolynomialLeftPad(db,dc,S i,t,eb,ec)

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

Definition DAG

PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) · 3PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l) · 2PolynomialLeftPad(b,c,L,t,d,e) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

polynomial_diagonal_prefix_entry · checked external prerequisitele_trans · checked external prerequisitesucc_le_succ · checked external prerequisitepolynomial_diagonal_term_functional · checked external prerequisitepolynomial_diagonal_term_left_padding_leftpolynomial_diagonal_term_left_padding_zero_leftle_succ · checked external prerequisitele_add_right · checked external prerequisiteadd_le_add_left · checked external prerequisitele_of_succ_le_succ · checked external prerequisite
Original expanded first-order statement 
forall ab ac L bb bc M AB AC t i db dc eb ec. (((forall pfp_repeat_index_diagonal_actual_padding_leftzeros. (exists pfa_gap_diagonal_actual_padding_leftzerosindex. pfa_gap_diagonal_actual_padding_leftzerosindex + S (pfp_repeat_index_diagonal_actual_padding_leftzeros) = (t)) -> (((exists ff_h_pfp_diagonal_actual_padding_leftzerosentry. ff_h_pfp_diagonal_actual_padding_leftzerosentry + S (0) = S ((S (pfp_repeat_index_diagonal_actual_padding_leftzeros)) * AC)) /\ exists ff_q_pfp_diagonal_actual_padding_leftzerosentry. AB = ff_q_pfp_diagonal_actual_padding_leftzerosentry * S ((S (pfp_repeat_index_diagonal_actual_padding_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_diagonal_actual_padding_left pfrep_value_diagonal_actual_padding_left. (exists pfa_gap_diagonal_actual_padding_leftbound. pfa_gap_diagonal_actual_padding_leftbound + S (pfrep_index_diagonal_actual_padding_left) = (L)) -> (((exists ff_h_pfp_diagonal_actual_padding_leftinput. ff_h_pfp_diagonal_actual_padding_leftinput + S (pfrep_value_diagonal_actual_padding_left) = S ((S (pfrep_index_diagonal_actual_padding_left)) * ac)) /\ exists ff_q_pfp_diagonal_actual_padding_leftinput. ab = ff_q_pfp_diagonal_actual_padding_leftinput * S ((S (pfrep_index_diagonal_actual_padding_left)) * ac) + (pfrep_value_diagonal_actual_padding_left))) -> (((exists ff_h_pfp_diagonal_actual_padding_leftoutput. ff_h_pfp_diagonal_actual_padding_leftoutput + S (pfrep_value_diagonal_actual_padding_left) = S ((S ((t)+pfrep_index_diagonal_actual_padding_left)) * AC)) /\ exists ff_q_pfp_diagonal_actual_padding_leftoutput. AB = ff_q_pfp_diagonal_actual_padding_leftoutput * S ((S ((t)+pfrep_index_diagonal_actual_padding_left)) * AC) + (pfrep_value_diagonal_actual_padding_left))))))) -> (forall pfc_index_diagonal_pad_old_left. (exists pfa_gap_diagonal_pad_old_leftbound. pfa_gap_diagonal_pad_old_leftbound + S (pfc_index_diagonal_pad_old_left) = (S i)) -> exists pfc_value_diagonal_pad_old_left. ((((exists ff_h_pfp_diagonal_pad_old_leftentry. ff_h_pfp_diagonal_pad_old_leftentry + S (pfc_value_diagonal_pad_old_left) = S ((S (pfc_index_diagonal_pad_old_left)) * dc)) /\ exists ff_q_pfp_diagonal_pad_old_leftentry. db = ff_q_pfp_diagonal_pad_old_leftentry * S ((S (pfc_index_diagonal_pad_old_left)) * dc) + (pfc_value_diagonal_pad_old_left))) /\ ((exists pfc_complement_diagonal_pad_old_leftterm pfc_left_diagonal_pad_old_leftterm pfc_right_diagonal_pad_old_leftterm. (((pfc_index_diagonal_pad_old_left)+pfc_complement_diagonal_pad_old_leftterm=(i)) /\ ((((((exists pfa_gap_diagonal_pad_old_lefttermleftinside. pfa_gap_diagonal_pad_old_lefttermleftinside + S (pfc_index_diagonal_pad_old_left) = (L)) /\ ((((exists ff_h_pfp_diagonal_pad_old_lefttermleftentry. ff_h_pfp_diagonal_pad_old_lefttermleftentry + S (pfc_left_diagonal_pad_old_leftterm) = S ((S (pfc_index_diagonal_pad_old_left)) * ac)) /\ exists ff_q_pfp_diagonal_pad_old_lefttermleftentry. ab = ff_q_pfp_diagonal_pad_old_lefttermleftentry * S ((S (pfc_index_diagonal_pad_old_left)) * ac) + (pfc_left_diagonal_pad_old_leftterm)))))) \/ (((exists pfc_gap_diagonal_pad_old_lefttermleftoutside. pfc_gap_diagonal_pad_old_lefttermleftoutside+(L)=(pfc_index_diagonal_pad_old_left)) /\ (((pfc_left_diagonal_pad_old_leftterm)=0))))) /\ ((((((exists pfa_gap_diagonal_pad_old_lefttermrightinside. pfa_gap_diagonal_pad_old_lefttermrightinside + S (pfc_complement_diagonal_pad_old_leftterm) = (M)) /\ ((((exists ff_h_pfp_diagonal_pad_old_lefttermrightentry. ff_h_pfp_diagonal_pad_old_lefttermrightentry + S (pfc_right_diagonal_pad_old_leftterm) = S ((S (pfc_complement_diagonal_pad_old_leftterm)) * bc)) /\ exists ff_q_pfp_diagonal_pad_old_lefttermrightentry. bb = ff_q_pfp_diagonal_pad_old_lefttermrightentry * S ((S (pfc_complement_diagonal_pad_old_leftterm)) * bc) + (pfc_right_diagonal_pad_old_leftterm)))))) \/ (((exists pfc_gap_diagonal_pad_old_lefttermrightoutside. pfc_gap_diagonal_pad_old_lefttermrightoutside+(M)=(pfc_complement_diagonal_pad_old_leftterm)) /\ (((pfc_right_diagonal_pad_old_leftterm)=0))))) /\ (((pfc_value_diagonal_pad_old_left)=pfc_left_diagonal_pad_old_leftterm*pfc_right_diagonal_pad_old_leftterm))))))))))) -> (forall pfc_index_diagonal_pad_new_left. (exists pfa_gap_diagonal_pad_new_leftbound. pfa_gap_diagonal_pad_new_leftbound + S (pfc_index_diagonal_pad_new_left) = (S (t+i))) -> exists pfc_value_diagonal_pad_new_left. ((((exists ff_h_pfp_diagonal_pad_new_leftentry. ff_h_pfp_diagonal_pad_new_leftentry + S (pfc_value_diagonal_pad_new_left) = S ((S (pfc_index_diagonal_pad_new_left)) * ec)) /\ exists ff_q_pfp_diagonal_pad_new_leftentry. eb = ff_q_pfp_diagonal_pad_new_leftentry * S ((S (pfc_index_diagonal_pad_new_left)) * ec) + (pfc_value_diagonal_pad_new_left))) /\ ((exists pfc_complement_diagonal_pad_new_leftterm pfc_left_diagonal_pad_new_leftterm pfc_right_diagonal_pad_new_leftterm. (((pfc_index_diagonal_pad_new_left)+pfc_complement_diagonal_pad_new_leftterm=(t+i)) /\ ((((((exists pfa_gap_diagonal_pad_new_lefttermleftinside. pfa_gap_diagonal_pad_new_lefttermleftinside + S (pfc_index_diagonal_pad_new_left) = (t+L)) /\ ((((exists ff_h_pfp_diagonal_pad_new_lefttermleftentry. ff_h_pfp_diagonal_pad_new_lefttermleftentry + S (pfc_left_diagonal_pad_new_leftterm) = S ((S (pfc_index_diagonal_pad_new_left)) * AC)) /\ exists ff_q_pfp_diagonal_pad_new_lefttermleftentry. AB = ff_q_pfp_diagonal_pad_new_lefttermleftentry * S ((S (pfc_index_diagonal_pad_new_left)) * AC) + (pfc_left_diagonal_pad_new_leftterm)))))) \/ (((exists pfc_gap_diagonal_pad_new_lefttermleftoutside. pfc_gap_diagonal_pad_new_lefttermleftoutside+(t+L)=(pfc_index_diagonal_pad_new_left)) /\ (((pfc_left_diagonal_pad_new_leftterm)=0))))) /\ ((((((exists pfa_gap_diagonal_pad_new_lefttermrightinside. pfa_gap_diagonal_pad_new_lefttermrightinside + S (pfc_complement_diagonal_pad_new_leftterm) = (M)) /\ ((((exists ff_h_pfp_diagonal_pad_new_lefttermrightentry. ff_h_pfp_diagonal_pad_new_lefttermrightentry + S (pfc_right_diagonal_pad_new_leftterm) = S ((S (pfc_complement_diagonal_pad_new_leftterm)) * bc)) /\ exists ff_q_pfp_diagonal_pad_new_lefttermrightentry. bb = ff_q_pfp_diagonal_pad_new_lefttermrightentry * S ((S (pfc_complement_diagonal_pad_new_leftterm)) * bc) + (pfc_right_diagonal_pad_new_leftterm)))))) \/ (((exists pfc_gap_diagonal_pad_new_lefttermrightoutside. pfc_gap_diagonal_pad_new_lefttermrightoutside+(M)=(pfc_complement_diagonal_pad_new_leftterm)) /\ (((pfc_right_diagonal_pad_new_leftterm)=0))))) /\ (((pfc_value_diagonal_pad_new_left)=pfc_left_diagonal_pad_new_leftterm*pfc_right_diagonal_pad_new_leftterm))))))))))) -> (((forall pfp_repeat_index_diagonal_pad_result_leftzeros. (exists pfa_gap_diagonal_pad_result_leftzerosindex. pfa_gap_diagonal_pad_result_leftzerosindex + S (pfp_repeat_index_diagonal_pad_result_leftzeros) = (t)) -> (((exists ff_h_pfp_diagonal_pad_result_leftzerosentry. ff_h_pfp_diagonal_pad_result_leftzerosentry + S (0) = S ((S (pfp_repeat_index_diagonal_pad_result_leftzeros)) * ec)) /\ exists ff_q_pfp_diagonal_pad_result_leftzerosentry. eb = ff_q_pfp_diagonal_pad_result_leftzerosentry * S ((S (pfp_repeat_index_diagonal_pad_result_leftzeros)) * ec) + (0)))) /\ ((forall pfrep_index_diagonal_pad_result_left pfrep_value_diagonal_pad_result_left. (exists pfa_gap_diagonal_pad_result_leftbound. pfa_gap_diagonal_pad_result_leftbound + S (pfrep_index_diagonal_pad_result_left) = (S i)) -> (((exists ff_h_pfp_diagonal_pad_result_leftinput. ff_h_pfp_diagonal_pad_result_leftinput + S (pfrep_value_diagonal_pad_result_left) = S ((S (pfrep_index_diagonal_pad_result_left)) * dc)) /\ exists ff_q_pfp_diagonal_pad_result_leftinput. db = ff_q_pfp_diagonal_pad_result_leftinput * S ((S (pfrep_index_diagonal_pad_result_left)) * dc) + (pfrep_value_diagonal_pad_result_left))) -> (((exists ff_h_pfp_diagonal_pad_result_leftoutput. ff_h_pfp_diagonal_pad_result_leftoutput + S (pfrep_value_diagonal_pad_result_left) = S ((S ((t)+pfrep_index_diagonal_pad_result_left)) * ec)) /\ exists ff_q_pfp_diagonal_pad_result_leftoutput. eb = ff_q_pfp_diagonal_pad_result_leftoutput * S ((S ((t)+pfrep_index_diagonal_pad_result_left)) * ec) + (pfrep_value_diagonal_pad_result_left)))))))

Complete tactic proof in conservative notation

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

124 script commands · 22 reading checkpoints · 5 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 term left padding zero leftpolynomial diagonal term left padding left
01Fix variables and assumptionsL1–10

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

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro L
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro M
  7. L7
    intro AB
  8. L8
    intro AC
  9. L9
    intro t
  10. L10
    intro i
02Fix variables and assumptionsL11–17

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

  1. L11
    intro db
  2. L12
    intro dc
  3. L13
    intro eb
  4. L14
    intro ec
  5. L15
    intro hpad
  6. L16
    intro hold
  7. L17
    intro hnew
03Separate the logical casesL18–18

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

  1. L18
    split
04Fix variables and assumptionsL19–20

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

  1. L19
    intro j
  2. L20
    intro hj
05Establish hvL21–30

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

  1. L21
    have hv : ∃ z. BetaAt(eb,ec,j,z) ∧ PolynomialDiagonalTerm(AB,AC,t + L,bb,bc,M,t + i,j,z)Definitions: BetaAt(eb,ec,j,z)PolynomialDiagonalTerm(AB,AC,t + L,bb,bc,M,t + i,j,z)Original native command in the exact edition
  2. L22
    specialize hnew (j)
  3. L23
    apply hnew
  4. L24
    specialize le_trans (S j)
  5. L25
    specialize le_trans (t)
  6. L26
    specialize le_trans (S (t+i))
  7. L27
    apply le_trans
  8. L28
    exact hj
  9. L29
    specialize le_succ (t)
  10. L30
    specialize le_succ (t+i)
06Use earlier factsL31–34

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

  1. L31
    apply le_succ
  2. L32
    specialize le_add_right (t)
  3. L33
    specialize le_add_right (i)
  4. L34
    apply le_add_right
07Separate the logical casesL35–36

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

  1. L35
    cases hv
  2. L36
    cases hv_witness
08Establish hzL37–46

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

  1. L37
    have hz : x=0
  2. L38
    specialize polynomial_diagonal_term_left_padding_zero_left (ab)
  3. L39
    specialize polynomial_diagonal_term_left_padding_zero_left (ac)
  4. L40
    specialize polynomial_diagonal_term_left_padding_zero_left (L)
  5. L41
    specialize polynomial_diagonal_term_left_padding_zero_left (bb)
  6. L42
    specialize polynomial_diagonal_term_left_padding_zero_left (bc)
  7. L43
    specialize polynomial_diagonal_term_left_padding_zero_left (M)
  8. L44
    specialize polynomial_diagonal_term_left_padding_zero_left (AB)
  9. L45
    specialize polynomial_diagonal_term_left_padding_zero_left (AC)
  10. L46
    specialize polynomial_diagonal_term_left_padding_zero_left (t)
09Use earlier factsL47–53

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

  1. L47
    specialize polynomial_diagonal_term_left_padding_zero_left (t+i)
  2. L48
    specialize polynomial_diagonal_term_left_padding_zero_left (j)
  3. L49
    specialize polynomial_diagonal_term_left_padding_zero_left (x)
  4. L50
    apply polynomial_diagonal_term_left_padding_zero_left
  5. L51
    exact hpad
  6. L52
    exact hj
  7. L53
    exact hv_witness_right
10Calculate and transport equalitiesL54–55

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

  1. L54
    rewrite hz at hv_witness_left
  2. L55
    rewrite hz at hv_witness_left
11Use earlier factsL56–56

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

  1. L56
    exact hv_witness_left
12Fix variables and assumptionsL57–60

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

  1. L57
    intro j
  2. L58
    intro a
  3. L59
    intro hj
  4. L60
    intro ha
13Establish htermL61–70

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

  1. L61
    have hterm : PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,a)Definitions: PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,a)Original native command in the exact edition
  2. L62
    specialize polynomial_diagonal_prefix_entry (ab)
  3. L63
    specialize polynomial_diagonal_prefix_entry (ac)
  4. L64
    specialize polynomial_diagonal_prefix_entry (L)
  5. L65
    specialize polynomial_diagonal_prefix_entry (bb)
  6. L66
    specialize polynomial_diagonal_prefix_entry (bc)
  7. L67
    specialize polynomial_diagonal_prefix_entry (M)
  8. L68
    specialize polynomial_diagonal_prefix_entry (i)
  9. L69
    specialize polynomial_diagonal_prefix_entry (db)
  10. L70
    specialize polynomial_diagonal_prefix_entry (dc)
14Use earlier factsL71–77

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

  1. L71
    specialize polynomial_diagonal_prefix_entry (S i)
  2. L72
    specialize polynomial_diagonal_prefix_entry (j)
  3. L73
    specialize polynomial_diagonal_prefix_entry (a)
  4. L74
    apply polynomial_diagonal_prefix_entry
  5. L75
    exact hold
  6. L76
    exact hj
  7. L77
    exact ha
15Establish hvL78–87

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

  1. L78
    have hv : ∃ z. BetaAt(eb,ec,t + j,z) ∧ PolynomialDiagonalTerm(AB,AC,t + L,bb,bc,M,t + i,t + j,z)Definitions: BetaAt(eb,ec,t + j,z)PolynomialDiagonalTerm(AB,AC,t + L,bb,bc,M,t + i,t + j,z)Original native command in the exact edition
  2. L79
    specialize hnew (t+j)
  3. L80
    apply hnew
  4. L81
    specialize succ_le_succ (t+j)
  5. L82
    specialize succ_le_succ (t+i)
  6. L83
    apply succ_le_succ
  7. L84
    specialize add_le_add_left (j)
  8. L85
    specialize add_le_add_left (i)
  9. L86
    specialize add_le_add_left (t)
  10. L87
    apply add_le_add_left
16Use earlier factsL88–91

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

  1. L88
    specialize le_of_succ_le_succ (j)
  2. L89
    specialize le_of_succ_le_succ (i)
  3. L90
    apply le_of_succ_le_succ
  4. L91
    exact hj
17Separate the logical casesL92–93

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

  1. L92
    cases hv
  2. L93
    cases hv_witness
18Establish heqL94–103

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

  1. L94
    have heq : x=a
  2. L95
    specialize polynomial_diagonal_term_functional (AB)
  3. L96
    specialize polynomial_diagonal_term_functional (AC)
  4. L97
    specialize polynomial_diagonal_term_functional (t+L)
  5. L98
    specialize polynomial_diagonal_term_functional (bb)
  6. L99
    specialize polynomial_diagonal_term_functional (bc)
  7. L100
    specialize polynomial_diagonal_term_functional (M)
  8. L101
    specialize polynomial_diagonal_term_functional (t+i)
  9. L102
    specialize polynomial_diagonal_term_functional (t+j)
  10. L103
    specialize polynomial_diagonal_term_functional (x)
19Use earlier factsL104–113

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

  1. L104
    specialize polynomial_diagonal_term_functional (a)
  2. L105
    apply polynomial_diagonal_term_functional
  3. L106
    exact hv_witness_right
  4. L107
    specialize polynomial_diagonal_term_left_padding_left (ab)
  5. L108
    specialize polynomial_diagonal_term_left_padding_left (ac)
  6. L109
    specialize polynomial_diagonal_term_left_padding_left (L)
  7. L110
    specialize polynomial_diagonal_term_left_padding_left (bb)
  8. L111
    specialize polynomial_diagonal_term_left_padding_left (bc)
  9. L112
    specialize polynomial_diagonal_term_left_padding_left (M)
  10. L113
    specialize polynomial_diagonal_term_left_padding_left (AB)
20Use earlier factsL114–121

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

  1. L114
    specialize polynomial_diagonal_term_left_padding_left (AC)
  2. L115
    specialize polynomial_diagonal_term_left_padding_left (t)
  3. L116
    specialize polynomial_diagonal_term_left_padding_left (i)
  4. L117
    specialize polynomial_diagonal_term_left_padding_left (j)
  5. L118
    specialize polynomial_diagonal_term_left_padding_left (a)
  6. L119
    apply polynomial_diagonal_term_left_padding_left
  7. L120
    exact hpad
  8. L121
    exact hterm
21Calculate and transport equalitiesL122–123

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

  1. L122
    rewrite heq at hv_witness_left
  2. L123
    rewrite heq at hv_witness_left
22Use earlier factsL124–124

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

  1. L124
    exact hv_witness_left

Library-wide reading audit

Original defined command ledger · 124 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro L
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro M
  7. 0007intro AB
  8. 0008intro AC
  9. 0009intro t
  10. 0010intro i
  11. 0011intro db
  12. 0012intro dc
  13. 0013intro eb
  14. 0014intro ec
  15. 0015intro hpad
  16. 0016intro hold
  17. 0017intro hnew
  18. 0018split
  19. 0019intro j
  20. 0020intro hj
  21. 0021have hv : ∃ z. BetaAt(eb,ec,j,z) ∧ PolynomialDiagonalTerm(AB,AC,t + L,bb,bc,M,t + i,j,z)
  22. 0022specialize hnew (j)
  23. 0023apply hnew
  24. 0024specialize le_trans (S j)
  25. 0025specialize le_trans (t)
  26. 0026specialize le_trans (S (t+i))
  27. 0027apply le_trans
  28. 0028exact hj
  29. 0029specialize le_succ (t)
  30. 0030specialize le_succ (t+i)
  31. 0031apply le_succ
  32. 0032specialize le_add_right (t)
  33. 0033specialize le_add_right (i)
  34. 0034apply le_add_right
  35. 0035cases hv
  36. 0036cases hv_witness
  37. 0037have hz : x=0
  38. 0038specialize polynomial_diagonal_term_left_padding_zero_left (ab)
  39. 0039specialize polynomial_diagonal_term_left_padding_zero_left (ac)
  40. 0040specialize polynomial_diagonal_term_left_padding_zero_left (L)
  41. 0041specialize polynomial_diagonal_term_left_padding_zero_left (bb)
  42. 0042specialize polynomial_diagonal_term_left_padding_zero_left (bc)
  43. 0043specialize polynomial_diagonal_term_left_padding_zero_left (M)
  44. 0044specialize polynomial_diagonal_term_left_padding_zero_left (AB)
  45. 0045specialize polynomial_diagonal_term_left_padding_zero_left (AC)
  46. 0046specialize polynomial_diagonal_term_left_padding_zero_left (t)
  47. 0047specialize polynomial_diagonal_term_left_padding_zero_left (t+i)
  48. 0048specialize polynomial_diagonal_term_left_padding_zero_left (j)
  49. 0049specialize polynomial_diagonal_term_left_padding_zero_left (x)
  50. 0050apply polynomial_diagonal_term_left_padding_zero_left
  51. 0051exact hpad
  52. 0052exact hj
  53. 0053exact hv_witness_right
  54. 0054rewrite hz at hv_witness_left
  55. 0055rewrite hz at hv_witness_left
  56. 0056exact hv_witness_left
  57. 0057intro j
  58. 0058intro a
  59. 0059intro hj
  60. 0060intro ha
  61. 0061have hterm : PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,a)
  62. 0062specialize polynomial_diagonal_prefix_entry (ab)
  63. 0063specialize polynomial_diagonal_prefix_entry (ac)
  64. 0064specialize polynomial_diagonal_prefix_entry (L)
  65. 0065specialize polynomial_diagonal_prefix_entry (bb)
  66. 0066specialize polynomial_diagonal_prefix_entry (bc)
  67. 0067specialize polynomial_diagonal_prefix_entry (M)
  68. 0068specialize polynomial_diagonal_prefix_entry (i)
  69. 0069specialize polynomial_diagonal_prefix_entry (db)
  70. 0070specialize polynomial_diagonal_prefix_entry (dc)
  71. 0071specialize polynomial_diagonal_prefix_entry (S i)
  72. 0072specialize polynomial_diagonal_prefix_entry (j)
  73. 0073specialize polynomial_diagonal_prefix_entry (a)
  74. 0074apply polynomial_diagonal_prefix_entry
  75. 0075exact hold
  76. 0076exact hj
  77. 0077exact ha
  78. 0078have hv : ∃ z. BetaAt(eb,ec,t + j,z) ∧ PolynomialDiagonalTerm(AB,AC,t + L,bb,bc,M,t + i,t + j,z)
  79. 0079specialize hnew (t+j)
  80. 0080apply hnew
  81. 0081specialize succ_le_succ (t+j)
  82. 0082specialize succ_le_succ (t+i)
  83. 0083apply succ_le_succ
  84. 0084specialize add_le_add_left (j)
  85. 0085specialize add_le_add_left (i)
  86. 0086specialize add_le_add_left (t)
  87. 0087apply add_le_add_left
  88. 0088specialize le_of_succ_le_succ (j)
  89. 0089specialize le_of_succ_le_succ (i)
  90. 0090apply le_of_succ_le_succ
  91. 0091exact hj
  92. 0092cases hv
  93. 0093cases hv_witness
  94. 0094have heq : x=a
  95. 0095specialize polynomial_diagonal_term_functional (AB)
  96. 0096specialize polynomial_diagonal_term_functional (AC)
  97. 0097specialize polynomial_diagonal_term_functional (t+L)
  98. 0098specialize polynomial_diagonal_term_functional (bb)
  99. 0099specialize polynomial_diagonal_term_functional (bc)
  100. 0100specialize polynomial_diagonal_term_functional (M)
  101. 0101specialize polynomial_diagonal_term_functional (t+i)
  102. 0102specialize polynomial_diagonal_term_functional (t+j)
  103. 0103specialize polynomial_diagonal_term_functional (x)
  104. 0104specialize polynomial_diagonal_term_functional (a)
  105. 0105apply polynomial_diagonal_term_functional
  106. 0106exact hv_witness_right
  107. 0107specialize polynomial_diagonal_term_left_padding_left (ab)
  108. 0108specialize polynomial_diagonal_term_left_padding_left (ac)
  109. 0109specialize polynomial_diagonal_term_left_padding_left (L)
  110. 0110specialize polynomial_diagonal_term_left_padding_left (bb)
  111. 0111specialize polynomial_diagonal_term_left_padding_left (bc)
  112. 0112specialize polynomial_diagonal_term_left_padding_left (M)
  113. 0113specialize polynomial_diagonal_term_left_padding_left (AB)
  114. 0114specialize polynomial_diagonal_term_left_padding_left (AC)
  115. 0115specialize polynomial_diagonal_term_left_padding_left (t)
  116. 0116specialize polynomial_diagonal_term_left_padding_left (i)
  117. 0117specialize polynomial_diagonal_term_left_padding_left (j)
  118. 0118specialize polynomial_diagonal_term_left_padding_left (a)
  119. 0119apply polynomial_diagonal_term_left_padding_left
  120. 0120exact hpad
  121. 0121exact hterm
  122. 0122rewrite heq at hv_witness_left
  123. 0123rewrite heq at hv_witness_left
  124. 0124exact hv_witness_left