LU001D · theorem body

lucas_modular_backward_product_fold

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

Any beta-coded chain of pointwise backward modular recurrences folds into the exact terminal value times the entire beta-coded finite product.

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

∀ l. ∀ p. ∀ b. ∀ c. ∀ z. ∀ t. ∀ n. ∀ k. ∀ P. Product(b,c,l,P) → BetaAt(z,t,0,n) → BetaAt(z,t,l,k) → (∀ x. ∀ y. ∀ m. ∀ i. Lt(x,l) → BetaAt(z,t,x,y) → BetaAt(z,t,S x,m) → BetaAt(b,c,x,i) → ModEq(p,y,m · i)) → ModEq(p,n,k · P)

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 PD0008 ModEq PD0013 BetaAt PD0014 Product

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0014 Product
Exact expanded first-order statement
forall l p b c z t n k P. (exists ff_u_lmd_fold_product ff_v_lmd_fold_product. ((((exists ff_h_lmd_fold_product_start. ff_h_lmd_fold_product_start + S (1) = S ((S (0)) * ff_v_lmd_fold_product)) /\ exists ff_q_lmd_fold_product_start. ff_u_lmd_fold_product = ff_q_lmd_fold_product_start * S ((S (0)) * ff_v_lmd_fold_product) + (1))) /\ ((((exists ff_h_lmd_fold_product_terminal. ff_h_lmd_fold_product_terminal + S (P) = S ((S (l)) * ff_v_lmd_fold_product)) /\ exists ff_q_lmd_fold_product_terminal. ff_u_lmd_fold_product = ff_q_lmd_fold_product_terminal * S ((S (l)) * ff_v_lmd_fold_product) + (P))) /\ forall ff_i_lmd_fold_product. (exists ff_lt_lmd_fold_product_bound. ff_lt_lmd_fold_product_bound + S ff_i_lmd_fold_product = l) -> exists ff_p_lmd_fold_product ff_r_lmd_fold_product ff_s_lmd_fold_product. ((((exists ff_h_lmd_fold_product_factor. ff_h_lmd_fold_product_factor + S (ff_p_lmd_fold_product) = S ((S (ff_i_lmd_fold_product)) * c)) /\ exists ff_q_lmd_fold_product_factor. b = ff_q_lmd_fold_product_factor * S ((S (ff_i_lmd_fold_product)) * c) + (ff_p_lmd_fold_product))) /\ ((((exists ff_h_lmd_fold_product_partial. ff_h_lmd_fold_product_partial + S (ff_r_lmd_fold_product) = S ((S (ff_i_lmd_fold_product)) * ff_v_lmd_fold_product)) /\ exists ff_q_lmd_fold_product_partial. ff_u_lmd_fold_product = ff_q_lmd_fold_product_partial * S ((S (ff_i_lmd_fold_product)) * ff_v_lmd_fold_product) + (ff_r_lmd_fold_product))) /\ ((((exists ff_h_lmd_fold_product_successor. ff_h_lmd_fold_product_successor + S (ff_s_lmd_fold_product) = S ((S (S ff_i_lmd_fold_product)) * ff_v_lmd_fold_product)) /\ exists ff_q_lmd_fold_product_successor. ff_u_lmd_fold_product = ff_q_lmd_fold_product_successor * S ((S (S ff_i_lmd_fold_product)) * ff_v_lmd_fold_product) + (ff_s_lmd_fold_product))) /\ ff_s_lmd_fold_product = ff_r_lmd_fold_product * ff_p_lmd_fold_product)))))) -> (((exists ff_h_lmd_fold_start. ff_h_lmd_fold_start + S (n) = S ((S (0)) * t)) /\ exists ff_q_lmd_fold_start. z = ff_q_lmd_fold_start * S ((S (0)) * t) + (n))) -> (((exists ff_h_lmd_fold_terminal. ff_h_lmd_fold_terminal + S (k) = S ((S (l)) * t)) /\ exists ff_q_lmd_fold_terminal. z = ff_q_lmd_fold_terminal * S ((S (l)) * t) + (k))) -> (forall lmd_step_index_fold_trace lmd_step_source_fold_trace lmd_step_successor_fold_trace lmd_step_factor_fold_trace. (exists lmd_gap_fold_trace_bound. lmd_gap_fold_trace_bound + S (lmd_step_index_fold_trace) = (l)) -> (((exists ff_h_lmd_fold_trace_source. ff_h_lmd_fold_trace_source + S (lmd_step_source_fold_trace) = S ((S (lmd_step_index_fold_trace)) * t)) /\ exists ff_q_lmd_fold_trace_source. z = ff_q_lmd_fold_trace_source * S ((S (lmd_step_index_fold_trace)) * t) + (lmd_step_source_fold_trace))) -> (((exists ff_h_lmd_fold_trace_successor. ff_h_lmd_fold_trace_successor + S (lmd_step_successor_fold_trace) = S ((S (S lmd_step_index_fold_trace)) * t)) /\ exists ff_q_lmd_fold_trace_successor. z = ff_q_lmd_fold_trace_successor * S ((S (S lmd_step_index_fold_trace)) * t) + (lmd_step_successor_fold_trace))) -> (((exists ff_h_lmd_fold_trace_factor. ff_h_lmd_fold_trace_factor + S (lmd_step_factor_fold_trace) = S ((S (lmd_step_index_fold_trace)) * c)) /\ exists ff_q_lmd_fold_trace_factor. b = ff_q_lmd_fold_trace_factor * S ((S (lmd_step_index_fold_trace)) * c) + (lmd_step_factor_fold_trace))) -> (exists lmd_mod_left_fold_trace_congruence lmd_mod_right_fold_trace_congruence. (lmd_step_source_fold_trace) + (p) * lmd_mod_left_fold_trace_congruence = (lmd_step_successor_fold_trace * lmd_step_factor_fold_trace) + (p) * lmd_mod_right_fold_trace_congruence)) -> (exists lmd_mod_left_fold_result lmd_mod_right_fold_result. (n) + (p) * lmd_mod_left_fold_result = (k * P) + (p) * lmd_mod_right_fold_result)

