BT00X9 · Bertrand theorem

beta_product_pointwise_le

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

Pointwise bounded decoded prefixes have ordered finite products.

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

∀ b. ∀ c. ∀ d. ∀ e. ∀ l. ∀ n. ∀ q. (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,z) → Le(y,z)) → Product(b,c,l,n) → Product(d,e,l,q) → Le(n,q)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0013 BetaAt PD0014 Product

7 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt PD0014 Product

11 occurrences

Exact expanded native-PA statement
forall b c d e l n q. (forall i a z. (exists bppl_bound. bppl_bound + S i = l) -> (((exists ff_h_bppl_left. ff_h_bppl_left + S (a) = S ((S (i)) * c)) /\ exists ff_q_bppl_left. b = ff_q_bppl_left * S ((S (i)) * c) + (a))) -> (((exists ff_h_bppl_right. ff_h_bppl_right + S (z) = S ((S (i)) * e)) /\ exists ff_q_bppl_right. d = ff_q_bppl_right * S ((S (i)) * e) + (z))) -> exists bppl_factor_gap. bppl_factor_gap + a = z) -> (exists ff_u_bppl_left_product ff_v_bppl_left_product. ((((exists ff_h_bppl_left_product_start. ff_h_bppl_left_product_start + S (1) = S ((S (0)) * ff_v_bppl_left_product)) /\ exists ff_q_bppl_left_product_start. ff_u_bppl_left_product = ff_q_bppl_left_product_start * S ((S (0)) * ff_v_bppl_left_product) + (1))) /\ ((((exists ff_h_bppl_left_product_terminal. ff_h_bppl_left_product_terminal + S (n) = S ((S (l)) * ff_v_bppl_left_product)) /\ exists ff_q_bppl_left_product_terminal. ff_u_bppl_left_product = ff_q_bppl_left_product_terminal * S ((S (l)) * ff_v_bppl_left_product) + (n))) /\ forall ff_i_bppl_left_product. (exists ff_lt_bppl_left_product_bound. ff_lt_bppl_left_product_bound + S ff_i_bppl_left_product = l) -> exists ff_p_bppl_left_product ff_r_bppl_left_product ff_s_bppl_left_product. ((((exists ff_h_bppl_left_product_factor. ff_h_bppl_left_product_factor + S (ff_p_bppl_left_product) = S ((S (ff_i_bppl_left_product)) * c)) /\ exists ff_q_bppl_left_product_factor. b = ff_q_bppl_left_product_factor * S ((S (ff_i_bppl_left_product)) * c) + (ff_p_bppl_left_product))) /\ ((((exists ff_h_bppl_left_product_partial. ff_h_bppl_left_product_partial + S (ff_r_bppl_left_product) = S ((S (ff_i_bppl_left_product)) * ff_v_bppl_left_product)) /\ exists ff_q_bppl_left_product_partial. ff_u_bppl_left_product = ff_q_bppl_left_product_partial * S ((S (ff_i_bppl_left_product)) * ff_v_bppl_left_product) + (ff_r_bppl_left_product))) /\ ((((exists ff_h_bppl_left_product_successor. ff_h_bppl_left_product_successor + S (ff_s_bppl_left_product) = S ((S (S ff_i_bppl_left_product)) * ff_v_bppl_left_product)) /\ exists ff_q_bppl_left_product_successor. ff_u_bppl_left_product = ff_q_bppl_left_product_successor * S ((S (S ff_i_bppl_left_product)) * ff_v_bppl_left_product) + (ff_s_bppl_left_product))) /\ ff_s_bppl_left_product = ff_r_bppl_left_product * ff_p_bppl_left_product)))))) -> (exists ff_u_bppl_right_product ff_v_bppl_right_product. ((((exists ff_h_bppl_right_product_start. ff_h_bppl_right_product_start + S (1) = S ((S (0)) * ff_v_bppl_right_product)) /\ exists ff_q_bppl_right_product_start. ff_u_bppl_right_product = ff_q_bppl_right_product_start * S ((S (0)) * ff_v_bppl_right_product) + (1))) /\ ((((exists ff_h_bppl_right_product_terminal. ff_h_bppl_right_product_terminal + S (q) = S ((S (l)) * ff_v_bppl_right_product)) /\ exists ff_q_bppl_right_product_terminal. ff_u_bppl_right_product = ff_q_bppl_right_product_terminal * S ((S (l)) * ff_v_bppl_right_product) + (q))) /\ forall ff_i_bppl_right_product. (exists ff_lt_bppl_right_product_bound. ff_lt_bppl_right_product_bound + S ff_i_bppl_right_product = l) -> exists ff_p_bppl_right_product ff_r_bppl_right_product ff_s_bppl_right_product. ((((exists ff_h_bppl_right_product_factor. ff_h_bppl_right_product_factor + S (ff_p_bppl_right_product) = S ((S (ff_i_bppl_right_product)) * e)) /\ exists ff_q_bppl_right_product_factor. d = ff_q_bppl_right_product_factor * S ((S (ff_i_bppl_right_product)) * e) + (ff_p_bppl_right_product))) /\ ((((exists ff_h_bppl_right_product_partial. ff_h_bppl_right_product_partial + S (ff_r_bppl_right_product) = S ((S (ff_i_bppl_right_product)) * ff_v_bppl_right_product)) /\ exists ff_q_bppl_right_product_partial. ff_u_bppl_right_product = ff_q_bppl_right_product_partial * S ((S (ff_i_bppl_right_product)) * ff_v_bppl_right_product) + (ff_r_bppl_right_product))) /\ ((((exists ff_h_bppl_right_product_successor. ff_h_bppl_right_product_successor + S (ff_s_bppl_right_product) = S ((S (S ff_i_bppl_right_product)) * ff_v_bppl_right_product)) /\ exists ff_q_bppl_right_product_successor. ff_u_bppl_right_product = ff_q_bppl_right_product_successor * S ((S (S ff_i_bppl_right_product)) * ff_v_bppl_right_product) + (ff_s_bppl_right_product))) /\ ff_s_bppl_right_product = ff_r_bppl_right_product * ff_p_bppl_right_product)))))) -> exists bppl_result_gap. bppl_result_gap + n = q

