LU0018 · theorem body

lucas_digit_chain_extend

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

One constructive quotient division and two beta-prefix extensions append the next genuinely successive digit without disturbing any earlier step.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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.

Statement with defined notation

∀ p. ∀ n. ∀ qb. ∀ qc. ∀ db. ∀ dc. ∀ l. ¬p = 0 → BetaAt(qb,qc,0,n) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ m. BetaAt(qb,qc,x,y) ∧ (BetaAt(qb,qc,S x,z) ∧ (BetaAt(db,dc,x,m) ∧ DivRem(y,p,z,m)))) → ∃ x. ∃ y. ∃ z. ∃ m. BetaAt(x,y,0,n) ∧ (∀ k. Lt(k,S l) → ∃ i. ∃ j. ∃ u. BetaAt(x,y,k,i) ∧ (BetaAt(x,y,S k,j) ∧ (BetaAt(z,m,k,u) ∧ DivRem(i,p,j,u))))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0007 DivRem PD0013 BetaAt

In local proof propositions

PD0002 Lt PD0007 DivRem PD0013 BetaAt
Exact expanded first-order statement
forall p n qb qc db dc l. ~(p = 0) -> (((((exists ff_h_lmd_extend_source_initial. ff_h_lmd_extend_source_initial + S (n) = S ((S (0)) * qc)) /\ exists ff_q_lmd_extend_source_initial. qb = ff_q_lmd_extend_source_initial * S ((S (0)) * qc) + (n))) /\ forall lmd_index_extend_source. (exists lmd_gap_extend_source_index. lmd_gap_extend_source_index + S (lmd_index_extend_source) = (l)) -> exists lmd_current_extend_source lmd_successor_extend_source lmd_digit_extend_source. ((((exists ff_h_lmd_extend_source_current. ff_h_lmd_extend_source_current + S (lmd_current_extend_source) = S ((S (lmd_index_extend_source)) * qc)) /\ exists ff_q_lmd_extend_source_current. qb = ff_q_lmd_extend_source_current * S ((S (lmd_index_extend_source)) * qc) + (lmd_current_extend_source))) /\ ((((exists ff_h_lmd_extend_source_successor. ff_h_lmd_extend_source_successor + S (lmd_successor_extend_source) = S ((S (S lmd_index_extend_source)) * qc)) /\ exists ff_q_lmd_extend_source_successor. qb = ff_q_lmd_extend_source_successor * S ((S (S lmd_index_extend_source)) * qc) + (lmd_successor_extend_source))) /\ ((((exists ff_h_lmd_extend_source_digit. ff_h_lmd_extend_source_digit + S (lmd_digit_extend_source) = S ((S (lmd_index_extend_source)) * dc)) /\ exists ff_q_lmd_extend_source_digit. db = ff_q_lmd_extend_source_digit * S ((S (lmd_index_extend_source)) * dc) + (lmd_digit_extend_source))) /\ ((lmd_current_extend_source = (p) * (lmd_successor_extend_source) + (lmd_digit_extend_source)) /\ (exists lmd_gap_extend_source_digit_bound. lmd_gap_extend_source_digit_bound + S (lmd_digit_extend_source) = (p)))))))) -> exists z t u v. (((((exists ff_h_lmd_extend_result_initial. ff_h_lmd_extend_result_initial + S (n) = S ((S (0)) * t)) /\ exists ff_q_lmd_extend_result_initial. z = ff_q_lmd_extend_result_initial * S ((S (0)) * t) + (n))) /\ forall lmd_index_extend_result. (exists lmd_gap_extend_result_index. lmd_gap_extend_result_index + S (lmd_index_extend_result) = (S l)) -> exists lmd_current_extend_result lmd_successor_extend_result lmd_digit_extend_result. ((((exists ff_h_lmd_extend_result_current. ff_h_lmd_extend_result_current + S (lmd_current_extend_result) = S ((S (lmd_index_extend_result)) * t)) /\ exists ff_q_lmd_extend_result_current. z = ff_q_lmd_extend_result_current * S ((S (lmd_index_extend_result)) * t) + (lmd_current_extend_result))) /\ ((((exists ff_h_lmd_extend_result_successor. ff_h_lmd_extend_result_successor + S (lmd_successor_extend_result) = S ((S (S lmd_index_extend_result)) * t)) /\ exists ff_q_lmd_extend_result_successor. z = ff_q_lmd_extend_result_successor * S ((S (S lmd_index_extend_result)) * t) + (lmd_successor_extend_result))) /\ ((((exists ff_h_lmd_extend_result_digit. ff_h_lmd_extend_result_digit + S (lmd_digit_extend_result) = S ((S (lmd_index_extend_result)) * v)) /\ exists ff_q_lmd_extend_result_digit. u = ff_q_lmd_extend_result_digit * S ((S (lmd_index_extend_result)) * v) + (lmd_digit_extend_result))) /\ ((lmd_current_extend_result = (p) * (lmd_successor_extend_result) + (lmd_digit_extend_result)) /\ (exists lmd_gap_extend_result_digit_bound. lmd_gap_extend_result_digit_bound + S (lmd_digit_extend_result) = (p))))))))