Proof neighborhood

Direct theorem prerequisites

beta_product_zero · Stable closed beta_at_unique · Stable closed mul_one · Stable closed mod_eq_refl · Stable closed beta_product_succ_decompose · Stable closed beta_at_exists · Stable closed lt_of_lt_of_le · Stable closed le_succ_self · Stable closed zero_add · Stable closed mod_eq_mul_right · Stable closed mod_eq_trans · Stable closed mul_assoc · Stable closed mul_comm · Stable closed

Direct theorem dependents

LU001I lucas_multidigit_congruence_from_one_step

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

143 script commands · 24 reading checkpoints · 11 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–1

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

  1. L1
    intro l
02Induction on lL2–11

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction l
  2. L3
    intro p
  3. L4
    intro b
  4. L5
    intro c
  5. L6
    intro z
  6. L7
    intro t
  7. L8
    intro n
  8. L9
    intro k
  9. L10
    intro P
  10. L11
    intro hproduct
03Fix variables and assumptionsL12–14

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

  1. L12
    intro hstart
  2. L13
    intro hterminal
  3. L14
    intro htrace
04Establish honeL15–20

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

  1. L15
    have hone : P = 1
  2. L16
    specialize beta_product_zero b
  3. L17
    specialize beta_product_zero c
  4. L18
    specialize beta_product_zero P
  5. L19
    apply beta_product_zero
  6. L20
    exact hproduct
05Establish hequalL21–29

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

  1. L21
    have hequal : n = k
  2. L22
    specialize beta_at_unique z
  3. L23
    specialize beta_at_unique t
  4. L24
    specialize beta_at_unique 0
  5. L25
    specialize beta_at_unique n
  6. L26
    specialize beta_at_unique k
  7. L27
    apply beta_at_unique
  8. L28
    exact hstart
  9. L29
    exact hterminal