Proof neighborhood

Direct theorem prerequisites

BT005I beta_product_zero BT005J beta_product_succ_decompose BT0018 le_succ BT000E le_refl BT00PV mul_le_mul

Direct theorem dependents

BT00XA beta_product_uniform_le_pow BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

97 script commands · 15 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.

Named ingredients (5)
beta product zerobeta product succ decomposele succle reflmul le mul
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–10

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 q
  4. L8
    intro hpw
  5. L9
    intro hn
  6. L10
    intro hq
03Establish hn1L11–16

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

  1. L11
    have hn1 : n = 1
  2. L12
    specialize beta_product_zero b
  3. L13
    specialize beta_product_zero c
  4. L14
    specialize beta_product_zero n
  5. L15
    apply beta_product_zero
  6. L16
    exact hn
04Establish hq1L17–26

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

  1. L17
    have hq1 : q = 1
  2. L18
    specialize beta_product_zero d
  3. L19
    specialize beta_product_zero e
  4. L20
    specialize beta_product_zero q
  5. L21
    apply beta_product_zero
  6. L22
    exact hq
  7. L23
    rewrite hn1
  8. L24
    rewrite hq1
  9. L25
    specialize le_refl 1
  10. L26
    exact le_refl
05Fix variables and assumptionsL27–31

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

  1. L27
    intro n
  2. L28
    intro q
  3. L29
    intro hpw
  4. L30
    intro hn
  5. L31
    intro hq
06Establish hndL32–38

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

  1. L32
    have hnd : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ n = r · a)Definitions: BetaAt(b,c,l,a)Product(b,c,l,r)Original native command in the exact edition
  2. L33
    specialize beta_product_succ_decompose b
  3. L34
    specialize beta_product_succ_decompose c
  4. L35
    specialize beta_product_succ_decompose l
  5. L36
    specialize beta_product_succ_decompose n
  6. L37
    apply beta_product_succ_decompose
  7. L38
    exact hn