Proof neighborhood

Direct theorem prerequisites

beta_at_exists · Stable closed division_remainder_exists · Stable closed beta_prefix_extend · Stable closed finite_lt_succ_eq_or_lt · Stable closed zero_add · Stable closed lt_of_lt_of_le · Stable closed le_succ_self · Stable closed succ_le_succ · Stable closed

Direct theorem dependents

LU0019 lucas_digit_chain_exists

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

132 script commands · 44 reading checkpoints · 8 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.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro qb
  4. L4
    intro qc
  5. L5
    intro db
  6. L6
    intro dc
  7. L7
    intro l
  8. L8
    intro hnonzero
  9. L9
    intro hchain
02Separate the logical casesL10–10

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

  1. L10
    cases hchain
03Establish hlastL11–15

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

  1. L11
    have hlast : ∃ q. BetaAt(qb,qc,l,q)Definitions: BetaAt(qb,qc,l,q)Original native command in the exact edition
  2. L12
    specialize beta_at_exists qb
  3. L13
    specialize beta_at_exists qc
  4. L14
    specialize beta_at_exists l
  5. L15
    exact beta_at_exists
04Separate the logical casesL16–16

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

  1. L16
    cases hlast
05Establish hdivisionL17–21

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

  1. L17
    have hdivision : ∃ Q. ∃ d. DivRem(x,p,Q,d)Definitions: DivRem(x,p,Q,d)Original native command in the exact edition
  2. L18
    specialize division_remainder_exists p
  3. L19
    specialize division_remainder_exists x
  4. L20
    apply division_remainder_exists
  5. L21
    exact hnonzero
06Separate the logical casesL22–24

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

  1. L22
    cases hdivision
  2. L23
    cases hdivision_witness
  3. L24
    cases hdivision_witness_witness
07Establish hqextendL25–30

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

  1. L25
    have hqextend : ∃ z. ∃ t. BetaAt(z,t,S l,x1) ∧ (∀ x. ∀ y. Lt(x,S l) → BetaAt(qb,qc,x,y) → BetaAt(z,t,x,y))Definitions: BetaAt(z,t,S l,x1)Lt(x,S l)BetaAt(qb,qc,x,y)BetaAt(z,t,x,y)Original native command in the exact edition
  2. L26
    specialize beta_prefix_extend (S l)
  3. L27
    specialize beta_prefix_extend qb
  4. L28
    specialize beta_prefix_extend qc
  5. L29
    specialize beta_prefix_extend x1
  6. L30
    exact beta_prefix_extend
08Separate the logical casesL31–33

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

  1. L31
    cases hqextend
  2. L32
    cases hqextend_witness
  3. L33
    cases hqextend_witness_witness
09Establish hdextendL34–39

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

  1. L34
    have hdextend : ∃ u. ∃ v. BetaAt(u,v,l,x2) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(db,dc,x,y) → BetaAt(u,v,x,y))Definitions: BetaAt(u,v,l,x2)Lt(x,l)BetaAt(db,dc,x,y)BetaAt(u,v,x,y)Original native command in the exact edition
  2. L35
    specialize beta_prefix_extend l
  3. L36
    specialize beta_prefix_extend db
  4. L37
    specialize beta_prefix_extend dc
  5. L38
    specialize beta_prefix_extend x2
  6. L39
    exact beta_prefix_extend
