beta_product_succ_append

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

1. 0001intro b
2. 0002intro c
3. 0003intro l
4. 0004intro r
5. 0005intro p
6. 0006intro hproduct
7. 0007intro hp
8. 0008cases hproduct
9. 0009cases hproduct_witness
10. 0010cases hproduct_witness_witness
11. 0011cases hproduct_witness_witness_right
12. 0012have hext : exists z d. (((exists h. h + S (r * p) = S ((S S l) * d)) /\ exists q. z = q * S ((S S l) * d) + (r * p)) /\ forall i a. (exists h. h + S i = S l) -> ((exists h. h + S a = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + a) -> ((exists h. h + S a = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + a))
13. 0013specialize beta_prefix_extend (S l)
14. 0014specialize beta_prefix_extend x
15. 0015specialize beta_prefix_extend x1
16. 0016specialize beta_prefix_extend (r * p)
17. 0017exact beta_prefix_extend
18. 0018cases hext
19. 0019cases hext_witness
20. 0020cases hext_witness_witness
21. 0021exists x2
22. 0022exists x3
23. 0023split
24. 0024specialize hext_witness_witness_right 0
25. 0025specialize hext_witness_witness_right 1
26. 0026apply hext_witness_witness_right
27. 0027have hzero : exists h. h + 0 = l
28. 0028specialize zero_le l
29. 0029exact zero_le
30. 0030specialize succ_le_succ 0
31. 0031specialize succ_le_succ l
32. 0032apply succ_le_succ
33. 0033exact hzero
34. 0034exact hproduct_witness_witness_left
35. 0035split
36. 0036exact hext_witness_witness_left
37. 0037intro i
38. 0038intro hi
39. 0039have hil : exists h. h + i = l
40. 0040specialize le_of_succ_le_succ i
41. 0041specialize le_of_succ_le_succ l
42. 0042apply le_of_succ_le_succ
43. 0043exact hi
44. 0044have hsplit : i = l \/ exists h. h + S i = l
45. 0045specialize le_eq_or_lt i
46. 0046specialize le_eq_or_lt l
47. 0047apply le_eq_or_lt
48. 0048exact hil
49. 0049cases hsplit
50. 0050exists p
51. 0051exists r
52. 0052exists r * p
53. 0053split
54. 0054rewrite hsplit_left
55. 0055rewrite hsplit_left
56. 0056exact hp
57. 0057split
58. 0058rewrite hsplit_left
59. 0059rewrite hsplit_left
60. 0060specialize hext_witness_witness_right l
61. 0061specialize hext_witness_witness_right r
62. 0062apply hext_witness_witness_right
63. 0063specialize le_refl (S l)
64. 0064exact le_refl
65. 0065exact hproduct_witness_witness_right_left
66. 0066split
67. 0067rewrite hsplit_left
68. 0068rewrite hsplit_left
69. 0069exact hext_witness_witness_left
70. 0070refl
71. 0071have hold : exists p0 r0 s0. (((exists h. h + S p0 = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p0) /\ (((exists h. h + S r0 = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + r0) /\ (((exists h. h + S s0 = S ((S S i) * x1)) /\ exists q. x = q * S ((S S i) * x1) + s0) /\ s0 = r0 * p0)))
72. 0072specialize hproduct_witness_witness_right_right i
73. 0073apply hproduct_witness_witness_right_right
74. 0074exact hsplit_right
75. 0075cases hold
76. 0076cases hold_witness
77. 0077cases hold_witness_witness
78. 0078cases hold_witness_witness_witness
79. 0079cases hold_witness_witness_witness_right
80. 0080cases hold_witness_witness_witness_right_right
81. 0081exists x4
82. 0082exists x5
83. 0083exists x6
84. 0084split
85. 0085exact hold_witness_witness_witness_left
86. 0086split
87. 0087specialize hext_witness_witness_right i
88. 0088specialize hext_witness_witness_right x5
89. 0089apply hext_witness_witness_right
90. 0090exact hi
91. 0091exact hold_witness_witness_witness_right_left
92. 0092split
93. 0093specialize hext_witness_witness_right (S i)
94. 0094specialize hext_witness_witness_right x6
95. 0095apply hext_witness_witness_right
96. 0096specialize succ_le_succ (S i)
97. 0097specialize succ_le_succ l
98. 0098apply succ_le_succ
99. 0099exact hsplit_right
100. 0100exact hold_witness_witness_witness_right_right_left
101. 0101exact hold_witness_witness_witness_right_right_right