06Establish hrightL30–39

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

  1. L30
    have hright : k * P = n
  2. L31
    rewrite hone
  3. L32
    trans k
  4. L33
    apply mul_one
  5. L34
    symm
  6. L35
    exact hequal
  7. L36
    rewrite hright
  8. L37
    specialize mod_eq_refl p
  9. L38
    specialize mod_eq_refl n
  10. L39
    exact mod_eq_refl
07Fix variables and assumptionsL40–49

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

  1. L40
    intro p
  2. L41
    intro b
  3. L42
    intro c
  4. L43
    intro z
  5. L44
    intro t
  6. L45
    intro n
  7. L46
    intro k
  8. L47
    intro P
  9. L48
    intro hproduct
  10. L49
    intro hstart
08Fix variables and assumptionsL50–51

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

  1. L50
    intro hterminal
  2. L51
    intro htrace
09Establish hdecompositionL52–58

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

  1. L52
    have hdecomposition : ∃ D. ∃ R. BetaAt(b,c,l,D) ∧ (Product(b,c,l,R) ∧ P = R · D)Definitions: BetaAt(b,c,l,D)Product(b,c,l,R)Original native command in the exact edition
  2. L53
    specialize beta_product_succ_decompose b
  3. L54
    specialize beta_product_succ_decompose c
  4. L55
    specialize beta_product_succ_decompose l
  5. L56
    specialize beta_product_succ_decompose P
  6. L57
    apply beta_product_succ_decompose
  7. L58
    exact hproduct
10Separate the logical casesL59–62

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

  1. L59
    cases hdecomposition
  2. L60
    cases hdecomposition_witness
  3. L61
    cases hdecomposition_witness_witness
  4. L62
    cases hdecomposition_witness_witness_right
11Establish hmiddleL63–67

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

  1. L63
    have hmiddle : ∃ q. BetaAt(z,t,l,q)Definitions: BetaAt(z,t,l,q)Original native command in the exact edition
  2. L64
    specialize beta_at_exists z
  3. L65
    specialize beta_at_exists t
  4. L66
    specialize beta_at_exists l
  5. L67
    exact beta_at_exists
12Separate the logical casesL68–68

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

  1. L68
    cases hmiddle
13Establish hrestrictedL69–78

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

  1. L69
    have hrestricted : ∀ lmd_step_index_fold_restricted. ∀ lmd_step_source_fold_restricted. ∀ lmd_step_successor_fold_restricted. ∀ lmd_step_factor_fold_restricted. Lt(lmd_step_index_fold_restricted,l) → BetaAt(z,t,lmd_step_index_fold_restricted,lmd_step_source_fold_restricted) → BetaAt(z,t,S lmd_step_index_fold_restricted,lmd_step_successor_fold_restricted) → BetaAt(b,c,lmd_step_index_fold_restricted,lmd_step_factor_fold_restricted) → ModEq(p,lmd_step_source_fold_restricted,lmd_step_successor_fold_restricted · lmd_step_factor_fold_restricted)Definitions: Lt(lmd_step_index_fold_restricted,l)BetaAt(z,t,lmd_step_index_fold_restricted,lmd_step_source_fold_restricted)BetaAt(z,t,S lmd_step_index_fold_restricted,lmd_step_successor_fold_restricted)BetaAt(b,c,lmd_step_index_fold_restricted,lmd_step_factor_fold_restricted)ModEq(p,lmd_step_source_fold_restricted,lmd_step_successor_fold_restricted · lmd_step_factor_fold_restricted)Original native command in the exact edition
  2. L70
    intro i
  3. L71
    intro A
  4. L72
    intro K
  5. L73
    intro D
  6. L74
    intro hi
  7. L75
    intro hA
  8. L76
    intro hK
  9. L77
    intro hD
  10. L78
    specialize htrace i
14Use earlier factsL79–88

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

  1. L79
    specialize htrace A
  2. L80
    specialize htrace K
  3. L81
    specialize htrace D
  4. L82
    apply htrace
  5. L83
    specialize lt_of_lt_of_le i
  6. L84
    specialize lt_of_lt_of_le l
  7. L85
    specialize lt_of_lt_of_le (S l)
  8. L86
    apply lt_of_lt_of_le
  9. L87
    exact hi
  10. L88
    specialize le_succ_self l