10Separate the logical casesL40–42

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

  1. L40
    cases hdextend
  2. L41
    cases hdextend_witness
  3. L42
    cases hdextend_witness_witness
11Construct an explicit witnessL43–46

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

  1. L43
    exists x3
  2. L44
    exists x4
  3. L45
    exists x5
  4. L46
    exists x6
12Separate the logical casesL47–47

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

  1. L47
    split
13Use earlier factsL48–50

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

  1. L48
    specialize hqextend_witness_witness_right 0
  2. L49
    specialize hqextend_witness_witness_right n
  3. L50
    apply hqextend_witness_witness_right
14Construct an explicit witnessL51–51

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

  1. L51
    exists l
15Calculate and transport equalitiesL52–52

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

  1. L52
    simp
16Use earlier factsL53–53

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

  1. L53
    exact hchain_left
17Fix variables and assumptionsL54–55

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

  1. L54
    intro i
  2. L55
    intro hi
18Establish hsplitL56–60

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

  1. L56
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L57
    specialize finite_lt_succ_eq_or_lt l
  3. L58
    specialize finite_lt_succ_eq_or_lt i
  4. L59
    apply finite_lt_succ_eq_or_lt
  5. L60
    exact hi
19Separate the logical casesL61–61

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

  1. L61
    cases hsplit
20Calculate and transport equalitiesL62–67

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

  1. L62
    rewrite hsplit_left
  2. L63
    rewrite hsplit_left
  3. L64
    rewrite hsplit_left
  4. L65
    rewrite hsplit_left
  5. L66
    rewrite hsplit_left
  6. L67
    rewrite hsplit_left
21Construct an explicit witnessL68–70

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

  1. L68
    exists x
  2. L69
    exists x1
  3. L70
    exists x2
22Separate the logical casesL71–71

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

  1. L71
    split
23Use earlier factsL72–74

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

  1. L72
    specialize hqextend_witness_witness_right l
  2. L73
    specialize hqextend_witness_witness_right x
  3. L74
    apply hqextend_witness_witness_right
24Construct an explicit witnessL75–75

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

  1. L75
    exists 0
25Use earlier factsL76–77

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

  1. L76
    apply zero_add
  2. L77
    exact hlast_witness
26Separate the logical casesL78–78

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

  1. L78
    split
27Use earlier factsL79–79

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

  1. L79
    exact hqextend_witness_witness_left
28Separate the logical casesL80–80

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

  1. L80
    split
29Use earlier factsL81–81

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

  1. L81
    exact hdextend_witness_witness_left
30Separate the logical casesL82–82

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

  1. L82
    split
31Use earlier factsL83–84

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

  1. L83
    exact hdivision_witness_witness_left
  2. L84
    exact hdivision_witness_witness_right
32Establish hpreviousL85–88

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

  1. L85
    have hprevious : ∃ q. ∃ Q. ∃ d. BetaAt(qb,qc,i,q) ∧ (BetaAt(qb,qc,S i,Q) ∧ (BetaAt(db,dc,i,d) ∧ DivRem(q,p,Q,d)))Definitions: BetaAt(qb,qc,i,q)BetaAt(qb,qc,S i,Q)BetaAt(db,dc,i,d)DivRem(q,p,Q,d)Original native command in the exact edition
  2. L86
    specialize hchain_right i
  3. L87
    apply hchain_right
  4. L88
    exact hsplit_right
33Separate the logical casesL89–95

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

  1. L89
    cases hprevious
  2. L90
    cases hprevious_witness
  3. L91
    cases hprevious_witness_witness
  4. L92
    cases hprevious_witness_witness_witness
  5. L93
    cases hprevious_witness_witness_witness_right
  6. L94
    cases hprevious_witness_witness_witness_right_right
  7. L95
    cases hprevious_witness_witness_witness_right_right_right