07Separate the logical casesL39–42

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

  1. L39
    cases hnd
  2. L40
    cases hnd_witness
  3. L41
    cases hnd_witness_witness
  4. L42
    cases hnd_witness_witness_right
08Establish hqdL43–49

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

  1. L43
    have hqd : ∃ a. ∃ r. BetaAt(d,e,l,a) ∧ (Product(d,e,l,r) ∧ q = r · a)Definitions: BetaAt(d,e,l,a)Product(d,e,l,r)Original native command in the exact edition
  2. L44
    specialize beta_product_succ_decompose d
  3. L45
    specialize beta_product_succ_decompose e
  4. L46
    specialize beta_product_succ_decompose l
  5. L47
    specialize beta_product_succ_decompose q
  6. L48
    apply beta_product_succ_decompose
  7. L49
    exact hq
09Separate the logical casesL50–53

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

  1. L50
    cases hqd
  2. L51
    cases hqd_witness
  3. L52
    cases hqd_witness_witness
  4. L53
    cases hqd_witness_witness_right
10Establish hpw_prefixL54–63

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

  1. L54
    have hpw_prefix : ∀ i. ∀ a. ∀ z. Lt(i,l) → BetaAt(b,c,i,a) → BetaAt(d,e,i,z) → Le(a,z)Definitions: Lt(i,l)BetaAt(b,c,i,a)BetaAt(d,e,i,z)Le(a,z)Original native command in the exact edition
  2. L55
    intro i
  3. L56
    intro a
  4. L57
    intro z
  5. L58
    intro hi
  6. L59
    intro ha
  7. L60
    intro hz
  8. L61
    specialize hpw i
  9. L62
    specialize hpw a
  10. L63
    specialize hpw z
11Use earlier factsL64–70

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

  1. L64
    apply hpw
  2. L65
    specialize le_succ (S i)
  3. L66
    specialize le_succ l
  4. L67
    apply le_succ
  5. L68
    exact hi
  6. L69
    exact ha
  7. L70
    exact hz
12Establish hprefixL71–77

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

  1. L71
    have hprefix : Le(x1,x3)Definitions: Le(x1,x3)Original native command in the exact edition
  2. L72
    specialize IH x1
  3. L73
    specialize IH x3
  4. L74
    apply IH
  5. L75
    exact hpw_prefix
  6. L76
    exact hnd_witness_witness_right_left
  7. L77
    exact hqd_witness_witness_right_left
13Establish hentryL78–86

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

  1. L78
    have hentry : Le(x,x2)Definitions: Le(x,x2)Original native command in the exact edition
  2. L79
    specialize hpw l
  3. L80
    specialize hpw x
  4. L81
    specialize hpw x2
  5. L82
    apply hpw
  6. L83
    specialize le_refl (S l)
  7. L84
    exact le_refl
  8. L85
    exact hnd_witness_witness_left
  9. L86
    exact hqd_witness_witness_left
14Establish hfoldL87–96

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

  1. L87
    have hfold : Le(x1 · x,x3 · x2)Definitions: Le(x1 · x,x3 · x2)Original native command in the exact edition
  2. L88
    specialize mul_le_mul x1
  3. L89
    specialize mul_le_mul x3
  4. L90
    specialize mul_le_mul x
  5. L91
    specialize mul_le_mul x2
  6. L92
    apply mul_le_mul
  7. L93
    exact hprefix
  8. L94
    exact hentry
  9. L95
    rewrite hnd_witness_witness_right_right
  10. L96
    rewrite hqd_witness_witness_right_right
15Use earlier factsL97–97

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

  1. L97
    exact hfold

Library-wide reading audit