15Use earlier factsL89–92

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

  1. L89
    exact le_succ_self
  2. L90
    exact hA
  3. L91
    exact hK
  4. L92
    exact hD
16Establish hbeforeL93–102

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

  1. L93
    have hbefore : ModEq(p,n,x2 · x1)Definitions: ModEq(p,n,x2 · x1)Original native command in the exact edition
  2. L94
    specialize IH p
  3. L95
    specialize IH b
  4. L96
    specialize IH c
  5. L97
    specialize IH z
  6. L98
    specialize IH t
  7. L99
    specialize IH n
  8. L100
    specialize IH x2
  9. L101
    specialize IH x1
  10. L102
    apply IH
17Use earlier factsL103–106

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

  1. L103
    exact hdecomposition_witness_witness_right_left
  2. L104
    exact hstart
  3. L105
    exact hmiddle_witness
  4. L106
    exact hrestricted
18Establish hlastL107–112

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

  1. L107
    have hlast : ModEq(p,x2,k · x)Definitions: ModEq(p,x2,k · x)Original native command in the exact edition
  2. L108
    specialize htrace l
  3. L109
    specialize htrace x2
  4. L110
    specialize htrace k
  5. L111
    specialize htrace x
  6. L112
    apply htrace
19Construct an explicit witnessL113–113

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

  1. L113
    exists 0
20Use earlier factsL114–117

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

  1. L114
    apply zero_add
  2. L115
    exact hmiddle_witness
  3. L116
    exact hterminal
  4. L117
    exact hdecomposition_witness_witness_left
21Establish hscaledL118–124

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

  1. L118
    have hscaled : ModEq(p,x2 · x1,k · x · x1)Definitions: ModEq(p,x2 · x1,k · x · x1)Original native command in the exact edition
  2. L119
    specialize mod_eq_mul_right p
  3. L120
    specialize mod_eq_mul_right x2
  4. L121
    specialize mod_eq_mul_right (k * x)
  5. L122
    specialize mod_eq_mul_right x1
  6. L123
    apply mod_eq_mul_right
  7. L124
    exact hlast
22Establish hcombinedL125–132

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

  1. L125
    have hcombined : ModEq(p,n,k · x · x1)Definitions: ModEq(p,n,k · x · x1)Original native command in the exact edition
  2. L126
    specialize mod_eq_trans p
  3. L127
    specialize mod_eq_trans n
  4. L128
    specialize mod_eq_trans (x2 * x1)
  5. L129
    specialize mod_eq_trans ((k * x) * x1)
  6. L130
    apply mod_eq_trans
  7. L131
    exact hbefore
  8. L132
    exact hscaled
23Establish htargetL133–142

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

  1. L133
    have htarget : (k * x) * x1 = k * P
  2. L134
    trans k * (x * x1)
  3. L135
    apply mul_assoc
  4. L136
    trans k * (x1 * x)
  5. L137
    congr
  6. L138
    refl
  7. L139
    apply mul_comm
  8. L140
    rewrite hdecomposition_witness_witness_right_right
  9. L141
    refl
  10. L142
    rewrite <- htarget
24Use earlier factsL143–143

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

  1. L143
    exact hcombined

Library-wide reading audit