34Establish hipreserveL96–103

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

  1. L96
    have hipreserve : Lt(i,S l)Definitions: Lt(i,S l)Original native command in the exact edition
  2. L97
    specialize lt_of_lt_of_le i
  3. L98
    specialize lt_of_lt_of_le l
  4. L99
    specialize lt_of_lt_of_le (S l)
  5. L100
    apply lt_of_lt_of_le
  6. L101
    exact hsplit_right
  7. L102
    specialize le_succ_self l
  8. L103
    exact le_succ_self
35Establish hnextpreserveL104–108

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

  1. L104
    have hnextpreserve : Lt(S i,S l)Definitions: Lt(S i,S l)Original native command in the exact edition
  2. L105
    specialize succ_le_succ (S i)
  3. L106
    specialize succ_le_succ l
  4. L107
    apply succ_le_succ
  5. L108
    exact hsplit_right
36Construct an explicit witnessL109–111

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

  1. L109
    exists x7
  2. L110
    exists x8
  3. L111
    exists x9
37Separate the logical casesL112–112

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

  1. L112
    split
38Use earlier factsL113–117

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

  1. L113
    specialize hqextend_witness_witness_right i
  2. L114
    specialize hqextend_witness_witness_right x7
  3. L115
    apply hqextend_witness_witness_right
  4. L116
    exact hipreserve
  5. L117
    exact hprevious_witness_witness_witness_left
39Separate the logical casesL118–118

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

  1. L118
    split
40Use earlier factsL119–123

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

  1. L119
    specialize hqextend_witness_witness_right (S i)
  2. L120
    specialize hqextend_witness_witness_right x8
  3. L121
    apply hqextend_witness_witness_right
  4. L122
    exact hnextpreserve
  5. L123
    exact hprevious_witness_witness_witness_right_left
41Separate the logical casesL124–124

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

  1. L124
    split
42Use earlier factsL125–129

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

  1. L125
    specialize hdextend_witness_witness_right i
  2. L126
    specialize hdextend_witness_witness_right x9
  3. L127
    apply hdextend_witness_witness_right
  4. L128
    exact hsplit_right
  5. L129
    exact hprevious_witness_witness_witness_right_right_left
43Separate the logical casesL130–130

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

  1. L130
    split