Original defined command ledger · 97 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005induction l
  6. 0006intro n
  7. 0007intro q
  8. 0008intro hpw
  9. 0009intro hn
  10. 0010intro hq
  11. 0011have hn1 : n = 1
  12. 0012specialize beta_product_zero b
  13. 0013specialize beta_product_zero c
  14. 0014specialize beta_product_zero n
  15. 0015apply beta_product_zero
  16. 0016exact hn
  17. 0017have hq1 : q = 1
  18. 0018specialize beta_product_zero d
  19. 0019specialize beta_product_zero e
  20. 0020specialize beta_product_zero q
  21. 0021apply beta_product_zero
  22. 0022exact hq
  23. 0023rewrite hn1
  24. 0024rewrite hq1
  25. 0025specialize le_refl 1
  26. 0026exact le_refl
  27. 0027intro n
  28. 0028intro q
  29. 0029intro hpw
  30. 0030intro hn
  31. 0031intro hq
  32. 0032have hnd : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ n = r · a)
    Exact native replay linehave hnd : exists a r. (((exists ff_h_bppl_left_decomposition_entry. ff_h_bppl_left_decomposition_entry + S (a) = S ((S (l)) * c)) /\ exists ff_q_bppl_left_decomposition_entry. b = ff_q_bppl_left_decomposition_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_bppl_left_decomposition_product ff_v_bppl_left_decomposition_product. ((((exists ff_h_bppl_left_decomposition_product_start. ff_h_bppl_left_decomposition_product_start + S (1) = S ((S (0)) * ff_v_bppl_left_decomposition_product)) /\ exists ff_q_bppl_left_decomposition_product_start. ff_u_bppl_left_decomposition_product = ff_q_bppl_left_decomposition_product_start * S ((S (0)) * ff_v_bppl_left_decomposition_product) + (1))) /\ ((((exists ff_h_bppl_left_decomposition_product_terminal. ff_h_bppl_left_decomposition_product_terminal + S (r) = S ((S (l)) * ff_v_bppl_left_decomposition_product)) /\ exists ff_q_bppl_left_decomposition_product_terminal. ff_u_bppl_left_decomposition_product = ff_q_bppl_left_decomposition_product_terminal * S ((S (l)) * ff_v_bppl_left_decomposition_product) + (r))) /\ forall ff_i_bppl_left_decomposition_product. (exists ff_lt_bppl_left_decomposition_product_bound. ff_lt_bppl_left_decomposition_product_bound + S ff_i_bppl_left_decomposition_product = l) -> exists ff_p_bppl_left_decomposition_product ff_r_bppl_left_decomposition_product ff_s_bppl_left_decomposition_product. ((((exists ff_h_bppl_left_decomposition_product_factor. ff_h_bppl_left_decomposition_product_factor + S (ff_p_bppl_left_decomposition_product) = S ((S (ff_i_bppl_left_decomposition_product)) * c)) /\ exists ff_q_bppl_left_decomposition_product_factor. b = ff_q_bppl_left_decomposition_product_factor * S ((S (ff_i_bppl_left_decomposition_product)) * c) + (ff_p_bppl_left_decomposition_product))) /\ ((((exists ff_h_bppl_left_decomposition_product_partial. ff_h_bppl_left_decomposition_product_partial + S (ff_r_bppl_left_decomposition_product) = S ((S (ff_i_bppl_left_decomposition_product)) * ff_v_bppl_left_decomposition_product)) /\ exists ff_q_bppl_left_decomposition_product_partial. ff_u_bppl_left_decomposition_product = ff_q_bppl_left_decomposition_product_partial * S ((S (ff_i_bppl_left_decomposition_product)) * ff_v_bppl_left_decomposition_product) + (ff_r_bppl_left_decomposition_product))) /\ ((((exists ff_h_bppl_left_decomposition_product_successor. ff_h_bppl_left_decomposition_product_successor + S (ff_s_bppl_left_decomposition_product) = S ((S (S ff_i_bppl_left_decomposition_product)) * ff_v_bppl_left_decomposition_product)) /\ exists ff_q_bppl_left_decomposition_product_successor. ff_u_bppl_left_decomposition_product = ff_q_bppl_left_decomposition_product_successor * S ((S (S ff_i_bppl_left_decomposition_product)) * ff_v_bppl_left_decomposition_product) + (ff_s_bppl_left_decomposition_product))) /\ ff_s_bppl_left_decomposition_product = ff_r_bppl_left_decomposition_product * ff_p_bppl_left_decomposition_product)))))) /\ n = r * a)
  33. 0033specialize beta_product_succ_decompose b
  34. 0034specialize beta_product_succ_decompose c
  35. 0035specialize beta_product_succ_decompose l
  36. 0036specialize beta_product_succ_decompose n
  37. 0037apply beta_product_succ_decompose
  38. 0038exact hn
  39. 0039cases hnd
  40. 0040cases hnd_witness
  41. 0041cases hnd_witness_witness
  42. 0042cases hnd_witness_witness_right
  43. 0043have hqd : ∃ a. ∃ r. BetaAt(d,e,l,a) ∧ (Product(d,e,l,r) ∧ q = r · a)
    Exact native replay linehave hqd : exists a r. (((exists ff_h_bppl_right_decomposition_entry. ff_h_bppl_right_decomposition_entry + S (a) = S ((S (l)) * e)) /\ exists ff_q_bppl_right_decomposition_entry. d = ff_q_bppl_right_decomposition_entry * S ((S (l)) * e) + (a))) /\ ((exists ff_u_bppl_right_decomposition_product ff_v_bppl_right_decomposition_product. ((((exists ff_h_bppl_right_decomposition_product_start. ff_h_bppl_right_decomposition_product_start + S (1) = S ((S (0)) * ff_v_bppl_right_decomposition_product)) /\ exists ff_q_bppl_right_decomposition_product_start. ff_u_bppl_right_decomposition_product = ff_q_bppl_right_decomposition_product_start * S ((S (0)) * ff_v_bppl_right_decomposition_product) + (1))) /\ ((((exists ff_h_bppl_right_decomposition_product_terminal. ff_h_bppl_right_decomposition_product_terminal + S (r) = S ((S (l)) * ff_v_bppl_right_decomposition_product)) /\ exists ff_q_bppl_right_decomposition_product_terminal. ff_u_bppl_right_decomposition_product = ff_q_bppl_right_decomposition_product_terminal * S ((S (l)) * ff_v_bppl_right_decomposition_product) + (r))) /\ forall ff_i_bppl_right_decomposition_product. (exists ff_lt_bppl_right_decomposition_product_bound. ff_lt_bppl_right_decomposition_product_bound + S ff_i_bppl_right_decomposition_product = l) -> exists ff_p_bppl_right_decomposition_product ff_r_bppl_right_decomposition_product ff_s_bppl_right_decomposition_product. ((((exists ff_h_bppl_right_decomposition_product_factor. ff_h_bppl_right_decomposition_product_factor + S (ff_p_bppl_right_decomposition_product) = S ((S (ff_i_bppl_right_decomposition_product)) * e)) /\ exists ff_q_bppl_right_decomposition_product_factor. d = ff_q_bppl_right_decomposition_product_factor * S ((S (ff_i_bppl_right_decomposition_product)) * e) + (ff_p_bppl_right_decomposition_product))) /\ ((((exists ff_h_bppl_right_decomposition_product_partial. ff_h_bppl_right_decomposition_product_partial + S (ff_r_bppl_right_decomposition_product) = S ((S (ff_i_bppl_right_decomposition_product)) * ff_v_bppl_right_decomposition_product)) /\ exists ff_q_bppl_right_decomposition_product_partial. ff_u_bppl_right_decomposition_product = ff_q_bppl_right_decomposition_product_partial * S ((S (ff_i_bppl_right_decomposition_product)) * ff_v_bppl_right_decomposition_product) + (ff_r_bppl_right_decomposition_product))) /\ ((((exists ff_h_bppl_right_decomposition_product_successor. ff_h_bppl_right_decomposition_product_successor + S (ff_s_bppl_right_decomposition_product) = S ((S (S ff_i_bppl_right_decomposition_product)) * ff_v_bppl_right_decomposition_product)) /\ exists ff_q_bppl_right_decomposition_product_successor. ff_u_bppl_right_decomposition_product = ff_q_bppl_right_decomposition_product_successor * S ((S (S ff_i_bppl_right_decomposition_product)) * ff_v_bppl_right_decomposition_product) + (ff_s_bppl_right_decomposition_product))) /\ ff_s_bppl_right_decomposition_product = ff_r_bppl_right_decomposition_product * ff_p_bppl_right_decomposition_product)))))) /\ q = r * a)
  44. 0044specialize beta_product_succ_decompose d
  45. 0045specialize beta_product_succ_decompose e
  46. 0046specialize beta_product_succ_decompose l
  47. 0047specialize beta_product_succ_decompose q
  48. 0048apply beta_product_succ_decompose
  49. 0049exact hq
  50. 0050cases hqd
  51. 0051cases hqd_witness
  52. 0052cases hqd_witness_witness
  53. 0053cases hqd_witness_witness_right
  54. 0054have hpw_prefix : ∀ i. ∀ a. ∀ z. Lt(i,l) → BetaAt(b,c,i,a) → BetaAt(d,e,i,z) → Le(a,z)
    Exact native replay linehave hpw_prefix : forall i a z. (exists bppl_prefix_bound. bppl_prefix_bound + S i = l) -> (((exists ff_h_bppl_prefix_left. ff_h_bppl_prefix_left + S (a) = S ((S (i)) * c)) /\ exists ff_q_bppl_prefix_left. b = ff_q_bppl_prefix_left * S ((S (i)) * c) + (a))) -> (((exists ff_h_bppl_prefix_right. ff_h_bppl_prefix_right + S (z) = S ((S (i)) * e)) /\ exists ff_q_bppl_prefix_right. d = ff_q_bppl_prefix_right * S ((S (i)) * e) + (z))) -> exists bppl_prefix_factor_gap. bppl_prefix_factor_gap + a = z
  55. 0055intro i
  56. 0056intro a
  57. 0057intro z
  58. 0058intro hi
  59. 0059intro ha
  60. 0060intro hz
  61. 0061specialize hpw i
  62. 0062specialize hpw a
  63. 0063specialize hpw z
  64. 0064apply hpw
  65. 0065specialize le_succ (S i)
  66. 0066specialize le_succ l
  67. 0067apply le_succ
  68. 0068exact hi
  69. 0069exact ha
  70. 0070exact hz
  71. 0071have hprefix : Le(x1,x3)
    Exact native replay linehave hprefix : exists k. k + x1 = x3
  72. 0072specialize IH x1
  73. 0073specialize IH x3
  74. 0074apply IH
  75. 0075exact hpw_prefix
  76. 0076exact hnd_witness_witness_right_left
  77. 0077exact hqd_witness_witness_right_left
  78. 0078have hentry : Le(x,x2)
    Exact native replay linehave hentry : exists k. k + x = x2
  79. 0079specialize hpw l
  80. 0080specialize hpw x
  81. 0081specialize hpw x2
  82. 0082apply hpw
  83. 0083specialize le_refl (S l)
  84. 0084exact le_refl
  85. 0085exact hnd_witness_witness_left
  86. 0086exact hqd_witness_witness_left
  87. 0087have hfold : Le(x1 · x,x3 · x2)
    Exact native replay linehave hfold : exists k. k + (x1 * x) = (x3 * x2)
  88. 0088specialize mul_le_mul x1
  89. 0089specialize mul_le_mul x3
  90. 0090specialize mul_le_mul x
  91. 0091specialize mul_le_mul x2
  92. 0092apply mul_le_mul
  93. 0093exact hprefix
  94. 0094exact hentry
  95. 0095rewrite hnd_witness_witness_right_right
  96. 0096rewrite hqd_witness_witness_right_right
  97. 0097exact hfold