CD000B

finite_sum_pointwise_strict_at

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A genuine strict pointwise witness makes otherwise monotone finite sums strictly ordered.

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.

Exact expanded first-order arithmetic statement

forall b c d e l n m i a v. (forall fms_i_le fms_a_le fms_v_le. (exists fms_gap_le. fms_gap_le + S (fms_i_le) = (l)) -> (((exists fs_h_fms_le_left. fs_h_fms_le_left + S (fms_a_le) = S ((S (fms_i_le)) * c)) /\ exists fs_q_fms_le_left. b = fs_q_fms_le_left * S ((S (fms_i_le)) * c) + (fms_a_le))) -> (((exists fs_h_fms_le_right. fs_h_fms_le_right + S (fms_v_le) = S ((S (fms_i_le)) * e)) /\ exists fs_q_fms_le_right. d = fs_q_fms_le_right * S ((S (fms_i_le)) * e) + (fms_v_le))) -> (exists fms_gap_le. fms_gap_le + (fms_a_le) = (fms_v_le))) -> (exists ff_u_fms_sum ff_v_fms_sum. ((((exists ff_h_fms_sum_start. ff_h_fms_sum_start + S (0) = S ((S (0)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_start. ff_u_fms_sum = ff_q_fms_sum_start * S ((S (0)) * ff_v_fms_sum) + (0))) /\ ((((exists ff_h_fms_sum_terminal. ff_h_fms_sum_terminal + S ((n)) = S ((S ((l))) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_terminal. ff_u_fms_sum = ff_q_fms_sum_terminal * S ((S ((l))) * ff_v_fms_sum) + ((n)))) /\ forall ff_i_fms_sum. (exists ff_lt_fms_sum_bound. ff_lt_fms_sum_bound + S ff_i_fms_sum = (l)) -> exists ff_a_fms_sum ff_r_fms_sum ff_s_fms_sum. ((((exists ff_h_fms_sum_summand. ff_h_fms_sum_summand + S (ff_a_fms_sum) = S ((S (ff_i_fms_sum)) * (c))) /\ exists ff_q_fms_sum_summand. (b) = ff_q_fms_sum_summand * S ((S (ff_i_fms_sum)) * (c)) + (ff_a_fms_sum))) /\ ((((exists ff_h_fms_sum_partial. ff_h_fms_sum_partial + S (ff_r_fms_sum) = S ((S (ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_partial. ff_u_fms_sum = ff_q_fms_sum_partial * S ((S (ff_i_fms_sum)) * ff_v_fms_sum) + (ff_r_fms_sum))) /\ ((((exists ff_h_fms_sum_successor. ff_h_fms_sum_successor + S (ff_s_fms_sum) = S ((S (S ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_successor. ff_u_fms_sum = ff_q_fms_sum_successor * S ((S (S ff_i_fms_sum)) * ff_v_fms_sum) + (ff_s_fms_sum))) /\ ff_s_fms_sum = ff_r_fms_sum + ff_a_fms_sum)))))) -> (exists ff_u_fms_sum ff_v_fms_sum. ((((exists ff_h_fms_sum_start. ff_h_fms_sum_start + S (0) = S ((S (0)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_start. ff_u_fms_sum = ff_q_fms_sum_start * S ((S (0)) * ff_v_fms_sum) + (0))) /\ ((((exists ff_h_fms_sum_terminal. ff_h_fms_sum_terminal + S ((m)) = S ((S ((l))) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_terminal. ff_u_fms_sum = ff_q_fms_sum_terminal * S ((S ((l))) * ff_v_fms_sum) + ((m)))) /\ forall ff_i_fms_sum. (exists ff_lt_fms_sum_bound. ff_lt_fms_sum_bound + S ff_i_fms_sum = (l)) -> exists ff_a_fms_sum ff_r_fms_sum ff_s_fms_sum. ((((exists ff_h_fms_sum_summand. ff_h_fms_sum_summand + S (ff_a_fms_sum) = S ((S (ff_i_fms_sum)) * (e))) /\ exists ff_q_fms_sum_summand. (d) = ff_q_fms_sum_summand * S ((S (ff_i_fms_sum)) * (e)) + (ff_a_fms_sum))) /\ ((((exists ff_h_fms_sum_partial. ff_h_fms_sum_partial + S (ff_r_fms_sum) = S ((S (ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_partial. ff_u_fms_sum = ff_q_fms_sum_partial * S ((S (ff_i_fms_sum)) * ff_v_fms_sum) + (ff_r_fms_sum))) /\ ((((exists ff_h_fms_sum_successor. ff_h_fms_sum_successor + S (ff_s_fms_sum) = S ((S (S ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_successor. ff_u_fms_sum = ff_q_fms_sum_successor * S ((S (S ff_i_fms_sum)) * ff_v_fms_sum) + (ff_s_fms_sum))) /\ ff_s_fms_sum = ff_r_fms_sum + ff_a_fms_sum)))))) -> (exists fms_gap_lt. fms_gap_lt + S (i) = (l)) -> (((exists fs_h_fms_strict_left. fs_h_fms_strict_left + S (a) = S ((S (i)) * c)) /\ exists fs_q_fms_strict_left. b = fs_q_fms_strict_left * S ((S (i)) * c) + (a))) -> (((exists fs_h_fms_strict_right. fs_h_fms_strict_right + S (v) = S ((S (i)) * e)) /\ exists fs_q_fms_strict_right. d = fs_q_fms_strict_right * S ((S (i)) * e) + (v))) -> (exists fms_gap_lt. fms_gap_lt + S (a) = (v)) -> (exists fms_gap_lt. fms_gap_lt + S (n) = (m))

Constructive proof overview

Generated structural guide

A genuine strict pointwise witness makes otherwise monotone finite sums strictly ordered.

The unchanged tactic script uses 10 declared prerequisites and contains 157 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_sum_succ_decompose Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized beta_sum_pointwise_le Alpha theorem; checked-use authorized le_succ Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized CD0007 finite_add_lt_of_lt_of_le CD0008 finite_add_lt_of_le_of_lt add_eq_zero_right Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

CD000C finite_bit_count_proper_subset_lt

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

157 script commands · 24 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.

Named ingredients (2)
finite add lt of lt of lefinite add lt of le of lt

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
02Induction on lL5–14

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

  1. L5
    induction l
  2. L6
    intro n
  3. L7
    intro m
  4. L8
    intro i
  5. L9
    intro a
  6. L10
    intro v
  7. L11
    intro hpoint
  8. L12
    intro hn
  9. L13
    intro hm
  10. L14
    intro hi
03Fix variables and assumptionsL15–17

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

  1. L15
    intro ha
  2. L16
    intro hv
  3. L17
    intro hav
04Separate the logical casesL18–19

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

  1. L18
    exfalso
  2. L19
    cases hi
05Establish hzL20–29

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

  1. L20
    have hz : S i=0
  2. L21
    specialize add_eq_zero_right x
  3. L22
    specialize add_eq_zero_right S i
  4. L23
    apply add_eq_zero_right
  5. L24
    exact hi_witness
  6. L25
    specialize succ_ne_zero i
  7. L26
    apply succ_ne_zero
  8. L27
    exact hz
  9. L28
    intro n
  10. L29
    intro m
06Fix variables and assumptionsL30–39

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

  1. L30
    intro i
  2. L31
    intro a
  3. L32
    intro v
  4. L33
    intro hpoint
  5. L34
    intro hn
  6. L35
    intro hm
  7. L36
    intro hi
  8. L37
    intro ha
  9. L38
    intro hv
  10. L39
    intro hav
07Establish hdAL40–46

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

  1. L40
    have hdA : ∃ fms_term_hdA. ∃ fms_sum_hdA. BetaAt(b,c,l,fms_term_hdA) ∧ (Sum(b,c,l,fms_sum_hdA) ∧ n = fms_sum_hdA + fms_term_hdA)Definitions: BetaAtSum
  2. L41
    specialize beta_sum_succ_decompose b
  3. L42
    specialize beta_sum_succ_decompose c
  4. L43
    specialize beta_sum_succ_decompose l
  5. L44
    specialize beta_sum_succ_decompose n
  6. L45
    apply beta_sum_succ_decompose
  7. L46
    exact hn
08Separate the logical casesL47–50

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

  1. L47
    cases hdA
  2. L48
    cases hdA_witness
  3. L49
    cases hdA_witness_witness
  4. L50
    cases hdA_witness_witness_right
09Establish hdBL51–57

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

  1. L51
    have hdB : ∃ fms_term_hdB. ∃ fms_sum_hdB. BetaAt(d,e,l,fms_term_hdB) ∧ (Sum(d,e,l,fms_sum_hdB) ∧ m = fms_sum_hdB + fms_term_hdB)Definitions: BetaAtSum
  2. L52
    specialize beta_sum_succ_decompose d
  3. L53
    specialize beta_sum_succ_decompose e
  4. L54
    specialize beta_sum_succ_decompose l
  5. L55
    specialize beta_sum_succ_decompose m
  6. L56
    apply beta_sum_succ_decompose
  7. L57
    exact hm
10Separate the logical casesL58–61

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

  1. L58
    cases hdB
  2. L59
    cases hdB_witness
  3. L60
    cases hdB_witness_witness
  4. L61
    cases hdB_witness_witness_right
11Establish hprefixL62–71

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

  1. L62
    have hprefix : forall fms_i_le fms_a_le fms_v_le. (exists fms_gap_le. fms_gap_le + S (fms_i_le) = (l)) -> (((exists fs_h_fms_le_left. fs_h_fms_le_left + S (fms_a_le) = S ((S (fms_i_le)) * c)) /\ exists fs_q_fms_le_left. b = fs_q_fms_le_left * S ((S (fms_i_le)) * c) + (fms_a_le))) -> (((exists fs_h_fms_le_right. fs_h_fms_le_right + S (fms_v_le) = S ((S (fms_i_le)) * e)) /\ exists fs_q_fms_le_right. d = fs_q_fms_le_right * S ((S (fms_i_le)) * e) + (fms_v_le))) -> (exists fms_gap_le. fms_gap_le + (fms_a_le) = (fms_v_le))
  2. L63
    intro j
  3. L64
    intro A
  4. L65
    intro B
  5. L66
    intro hj
  6. L67
    intro hA
  7. L68
    intro hB
  8. L69
    specialize hpoint j
  9. L70
    specialize hpoint A
  10. L71
    specialize hpoint B
12Use earlier factsL72–78

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

  1. L72
    apply hpoint
  2. L73
    specialize le_succ S j
  3. L74
    specialize le_succ l
  4. L75
    apply le_succ
  5. L76
    exact hj
  6. L77
    exact hA
  7. L78
    exact hB
13Establish hlastL79–87

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

  1. L79
    have hlast : exists fms_gap_le. fms_gap_le + (x) = (x2)
  2. L80
    specialize hpoint l
  3. L81
    specialize hpoint x
  4. L82
    specialize hpoint x2
  5. L83
    apply hpoint
  6. L84
    specialize le_refl S l
  7. L85
    apply le_refl
  8. L86
    exact hdA_witness_witness_left
  9. L87
    exact hdB_witness_witness_left
14Establish hcaseL88–92

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. L88
    have hcase : i=l \/ (exists fms_gap_lt. fms_gap_lt + S (i) = (l))
  2. L89
    specialize finite_lt_succ_eq_or_lt l
  3. L90
    specialize finite_lt_succ_eq_or_lt i
  4. L91
    apply finite_lt_succ_eq_or_lt
  5. L92
    exact hi
15Separate the logical casesL93–93

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

  1. L93
    cases hcase
16Calculate and transport equalitiesL94–97

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

  1. L94
    rewrite hcase_left at ha
  2. L95
    rewrite hcase_left at ha
  3. L96
    rewrite hcase_left at hv
  4. L97
    rewrite hcase_left at hv
17Establish heAL98–106

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

  1. L98
    have heA : a=x
  2. L99
    specialize beta_at_unique b
  3. L100
    specialize beta_at_unique c
  4. L101
    specialize beta_at_unique l
  5. L102
    specialize beta_at_unique a
  6. L103
    specialize beta_at_unique x
  7. L104
    apply beta_at_unique
  8. L105
    exact ha
  9. L106
    exact hdA_witness_witness_left
18Establish heBL107–116

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

  1. L107
    have heB : v=x2
  2. L108
    specialize beta_at_unique d
  3. L109
    specialize beta_at_unique e
  4. L110
    specialize beta_at_unique l
  5. L111
    specialize beta_at_unique v
  6. L112
    specialize beta_at_unique x2
  7. L113
    apply beta_at_unique
  8. L114
    exact hv
  9. L115
    exact hdB_witness_witness_left
  10. L116
    rewrite heA at hav
19Calculate and transport equalitiesL117–119

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

  1. L117
    rewrite heB at hav
  2. L118
    rewrite hdA_witness_witness_right_right
  3. L119
    rewrite hdB_witness_witness_right_right
20Use earlier factsL120–129

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

  1. L120
    specialize finite_add_lt_of_le_of_lt x1
  2. L121
    specialize finite_add_lt_of_le_of_lt x3
  3. L122
    specialize finite_add_lt_of_le_of_lt x
  4. L123
    specialize finite_add_lt_of_le_of_lt x2
  5. L124
    apply finite_add_lt_of_le_of_lt
  6. L125
    specialize beta_sum_pointwise_le b
  7. L126
    specialize beta_sum_pointwise_le c
  8. L127
    specialize beta_sum_pointwise_le d
  9. L128
    specialize beta_sum_pointwise_le e
  10. L129
    specialize beta_sum_pointwise_le l
21Use earlier factsL130–136

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

  1. L130
    specialize beta_sum_pointwise_le x1
  2. L131
    specialize beta_sum_pointwise_le x3
  3. L132
    apply beta_sum_pointwise_le
  4. L133
    exact hprefix
  5. L134
    exact hdA_witness_witness_right_left
  6. L135
    exact hdB_witness_witness_right_left
  7. L136
    exact hav
22Calculate and transport equalitiesL137–138

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

  1. L137
    rewrite hdA_witness_witness_right_right
  2. L138
    rewrite hdB_witness_witness_right_right
23Use earlier factsL139–148

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

  1. L139
    specialize finite_add_lt_of_lt_of_le x1
  2. L140
    specialize finite_add_lt_of_lt_of_le x3
  3. L141
    specialize finite_add_lt_of_lt_of_le x
  4. L142
    specialize finite_add_lt_of_lt_of_le x2
  5. L143
    apply finite_add_lt_of_lt_of_le
  6. L144
    specialize IH x1
  7. L145
    specialize IH x3
  8. L146
    specialize IH i
  9. L147
    specialize IH a
  10. L148
    specialize IH v
24Use earlier factsL149–157

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

  1. L149
    apply IH
  2. L150
    exact hprefix
  3. L151
    exact hdA_witness_witness_right_left
  4. L152
    exact hdB_witness_witness_right_left
  5. L153
    exact hcase_right
  6. L154
    exact ha
  7. L155
    exact hv
  8. L156
    exact hav
  9. L157
    exact hlast

Library-wide reading audit

Original exact command ledger · 157 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005induction l
  6. 0006intro n
  7. 0007intro m
  8. 0008intro i
  9. 0009intro a
  10. 0010intro v
  11. 0011intro hpoint
  12. 0012intro hn
  13. 0013intro hm
  14. 0014intro hi
  15. 0015intro ha
  16. 0016intro hv
  17. 0017intro hav
  18. 0018exfalso
  19. 0019cases hi
  20. 0020have hz : S i=0
  21. 0021specialize add_eq_zero_right x
  22. 0022specialize add_eq_zero_right S i
  23. 0023apply add_eq_zero_right
  24. 0024exact hi_witness
  25. 0025specialize succ_ne_zero i
  26. 0026apply succ_ne_zero
  27. 0027exact hz
  28. 0028intro n
  29. 0029intro m
  30. 0030intro i
  31. 0031intro a
  32. 0032intro v
  33. 0033intro hpoint
  34. 0034intro hn
  35. 0035intro hm
  36. 0036intro hi
  37. 0037intro ha
  38. 0038intro hv
  39. 0039intro hav
  40. 0040have hdA : exists fms_term_hdA fms_sum_hdA. (((exists fs_h_fms_hdA. fs_h_fms_hdA + S (fms_term_hdA) = S ((S (l)) * c)) /\ exists fs_q_fms_hdA. b = fs_q_fms_hdA * S ((S (l)) * c) + (fms_term_hdA))) /\ ((exists ff_u_fms_hdA ff_v_fms_hdA. ((((exists ff_h_fms_hdA_start. ff_h_fms_hdA_start + S (0) = S ((S (0)) * ff_v_fms_hdA)) /\ exists ff_q_fms_hdA_start. ff_u_fms_hdA = ff_q_fms_hdA_start * S ((S (0)) * ff_v_fms_hdA) + (0))) /\ ((((exists ff_h_fms_hdA_terminal. ff_h_fms_hdA_terminal + S ((fms_sum_hdA)) = S ((S ((l))) * ff_v_fms_hdA)) /\ exists ff_q_fms_hdA_terminal. ff_u_fms_hdA = ff_q_fms_hdA_terminal * S ((S ((l))) * ff_v_fms_hdA) + ((fms_sum_hdA)))) /\ forall ff_i_fms_hdA. (exists ff_lt_fms_hdA_bound. ff_lt_fms_hdA_bound + S ff_i_fms_hdA = (l)) -> exists ff_a_fms_hdA ff_r_fms_hdA ff_s_fms_hdA. ((((exists ff_h_fms_hdA_summand. ff_h_fms_hdA_summand + S (ff_a_fms_hdA) = S ((S (ff_i_fms_hdA)) * (c))) /\ exists ff_q_fms_hdA_summand. (b) = ff_q_fms_hdA_summand * S ((S (ff_i_fms_hdA)) * (c)) + (ff_a_fms_hdA))) /\ ((((exists ff_h_fms_hdA_partial. ff_h_fms_hdA_partial + S (ff_r_fms_hdA) = S ((S (ff_i_fms_hdA)) * ff_v_fms_hdA)) /\ exists ff_q_fms_hdA_partial. ff_u_fms_hdA = ff_q_fms_hdA_partial * S ((S (ff_i_fms_hdA)) * ff_v_fms_hdA) + (ff_r_fms_hdA))) /\ ((((exists ff_h_fms_hdA_successor. ff_h_fms_hdA_successor + S (ff_s_fms_hdA) = S ((S (S ff_i_fms_hdA)) * ff_v_fms_hdA)) /\ exists ff_q_fms_hdA_successor. ff_u_fms_hdA = ff_q_fms_hdA_successor * S ((S (S ff_i_fms_hdA)) * ff_v_fms_hdA) + (ff_s_fms_hdA))) /\ ff_s_fms_hdA = ff_r_fms_hdA + ff_a_fms_hdA)))))) /\ n=fms_sum_hdA+fms_term_hdA)
  41. 0041specialize beta_sum_succ_decompose b
  42. 0042specialize beta_sum_succ_decompose c
  43. 0043specialize beta_sum_succ_decompose l
  44. 0044specialize beta_sum_succ_decompose n
  45. 0045apply beta_sum_succ_decompose
  46. 0046exact hn
  47. 0047cases hdA
  48. 0048cases hdA_witness
  49. 0049cases hdA_witness_witness
  50. 0050cases hdA_witness_witness_right
  51. 0051have hdB : exists fms_term_hdB fms_sum_hdB. (((exists fs_h_fms_hdB. fs_h_fms_hdB + S (fms_term_hdB) = S ((S (l)) * e)) /\ exists fs_q_fms_hdB. d = fs_q_fms_hdB * S ((S (l)) * e) + (fms_term_hdB))) /\ ((exists ff_u_fms_hdB ff_v_fms_hdB. ((((exists ff_h_fms_hdB_start. ff_h_fms_hdB_start + S (0) = S ((S (0)) * ff_v_fms_hdB)) /\ exists ff_q_fms_hdB_start. ff_u_fms_hdB = ff_q_fms_hdB_start * S ((S (0)) * ff_v_fms_hdB) + (0))) /\ ((((exists ff_h_fms_hdB_terminal. ff_h_fms_hdB_terminal + S ((fms_sum_hdB)) = S ((S ((l))) * ff_v_fms_hdB)) /\ exists ff_q_fms_hdB_terminal. ff_u_fms_hdB = ff_q_fms_hdB_terminal * S ((S ((l))) * ff_v_fms_hdB) + ((fms_sum_hdB)))) /\ forall ff_i_fms_hdB. (exists ff_lt_fms_hdB_bound. ff_lt_fms_hdB_bound + S ff_i_fms_hdB = (l)) -> exists ff_a_fms_hdB ff_r_fms_hdB ff_s_fms_hdB. ((((exists ff_h_fms_hdB_summand. ff_h_fms_hdB_summand + S (ff_a_fms_hdB) = S ((S (ff_i_fms_hdB)) * (e))) /\ exists ff_q_fms_hdB_summand. (d) = ff_q_fms_hdB_summand * S ((S (ff_i_fms_hdB)) * (e)) + (ff_a_fms_hdB))) /\ ((((exists ff_h_fms_hdB_partial. ff_h_fms_hdB_partial + S (ff_r_fms_hdB) = S ((S (ff_i_fms_hdB)) * ff_v_fms_hdB)) /\ exists ff_q_fms_hdB_partial. ff_u_fms_hdB = ff_q_fms_hdB_partial * S ((S (ff_i_fms_hdB)) * ff_v_fms_hdB) + (ff_r_fms_hdB))) /\ ((((exists ff_h_fms_hdB_successor. ff_h_fms_hdB_successor + S (ff_s_fms_hdB) = S ((S (S ff_i_fms_hdB)) * ff_v_fms_hdB)) /\ exists ff_q_fms_hdB_successor. ff_u_fms_hdB = ff_q_fms_hdB_successor * S ((S (S ff_i_fms_hdB)) * ff_v_fms_hdB) + (ff_s_fms_hdB))) /\ ff_s_fms_hdB = ff_r_fms_hdB + ff_a_fms_hdB)))))) /\ m=fms_sum_hdB+fms_term_hdB)
  52. 0052specialize beta_sum_succ_decompose d
  53. 0053specialize beta_sum_succ_decompose e
  54. 0054specialize beta_sum_succ_decompose l
  55. 0055specialize beta_sum_succ_decompose m
  56. 0056apply beta_sum_succ_decompose
  57. 0057exact hm
  58. 0058cases hdB
  59. 0059cases hdB_witness
  60. 0060cases hdB_witness_witness
  61. 0061cases hdB_witness_witness_right
  62. 0062have hprefix : forall fms_i_le fms_a_le fms_v_le. (exists fms_gap_le. fms_gap_le + S (fms_i_le) = (l)) -> (((exists fs_h_fms_le_left. fs_h_fms_le_left + S (fms_a_le) = S ((S (fms_i_le)) * c)) /\ exists fs_q_fms_le_left. b = fs_q_fms_le_left * S ((S (fms_i_le)) * c) + (fms_a_le))) -> (((exists fs_h_fms_le_right. fs_h_fms_le_right + S (fms_v_le) = S ((S (fms_i_le)) * e)) /\ exists fs_q_fms_le_right. d = fs_q_fms_le_right * S ((S (fms_i_le)) * e) + (fms_v_le))) -> (exists fms_gap_le. fms_gap_le + (fms_a_le) = (fms_v_le))
  63. 0063intro j
  64. 0064intro A
  65. 0065intro B
  66. 0066intro hj
  67. 0067intro hA
  68. 0068intro hB
  69. 0069specialize hpoint j
  70. 0070specialize hpoint A
  71. 0071specialize hpoint B
  72. 0072apply hpoint
  73. 0073specialize le_succ S j
  74. 0074specialize le_succ l
  75. 0075apply le_succ
  76. 0076exact hj
  77. 0077exact hA
  78. 0078exact hB
  79. 0079have hlast : exists fms_gap_le. fms_gap_le + (x) = (x2)
  80. 0080specialize hpoint l
  81. 0081specialize hpoint x
  82. 0082specialize hpoint x2
  83. 0083apply hpoint
  84. 0084specialize le_refl S l
  85. 0085apply le_refl
  86. 0086exact hdA_witness_witness_left
  87. 0087exact hdB_witness_witness_left
  88. 0088have hcase : i=l \/ (exists fms_gap_lt. fms_gap_lt + S (i) = (l))
  89. 0089specialize finite_lt_succ_eq_or_lt l
  90. 0090specialize finite_lt_succ_eq_or_lt i
  91. 0091apply finite_lt_succ_eq_or_lt
  92. 0092exact hi
  93. 0093cases hcase
  94. 0094rewrite hcase_left at ha
  95. 0095rewrite hcase_left at ha
  96. 0096rewrite hcase_left at hv
  97. 0097rewrite hcase_left at hv
  98. 0098have heA : a=x
  99. 0099specialize beta_at_unique b
  100. 0100specialize beta_at_unique c
  101. 0101specialize beta_at_unique l
  102. 0102specialize beta_at_unique a
  103. 0103specialize beta_at_unique x
  104. 0104apply beta_at_unique
  105. 0105exact ha
  106. 0106exact hdA_witness_witness_left
  107. 0107have heB : v=x2
  108. 0108specialize beta_at_unique d
  109. 0109specialize beta_at_unique e
  110. 0110specialize beta_at_unique l
  111. 0111specialize beta_at_unique v
  112. 0112specialize beta_at_unique x2
  113. 0113apply beta_at_unique
  114. 0114exact hv
  115. 0115exact hdB_witness_witness_left
  116. 0116rewrite heA at hav
  117. 0117rewrite heB at hav
  118. 0118rewrite hdA_witness_witness_right_right
  119. 0119rewrite hdB_witness_witness_right_right
  120. 0120specialize finite_add_lt_of_le_of_lt x1
  121. 0121specialize finite_add_lt_of_le_of_lt x3
  122. 0122specialize finite_add_lt_of_le_of_lt x
  123. 0123specialize finite_add_lt_of_le_of_lt x2
  124. 0124apply finite_add_lt_of_le_of_lt
  125. 0125specialize beta_sum_pointwise_le b
  126. 0126specialize beta_sum_pointwise_le c
  127. 0127specialize beta_sum_pointwise_le d
  128. 0128specialize beta_sum_pointwise_le e
  129. 0129specialize beta_sum_pointwise_le l
  130. 0130specialize beta_sum_pointwise_le x1
  131. 0131specialize beta_sum_pointwise_le x3
  132. 0132apply beta_sum_pointwise_le
  133. 0133exact hprefix
  134. 0134exact hdA_witness_witness_right_left
  135. 0135exact hdB_witness_witness_right_left
  136. 0136exact hav
  137. 0137rewrite hdA_witness_witness_right_right
  138. 0138rewrite hdB_witness_witness_right_right
  139. 0139specialize finite_add_lt_of_lt_of_le x1
  140. 0140specialize finite_add_lt_of_lt_of_le x3
  141. 0141specialize finite_add_lt_of_lt_of_le x
  142. 0142specialize finite_add_lt_of_lt_of_le x2
  143. 0143apply finite_add_lt_of_lt_of_le
  144. 0144specialize IH x1
  145. 0145specialize IH x3
  146. 0146specialize IH i
  147. 0147specialize IH a
  148. 0148specialize IH v
  149. 0149apply IH
  150. 0150exact hprefix
  151. 0151exact hdA_witness_witness_right_left
  152. 0152exact hdB_witness_witness_right_left
  153. 0153exact hcase_right
  154. 0154exact ha
  155. 0155exact hv
  156. 0156exact hav
  157. 0157exact hlast