44Use earlier factsL131–132

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

  1. L131
    exact hprevious_witness_witness_witness_right_right_right_left
  2. L132
    exact hprevious_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original defined command ledger · 132 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro qb
  4. 0004intro qc
  5. 0005intro db
  6. 0006intro dc
  7. 0007intro l
  8. 0008intro hnonzero
  9. 0009intro hchain
  10. 0010cases hchain
  11. 0011have hlast : ∃ q. BetaAt(qb,qc,l,q)
    Exact native replay linehave hlast : exists q. (((exists ff_h_lmd_last_old. ff_h_lmd_last_old + S (q) = S ((S (l)) * qc)) /\ exists ff_q_lmd_last_old. qb = ff_q_lmd_last_old * S ((S (l)) * qc) + (q)))
  12. 0012specialize beta_at_exists qb
  13. 0013specialize beta_at_exists qc
  14. 0014specialize beta_at_exists l
  15. 0015exact beta_at_exists
  16. 0016cases hlast
  17. 0017have hdivision : ∃ Q. ∃ d. DivRem(x,p,Q,d)
    Exact native replay linehave hdivision : exists Q d. ((x = p * Q + d) /\ (exists lmd_gap_new_digit_bound. lmd_gap_new_digit_bound + S (d) = (p)))
  18. 0018specialize division_remainder_exists p
  19. 0019specialize division_remainder_exists x
  20. 0020apply division_remainder_exists
  21. 0021exact hnonzero
  22. 0022cases hdivision
  23. 0023cases hdivision_witness
  24. 0024cases hdivision_witness_witness
  25. 0025have hqextend : ∃ z. ∃ t. BetaAt(z,t,S l,x1) ∧ (∀ x. ∀ y. Lt(x,S l) → BetaAt(qb,qc,x,y) → BetaAt(z,t,x,y))
    Exact native replay linehave hqextend : exists z t. ((((exists ff_h_lmd_quotient_new. ff_h_lmd_quotient_new + S (x1) = S ((S (S l)) * t)) /\ exists ff_q_lmd_quotient_new. z = ff_q_lmd_quotient_new * S ((S (S l)) * t) + (x1))) /\ forall i y. (exists lmd_gap_quotient_preserve_bound. lmd_gap_quotient_preserve_bound + S (i) = (S l)) -> (((exists ff_h_lmd_quotient_preserve_old. ff_h_lmd_quotient_preserve_old + S (y) = S ((S (i)) * qc)) /\ exists ff_q_lmd_quotient_preserve_old. qb = ff_q_lmd_quotient_preserve_old * S ((S (i)) * qc) + (y))) -> (((exists ff_h_lmd_quotient_preserve_new. ff_h_lmd_quotient_preserve_new + S (y) = S ((S (i)) * t)) /\ exists ff_q_lmd_quotient_preserve_new. z = ff_q_lmd_quotient_preserve_new * S ((S (i)) * t) + (y))))
  26. 0026specialize beta_prefix_extend (S l)
  27. 0027specialize beta_prefix_extend qb
  28. 0028specialize beta_prefix_extend qc
  29. 0029specialize beta_prefix_extend x1
  30. 0030exact beta_prefix_extend
  31. 0031cases hqextend
  32. 0032cases hqextend_witness
  33. 0033cases hqextend_witness_witness
  34. 0034have hdextend : ∃ u. ∃ v. BetaAt(u,v,l,x2) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(db,dc,x,y) → BetaAt(u,v,x,y))
    Exact native replay linehave hdextend : exists u v. ((((exists ff_h_lmd_digit_new. ff_h_lmd_digit_new + S (x2) = S ((S (l)) * v)) /\ exists ff_q_lmd_digit_new. u = ff_q_lmd_digit_new * S ((S (l)) * v) + (x2))) /\ forall i y. (exists lmd_gap_digit_preserve_bound. lmd_gap_digit_preserve_bound + S (i) = (l)) -> (((exists ff_h_lmd_digit_preserve_old. ff_h_lmd_digit_preserve_old + S (y) = S ((S (i)) * dc)) /\ exists ff_q_lmd_digit_preserve_old. db = ff_q_lmd_digit_preserve_old * S ((S (i)) * dc) + (y))) -> (((exists ff_h_lmd_digit_preserve_new. ff_h_lmd_digit_preserve_new + S (y) = S ((S (i)) * v)) /\ exists ff_q_lmd_digit_preserve_new. u = ff_q_lmd_digit_preserve_new * S ((S (i)) * v) + (y))))
  35. 0035specialize beta_prefix_extend l
  36. 0036specialize beta_prefix_extend db
  37. 0037specialize beta_prefix_extend dc
  38. 0038specialize beta_prefix_extend x2
  39. 0039exact beta_prefix_extend
  40. 0040cases hdextend
  41. 0041cases hdextend_witness
  42. 0042cases hdextend_witness_witness
  43. 0043exists x3
  44. 0044exists x4
  45. 0045exists x5
  46. 0046exists x6
  47. 0047split
  48. 0048specialize hqextend_witness_witness_right 0
  49. 0049specialize hqextend_witness_witness_right n
  50. 0050apply hqextend_witness_witness_right
  51. 0051exists l
  52. 0052simp
  53. 0053exact hchain_left
  54. 0054intro i
  55. 0055intro hi
  56. 0056have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists gap. gap + S i = l
  57. 0057specialize finite_lt_succ_eq_or_lt l
  58. 0058specialize finite_lt_succ_eq_or_lt i
  59. 0059apply finite_lt_succ_eq_or_lt
  60. 0060exact hi
  61. 0061cases hsplit
  62. 0062rewrite hsplit_left
  63. 0063rewrite hsplit_left
  64. 0064rewrite hsplit_left
  65. 0065rewrite hsplit_left
  66. 0066rewrite hsplit_left
  67. 0067rewrite hsplit_left
  68. 0068exists x
  69. 0069exists x1
  70. 0070exists x2
  71. 0071split
  72. 0072specialize hqextend_witness_witness_right l
  73. 0073specialize hqextend_witness_witness_right x
  74. 0074apply hqextend_witness_witness_right
  75. 0075exists 0
  76. 0076apply zero_add
  77. 0077exact hlast_witness
  78. 0078split
  79. 0079exact hqextend_witness_witness_left
  80. 0080split
  81. 0081exact hdextend_witness_witness_left
  82. 0082split
  83. 0083exact hdivision_witness_witness_left
  84. 0084exact hdivision_witness_witness_right
  85. 0085have hprevious : ∃ q. ∃ Q. ∃ d. BetaAt(qb,qc,i,q) ∧ (BetaAt(qb,qc,S i,Q) ∧ (BetaAt(db,dc,i,d) ∧ DivRem(q,p,Q,d)))
    Exact native replay linehave hprevious : exists q Q d. ((((exists ff_h_lmd_old_current. ff_h_lmd_old_current + S (q) = S ((S (i)) * qc)) /\ exists ff_q_lmd_old_current. qb = ff_q_lmd_old_current * S ((S (i)) * qc) + (q))) /\ ((((exists ff_h_lmd_old_next. ff_h_lmd_old_next + S (Q) = S ((S (S i)) * qc)) /\ exists ff_q_lmd_old_next. qb = ff_q_lmd_old_next * S ((S (S i)) * qc) + (Q))) /\ ((((exists ff_h_lmd_old_digit. ff_h_lmd_old_digit + S (d) = S ((S (i)) * dc)) /\ exists ff_q_lmd_old_digit. db = ff_q_lmd_old_digit * S ((S (i)) * dc) + (d))) /\ ((q = p * Q + d) /\ (exists lmd_gap_old_bound. lmd_gap_old_bound + S (d) = (p))))))
  86. 0086specialize hchain_right i
  87. 0087apply hchain_right
  88. 0088exact hsplit_right
  89. 0089cases hprevious
  90. 0090cases hprevious_witness
  91. 0091cases hprevious_witness_witness
  92. 0092cases hprevious_witness_witness_witness
  93. 0093cases hprevious_witness_witness_witness_right
  94. 0094cases hprevious_witness_witness_witness_right_right
  95. 0095cases hprevious_witness_witness_witness_right_right_right
  96. 0096have hipreserve : Lt(i,S l)
    Exact native replay linehave hipreserve : exists gap. gap + S i = S l
  97. 0097specialize lt_of_lt_of_le i
  98. 0098specialize lt_of_lt_of_le l
  99. 0099specialize lt_of_lt_of_le (S l)
  100. 0100apply lt_of_lt_of_le
  101. 0101exact hsplit_right
  102. 0102specialize le_succ_self l
  103. 0103exact le_succ_self
  104. 0104have hnextpreserve : Lt(S i,S l)
    Exact native replay linehave hnextpreserve : exists gap. gap + S (S i) = S l
  105. 0105specialize succ_le_succ (S i)
  106. 0106specialize succ_le_succ l
  107. 0107apply succ_le_succ
  108. 0108exact hsplit_right
  109. 0109exists x7
  110. 0110exists x8
  111. 0111exists x9
  112. 0112split
  113. 0113specialize hqextend_witness_witness_right i
  114. 0114specialize hqextend_witness_witness_right x7
  115. 0115apply hqextend_witness_witness_right
  116. 0116exact hipreserve
  117. 0117exact hprevious_witness_witness_witness_left
  118. 0118split
  119. 0119specialize hqextend_witness_witness_right (S i)
  120. 0120specialize hqextend_witness_witness_right x8
  121. 0121apply hqextend_witness_witness_right
  122. 0122exact hnextpreserve
  123. 0123exact hprevious_witness_witness_witness_right_left
  124. 0124split
  125. 0125specialize hdextend_witness_witness_right i
  126. 0126specialize hdextend_witness_witness_right x9
  127. 0127apply hdextend_witness_witness_right
  128. 0128exact hsplit_right
  129. 0129exact hprevious_witness_witness_witness_right_right_left
  130. 0130split
  131. 0131exact hprevious_witness_witness_witness_right_right_right_left
  132. 0132exact hprevious_witness_witness_witness_right_right_right_right