Original defined command ledger · 143 lines
  1. 0001intro l
  2. 0002induction l
  3. 0003intro p
  4. 0004intro b
  5. 0005intro c
  6. 0006intro z
  7. 0007intro t
  8. 0008intro n
  9. 0009intro k
  10. 0010intro P
  11. 0011intro hproduct
  12. 0012intro hstart
  13. 0013intro hterminal
  14. 0014intro htrace
  15. 0015have hone : P = 1
  16. 0016specialize beta_product_zero b
  17. 0017specialize beta_product_zero c
  18. 0018specialize beta_product_zero P
  19. 0019apply beta_product_zero
  20. 0020exact hproduct
  21. 0021have hequal : n = k
  22. 0022specialize beta_at_unique z
  23. 0023specialize beta_at_unique t
  24. 0024specialize beta_at_unique 0
  25. 0025specialize beta_at_unique n
  26. 0026specialize beta_at_unique k
  27. 0027apply beta_at_unique
  28. 0028exact hstart
  29. 0029exact hterminal
  30. 0030have hright : k * P = n
  31. 0031rewrite hone
  32. 0032trans k
  33. 0033apply mul_one
  34. 0034symm
  35. 0035exact hequal
  36. 0036rewrite hright
  37. 0037specialize mod_eq_refl p
  38. 0038specialize mod_eq_refl n
  39. 0039exact mod_eq_refl
  40. 0040intro p
  41. 0041intro b
  42. 0042intro c
  43. 0043intro z
  44. 0044intro t
  45. 0045intro n
  46. 0046intro k
  47. 0047intro P
  48. 0048intro hproduct
  49. 0049intro hstart
  50. 0050intro hterminal
  51. 0051intro htrace
  52. 0052have hdecomposition : ∃ D. ∃ R. BetaAt(b,c,l,D) ∧ (Product(b,c,l,R) ∧ P = R · D)
    Exact native replay linehave hdecomposition : exists D R. ((((exists ff_h_lmd_fold_last_factor. ff_h_lmd_fold_last_factor + S (D) = S ((S (l)) * c)) /\ exists ff_q_lmd_fold_last_factor. b = ff_q_lmd_fold_last_factor * S ((S (l)) * c) + (D))) /\ ((exists ff_u_lmd_fold_previous ff_v_lmd_fold_previous. ((((exists ff_h_lmd_fold_previous_start. ff_h_lmd_fold_previous_start + S (1) = S ((S (0)) * ff_v_lmd_fold_previous)) /\ exists ff_q_lmd_fold_previous_start. ff_u_lmd_fold_previous = ff_q_lmd_fold_previous_start * S ((S (0)) * ff_v_lmd_fold_previous) + (1))) /\ ((((exists ff_h_lmd_fold_previous_terminal. ff_h_lmd_fold_previous_terminal + S (R) = S ((S (l)) * ff_v_lmd_fold_previous)) /\ exists ff_q_lmd_fold_previous_terminal. ff_u_lmd_fold_previous = ff_q_lmd_fold_previous_terminal * S ((S (l)) * ff_v_lmd_fold_previous) + (R))) /\ forall ff_i_lmd_fold_previous. (exists ff_lt_lmd_fold_previous_bound. ff_lt_lmd_fold_previous_bound + S ff_i_lmd_fold_previous = l) -> exists ff_p_lmd_fold_previous ff_r_lmd_fold_previous ff_s_lmd_fold_previous. ((((exists ff_h_lmd_fold_previous_factor. ff_h_lmd_fold_previous_factor + S (ff_p_lmd_fold_previous) = S ((S (ff_i_lmd_fold_previous)) * c)) /\ exists ff_q_lmd_fold_previous_factor. b = ff_q_lmd_fold_previous_factor * S ((S (ff_i_lmd_fold_previous)) * c) + (ff_p_lmd_fold_previous))) /\ ((((exists ff_h_lmd_fold_previous_partial. ff_h_lmd_fold_previous_partial + S (ff_r_lmd_fold_previous) = S ((S (ff_i_lmd_fold_previous)) * ff_v_lmd_fold_previous)) /\ exists ff_q_lmd_fold_previous_partial. ff_u_lmd_fold_previous = ff_q_lmd_fold_previous_partial * S ((S (ff_i_lmd_fold_previous)) * ff_v_lmd_fold_previous) + (ff_r_lmd_fold_previous))) /\ ((((exists ff_h_lmd_fold_previous_successor. ff_h_lmd_fold_previous_successor + S (ff_s_lmd_fold_previous) = S ((S (S ff_i_lmd_fold_previous)) * ff_v_lmd_fold_previous)) /\ exists ff_q_lmd_fold_previous_successor. ff_u_lmd_fold_previous = ff_q_lmd_fold_previous_successor * S ((S (S ff_i_lmd_fold_previous)) * ff_v_lmd_fold_previous) + (ff_s_lmd_fold_previous))) /\ ff_s_lmd_fold_previous = ff_r_lmd_fold_previous * ff_p_lmd_fold_previous)))))) /\ P = R * D))
  53. 0053specialize beta_product_succ_decompose b
  54. 0054specialize beta_product_succ_decompose c
  55. 0055specialize beta_product_succ_decompose l
  56. 0056specialize beta_product_succ_decompose P
  57. 0057apply beta_product_succ_decompose
  58. 0058exact hproduct
  59. 0059cases hdecomposition
  60. 0060cases hdecomposition_witness
  61. 0061cases hdecomposition_witness_witness
  62. 0062cases hdecomposition_witness_witness_right
  63. 0063have hmiddle : ∃ q. BetaAt(z,t,l,q)
    Exact native replay linehave hmiddle : exists q. (((exists ff_h_lmd_fold_middle. ff_h_lmd_fold_middle + S (q) = S ((S (l)) * t)) /\ exists ff_q_lmd_fold_middle. z = ff_q_lmd_fold_middle * S ((S (l)) * t) + (q)))
  64. 0064specialize beta_at_exists z
  65. 0065specialize beta_at_exists t
  66. 0066specialize beta_at_exists l
  67. 0067exact beta_at_exists
  68. 0068cases hmiddle
  69. 0069have hrestricted : ∀ lmd_step_index_fold_restricted. ∀ lmd_step_source_fold_restricted. ∀ lmd_step_successor_fold_restricted. ∀ lmd_step_factor_fold_restricted. Lt(lmd_step_index_fold_restricted,l) → BetaAt(z,t,lmd_step_index_fold_restricted,lmd_step_source_fold_restricted) → BetaAt(z,t,S lmd_step_index_fold_restricted,lmd_step_successor_fold_restricted) → BetaAt(b,c,lmd_step_index_fold_restricted,lmd_step_factor_fold_restricted) → ModEq(p,lmd_step_source_fold_restricted,lmd_step_successor_fold_restricted · lmd_step_factor_fold_restricted)
    Exact native replay linehave hrestricted : forall lmd_step_index_fold_restricted lmd_step_source_fold_restricted lmd_step_successor_fold_restricted lmd_step_factor_fold_restricted. (exists lmd_gap_fold_restricted_bound. lmd_gap_fold_restricted_bound + S (lmd_step_index_fold_restricted) = (l)) -> (((exists ff_h_lmd_fold_restricted_source. ff_h_lmd_fold_restricted_source + S (lmd_step_source_fold_restricted) = S ((S (lmd_step_index_fold_restricted)) * t)) /\ exists ff_q_lmd_fold_restricted_source. z = ff_q_lmd_fold_restricted_source * S ((S (lmd_step_index_fold_restricted)) * t) + (lmd_step_source_fold_restricted))) -> (((exists ff_h_lmd_fold_restricted_successor. ff_h_lmd_fold_restricted_successor + S (lmd_step_successor_fold_restricted) = S ((S (S lmd_step_index_fold_restricted)) * t)) /\ exists ff_q_lmd_fold_restricted_successor. z = ff_q_lmd_fold_restricted_successor * S ((S (S lmd_step_index_fold_restricted)) * t) + (lmd_step_successor_fold_restricted))) -> (((exists ff_h_lmd_fold_restricted_factor. ff_h_lmd_fold_restricted_factor + S (lmd_step_factor_fold_restricted) = S ((S (lmd_step_index_fold_restricted)) * c)) /\ exists ff_q_lmd_fold_restricted_factor. b = ff_q_lmd_fold_restricted_factor * S ((S (lmd_step_index_fold_restricted)) * c) + (lmd_step_factor_fold_restricted))) -> (exists lmd_mod_left_fold_restricted_congruence lmd_mod_right_fold_restricted_congruence. (lmd_step_source_fold_restricted) + (p) * lmd_mod_left_fold_restricted_congruence = (lmd_step_successor_fold_restricted * lmd_step_factor_fold_restricted) + (p) * lmd_mod_right_fold_restricted_congruence)
  70. 0070intro i
  71. 0071intro A
  72. 0072intro K
  73. 0073intro D
  74. 0074intro hi
  75. 0075intro hA
  76. 0076intro hK
  77. 0077intro hD
  78. 0078specialize htrace i
  79. 0079specialize htrace A
  80. 0080specialize htrace K
  81. 0081specialize htrace D
  82. 0082apply htrace
  83. 0083specialize lt_of_lt_of_le i
  84. 0084specialize lt_of_lt_of_le l
  85. 0085specialize lt_of_lt_of_le (S l)
  86. 0086apply lt_of_lt_of_le
  87. 0087exact hi
  88. 0088specialize le_succ_self l
  89. 0089exact le_succ_self
  90. 0090exact hA
  91. 0091exact hK
  92. 0092exact hD
  93. 0093have hbefore : ModEq(p,n,x2 · x1)
    Exact native replay linehave hbefore : (exists lmd_mod_left_fold_before lmd_mod_right_fold_before. (n) + (p) * lmd_mod_left_fold_before = (x2 * x1) + (p) * lmd_mod_right_fold_before)
  94. 0094specialize IH p
  95. 0095specialize IH b
  96. 0096specialize IH c
  97. 0097specialize IH z
  98. 0098specialize IH t
  99. 0099specialize IH n
  100. 0100specialize IH x2
  101. 0101specialize IH x1
  102. 0102apply IH
  103. 0103exact hdecomposition_witness_witness_right_left
  104. 0104exact hstart
  105. 0105exact hmiddle_witness
  106. 0106exact hrestricted
  107. 0107have hlast : ModEq(p,x2,k · x)
    Exact native replay linehave hlast : (exists lmd_mod_left_fold_last lmd_mod_right_fold_last. (x2) + (p) * lmd_mod_left_fold_last = (k * x) + (p) * lmd_mod_right_fold_last)
  108. 0108specialize htrace l
  109. 0109specialize htrace x2
  110. 0110specialize htrace k
  111. 0111specialize htrace x
  112. 0112apply htrace
  113. 0113exists 0
  114. 0114apply zero_add
  115. 0115exact hmiddle_witness
  116. 0116exact hterminal
  117. 0117exact hdecomposition_witness_witness_left
  118. 0118have hscaled : ModEq(p,x2 · x1,k · x · x1)
    Exact native replay linehave hscaled : (exists lmd_mod_left_fold_scaled lmd_mod_right_fold_scaled. (x2 * x1) + (p) * lmd_mod_left_fold_scaled = ((k * x) * x1) + (p) * lmd_mod_right_fold_scaled)
  119. 0119specialize mod_eq_mul_right p
  120. 0120specialize mod_eq_mul_right x2
  121. 0121specialize mod_eq_mul_right (k * x)
  122. 0122specialize mod_eq_mul_right x1
  123. 0123apply mod_eq_mul_right
  124. 0124exact hlast
  125. 0125have hcombined : ModEq(p,n,k · x · x1)
    Exact native replay linehave hcombined : (exists lmd_mod_left_fold_combined lmd_mod_right_fold_combined. (n) + (p) * lmd_mod_left_fold_combined = ((k * x) * x1) + (p) * lmd_mod_right_fold_combined)
  126. 0126specialize mod_eq_trans p
  127. 0127specialize mod_eq_trans n
  128. 0128specialize mod_eq_trans (x2 * x1)
  129. 0129specialize mod_eq_trans ((k * x) * x1)
  130. 0130apply mod_eq_trans
  131. 0131exact hbefore
  132. 0132exact hscaled
  133. 0133have htarget : (k * x) * x1 = k * P
  134. 0134trans k * (x * x1)
  135. 0135apply mul_assoc
  136. 0136trans k * (x1 * x)
  137. 0137congr
  138. 0138refl
  139. 0139apply mul_comm
  140. 0140rewrite hdecomposition_witness_witness_right_right
  141. 0141refl
  142. 0142rewrite <- htarget
  143. 0143exact hcombined