Prime-Field Polynomial GCD and Bézout — exact evidence

forall n. 0 + n = n

1. induction n
2. simp
3. simp [IH]

forall n m. S n + m = S (n + m)

1. intro n
2. induction m
3. simp
4. simp [IH]

forall n m. n + m = m + n

1. intro n
2. induction m
3. simp [zero_add]
4. simp [add_succ_left, IH]

forall n m k. (n + m) + k = n + (m + k)

1. intro n
2. intro m
3. induction k
4. simp
5. simp [IH]

forall n. 0 * n = 0

1. induction n
2. simp
3. simp [IH]

forall n m. S n * m = n * m + m

1. intro n
2. induction m
3. simp
4. specialize add_comm n
5. specialize add_comm m
6. simp [IH, add_comm, add_assoc]

forall n m. n * m = m * n

1. intro n
2. induction m
3. simp [mul_zero_left]
4. simp [IH, mul_succ_left]

forall n m k. n * (m + k) = n * m + n * k

1. intro n
2. intro m
3. induction k
4. simp
5. simp [IH, add_assoc]

forall n m k. (n * m) * k = n * (m * k)

1. intro n
2. intro m
3. induction k
4. simp
5. simp [IH, mul_add]

forall n. 1 * n = n

1. induction n
2. simp
3. simp [IH]

forall n. n * 1 = n

1. intro n
2. simp [zero_add]

forall n m k. (n + m) * k = n * k + m * k

1. intro n
2. intro m
3. intro k
4. simp [mul_comm, mul_add]

forall n. ~(S n = 0)

1. apply PA1

forall n m. S n = S m -> n = m

1. apply PA2

forall n. n <= n

1. intro n
2. exists 0
3. simp [zero_add]

forall n m k. n <= m -> m <= k -> n <= k

1. intro n
2. intro m
3. intro k
4. intro h_nm
5. intro h_mk
6. cases h_nm
7. cases h_mk
8. exists x1 + x
9. simp [add_assoc, h_nm_witness, h_mk_witness]

forall p n. S p + n = n -> false

1. intro p
2. induction n
3. intro h
4. apply PA1
5. rewrite PA3 at h
6. exact h
7. intro h
8. apply IH
9. apply PA2
10. rewrite PA4 at h
11. exact h

forall a b n. (b + a) + n = n -> a + n = n

1. intro a
2. induction b
3. intro n
4. intro h
5. specialize zero_add a
6. rewrite zero_add at h
7. exact h
8. intro n
9. intro h
10. exfalso
11. specialize no_succ_add_fixed (b + a)
12. specialize no_succ_add_fixed n
13. apply no_succ_add_fixed
14. specialize add_succ_left b
15. specialize add_succ_left a
16. rewrite add_succ_left at h
17. exact h

forall a b n m. a + n = m -> b + m = n -> n = m

1. intro a
2. intro b
3. intro n
4. intro m
5. intro h_anm
6. intro h_bmn
7. symm
8. rewrite <- h_anm
9. specialize drop_add_prefix_from_fixed a
10. specialize drop_add_prefix_from_fixed b
11. specialize drop_add_prefix_from_fixed n
12. apply drop_add_prefix_from_fixed
13. specialize add_assoc b
14. specialize add_assoc a
15. specialize add_assoc n
16. rewrite add_assoc
17. rewrite h_anm
18. rewrite h_bmn
19. refl

forall n m. n <= m -> m <= n -> n = m

1. intro n
2. intro m
3. intro h_nm
4. intro h_mn
5. cases h_nm
6. cases h_mn
7. apply antisymm_from_witnesses
8. exact h_nm_witness
9. exact h_mn_witness

forall n m. n <= m \/ m <= n

1. induction n
2. intro m
3. left
4. exists m
5. simp
6. induction m
7. right
8. exists (S n)
9. simp
10. specialize IH m
11. cases IH
12. cases IH_left
13. left
14. exists x
15. rewrite PA4
16. congr
17. exact IH_left_witness
18. cases IH_right
19. right
20. exists x
21. rewrite PA4
22. congr
23. exact IH_right_witness

forall a b. a + b = 0 -> b = 0

1. intro a
2. induction b
3. intro h
4. refl
5. intro h
6. exfalso
7. apply PA1
8. rewrite PA4 at h
9. exact h

forall n m. n * m = 0 -> n = 0 \/ m = 0

1. intro n
2. induction m
3. intro h
4. right
5. refl
6. intro h
7. left
8. specialize add_eq_zero_right (n * m)
9. specialize add_eq_zero_right n
10. apply add_eq_zero_right
11. rewrite PA6 at h
12. exact h

forall n. n = 0 \/ exists k. n = S k

1. induction n
2. left
3. refl
4. right
5. exists n
6. refl

forall n. ~(n = 0) -> exists k. n = S k

1. induction n
2. intro h
3. exfalso
4. apply h
5. refl
6. intro h
7. exists n
8. refl

forall a b c d. a = b -> c = d -> a + c = b + d

1. intro a
2. intro b
3. intro c
4. intro d
5. intro hab
6. intro hcd
7. congr
8. exact hab
9. exact hcd

forall a b c. a + c = b + c -> a = b

1. intro a
2. intro b
3. induction c
4. intro h
5. rewrite PA3 at h
6. rewrite PA3 at h
7. exact h
8. intro h
9. apply IH
10. apply PA2
11. rewrite PA4 at h
12. rewrite PA4 at h
13. exact h

forall a b c. a + b = a + c -> b = c

1. intro a
2. intro b
3. intro c
4. intro h
5. specialize add_right_cancel b
6. specialize add_right_cancel c
7. specialize add_right_cancel a
8. apply add_right_cancel
9. trans a + b
10. apply add_comm
11. trans a + c
12. exact h
13. apply add_comm

forall n. 0 <= n

1. intro n
2. exists n
3. rewrite PA3
4. refl

forall n. n <= S n

1. intro n
2. exists 1
3. simp [add_succ_left, zero_add]

forall n. n <= 0 -> n = 0

1. intro n
2. intro h
3. cases h
4. apply add_eq_zero_right
5. exact h_witness

forall n. ~(n = 0) -> 1 <= n

1. induction n
2. intro h
3. exfalso
4. apply h
5. refl
6. intro h
7. exists n
8. simp

forall a b. exists k. k + a = b + a

1. intro a
2. intro b
3. exists b
4. refl

forall a b. exists k. k + a = a + b

1. intro a
2. intro b
3. exists b
4. apply add_comm

forall a b c. (exists k. k + a = b) -> exists r. r + (a + c) = b + c

1. intro a
2. intro b
3. intro c
4. intro h
5. cases h
6. exists x
7. trans (x + a) + c
8. symm
9. apply add_assoc
10. congr
11. exact h_witness
12. refl

forall a b c. (exists k. k + a = b) -> exists r. r + (c + a) = c + b

1. intro a
2. intro b
3. intro c
4. intro h
5. cases h
6. exists x
7. trans (x + c) + a
8. symm
9. apply add_assoc
10. trans (c + x) + a
11. congr
12. apply add_comm
13. refl
14. trans c + (x + a)
15. apply add_assoc
16. congr
17. refl
18. exact h_witness

forall a b. (exists k. k + a = b) -> exists r. r + S a = S b

1. intro a
2. intro b
3. intro h
4. cases h
5. exists x
6. rewrite PA4
7. congr
8. exact h_witness

forall a b. (exists k. k + S a = S b) -> exists r. r + a = b

1. intro a
2. intro b
3. intro h
4. cases h
5. exists x
6. apply PA2
7. trans x + S a
8. symm
9. apply PA4
10. exact h_witness

forall a b. (exists k. k + a = b) -> exists r. r + a = S b

1. intro a
2. intro b
3. intro h
4. cases h
5. exists S x
6. trans S (x + a)
7. apply add_succ_left
8. congr
9. exact h_witness

forall a b. (exists k. k + S a = b) -> exists r. r + a = b

1. intro a
2. intro b
3. intro h
4. cases h
5. exists S x
6. trans x + S a
7. trans S (x + a)
8. apply add_succ_left
9. symm
10. apply PA4
11. exact h_witness

forall a b c. (exists k. k + (a + c) = b + c) -> exists r. r + a = b

1. intro a
2. intro b
3. intro c
4. intro h
5. cases h
6. exists x
7. specialize add_right_cancel (x + a)
8. specialize add_right_cancel b
9. specialize add_right_cancel c
10. apply add_right_cancel
11. trans x + (a + c)
12. apply add_assoc
13. exact h_witness

forall n. ~(exists k. k + S n = n)

1. intro n
2. intro h
3. cases h
4. specialize no_succ_add_fixed x
5. specialize no_succ_add_fixed n
6. apply no_succ_add_fixed
7. trans x + S n
8. trans S (x + n)
9. apply add_succ_left
10. symm
11. apply PA4
12. exact h_witness

forall a b. (exists k. k + a = b) -> a = b \/ exists k. k + S a = b

1. intro a
2. intro b
3. intro h
4. cases h
5. specialize zero_or_succ x
6. cases zero_or_succ
7. left
8. rewrite zero_or_succ_left at h_witness
9. specialize zero_add a
10. rewrite zero_add at h_witness
11. exact h_witness
12. cases zero_or_succ_right
13. right
14. exists x1
15. trans S x1 + a
16. trans S (x1 + a)
17. apply PA4
18. symm
19. apply add_succ_left
20. rewrite <- zero_or_succ_right_witness
21. exact h_witness

forall a b c. (exists k. k + S a = b) -> (exists k. k + b = c) -> exists k. k + S a = c

1. intro a
2. intro b
3. intro c
4. intro hab
5. intro hbc
6. specialize le_trans (S a)
7. specialize le_trans b
8. specialize le_trans c
9. apply le_trans
10. exact hab
11. exact hbc

forall a b. (exists k. k + a = b) \/ exists k. k + S b = a

1. induction a
2. intro b
3. left
4. exists b
5. apply PA3
6. induction b
7. right
8. exists a
9. trans S (a + 0)
10. apply PA4
11. congr
12. apply PA3
13. specialize IH b
14. cases IH
15. left
16. cases IH_left
17. exists x
18. rewrite PA4
19. congr
20. exact IH_left_witness
21. right
22. cases IH_right
23. exists x
24. rewrite PA4
25. congr
26. exact IH_right_witness

forall a b. a = b \/ ((exists k. k + S a = b) \/ exists k. k + S b = a)

1. induction a
2. induction b
3. left
4. refl
5. right
6. left
7. exists b
8. trans S (b + 0)
9. apply PA4
10. congr
11. apply PA3
12. induction b
13. right
14. right
15. exists a
16. trans S (a + 0)
17. apply PA4
18. congr
19. apply PA3
20. specialize IH b
21. cases IH
22. left
23. congr
24. exact IH_left
25. cases IH_right
26. right
27. left
28. cases IH_right_left
29. exists x
30. rewrite PA4
31. congr
32. exact IH_right_left_witness
33. right
34. right
35. cases IH_right_right
36. exists x
37. rewrite PA4
38. congr
39. exact IH_right_right_witness

forall a b. (exists k. k + S a = b) -> ~ (exists k. k + b = a)

1. have hbad : forall z u v. ~(z = u + (v + S z))
2. intro z
3. induction z
4. intro u
5. intro v
6. intro hz
7. apply PA1
8. symm
9. rewrite PA4 at hz
10. rewrite PA4 at hz
11. exact hz
12. intro u
13. intro v
14. intro hz
15. specialize IH u
16. specialize IH v
17. apply IH
18. apply PA2
19. rewrite PA4 at hz
20. rewrite PA4 at hz
21. exact hz
22. intro a
23. intro b
24. intro hab
25. intro hba
26. cases hab
27. cases hba
28. specialize hbad a
29. specialize hbad x1
30. specialize hbad x
31. apply hbad
32. symm
33. rewrite <- hab_witness at hba_witness
34. exact hba_witness

forall r m a b. (exists k. k + S r = m) -> ~(r = (a + m) + b)

1. have hbad : forall z a w b. ~(z = (a + (w + S z)) + b)
2. intro z
3. induction z
4. intro a
5. intro w
6. intro b
7. intro hz
8. apply PA1
9. symm
10. rewrite PA4 at hz
11. rewrite PA4 at hz
12. specialize add_succ_left (a + (w + 0))
13. specialize add_succ_left b
14. rewrite add_succ_left at hz
15. exact hz
16. intro a
17. intro w
18. intro b
19. intro hz
20. specialize IH a
21. specialize IH w
22. specialize IH b
23. apply IH
24. apply PA2
25. rewrite PA4 at hz
26. rewrite PA4 at hz
27. specialize add_succ_left (a + (w + S z))
28. specialize add_succ_left b
29. rewrite add_succ_left at hz
30. exact hz
31. intro r
32. intro m
33. intro a
34. intro b
35. intro hr
36. intro heq
37. cases hr
38. specialize hbad r
39. specialize hbad a
40. specialize hbad x
41. specialize hbad b
42. apply hbad
43. rewrite <- hr_witness at heq
44. exact heq

forall a b c. (exists k. k + a = b) -> exists r. r + a * c = b * c

1. intro a
2. intro b
3. intro c
4. intro h
5. cases h
6. exists x * c
7. trans (x + a) * c
8. symm
9. apply add_mul
10. congr
11. exact h_witness
12. refl

forall d n. exists q r. n = S d * q + r /\ S r <= S d

1. intro d
2. induction n
3. exists 0
4. exists 0
5. split
6. simp
7. exists d
8. simp
9. cases IH
10. cases IH_witness
11. cases IH_witness_witness
12. cases IH_witness_witness_right
13. specialize zero_or_succ x2
14. cases zero_or_succ
15. rewrite zero_or_succ_left at IH_witness_witness_right_witness
16. specialize zero_add S x1
17. rewrite zero_add at IH_witness_witness_right_witness
18. have hrd : x1 = d
19. apply PA2
20. exact IH_witness_witness_right_witness
21. exists S x
22. exists 0
23. split
24. rewrite IH_witness_witness_left
25. rewrite hrd
26. simp
27. exists d
28. simp
29. cases zero_or_succ_right
30. exists x
31. exists S x1
32. split
33. rewrite IH_witness_witness_left
34. simp
35. exists x3
36. rewrite <- IH_witness_witness_right_witness
37. rewrite zero_or_succ_right_witness
38. simp [add_succ_left]

forall m n. ~(m = 0) -> exists q r. n = m * q + r /\ S r <= m

1. intro m
2. intro n
3. intro hm
4. specialize zero_or_succ m
5. cases zero_or_succ
6. exfalso
7. apply hm
8. exact zero_or_succ_left
9. cases zero_or_succ_right
10. specialize division_remainder_succ x
11. specialize division_remainder_succ n
12. rewrite zero_or_succ_right_witness
13. rewrite zero_or_succ_right_witness
14. exact division_remainder_succ

forall m q q2 r s k. (exists z. z + S r = m) -> S k + q = q2 -> ~(m * q + r = m * q2 + s)

1. intro m
2. intro q
3. intro q2
4. intro r
5. intro s
6. intro k
7. intro hr
8. intro hgap
9. intro heq
10. specialize lt_not_eq_add_middle r
11. specialize lt_not_eq_add_middle m
12. specialize lt_not_eq_add_middle (m * k)
13. specialize lt_not_eq_add_middle s
14. apply lt_not_eq_add_middle
15. exact hr
16. specialize add_left_cancel (m * q)
17. specialize add_left_cancel r
18. specialize add_left_cancel ((m * k + m) + s)
19. apply add_left_cancel
20. trans m * q2 + s
21. exact heq
22. rewrite <- hgap
23. specialize add_comm S k
24. specialize add_comm q
25. rewrite add_comm
26. specialize mul_add m
27. specialize mul_add q
28. specialize mul_add S k
29. rewrite mul_add
30. rewrite PA6
31. specialize add_assoc (m * q)
32. specialize add_assoc (m * k + m)
33. specialize add_assoc s
34. apply add_assoc

forall m n q r q2 r2. n = m * q + r -> (exists k. k + S r = m) -> n = m * q2 + r2 -> (exists k. k + S r2 = m) -> q = q2 /\ r = r2

1. intro m
2. intro n
3. intro q
4. intro r
5. intro q2
6. intro r2
7. intro h1
8. intro hr
9. intro h2
10. intro hr2
11. have hsum : m * q + r = m * q2 + r2
12. trans n
13. symm
14. exact h1
15. exact h2
16. specialize le_total q
17. specialize le_total q2
18. cases le_total
19. cases le_total_left
20. specialize zero_or_succ x
21. cases zero_or_succ
22. rewrite zero_or_succ_left at le_total_left_witness
23. specialize zero_add q
24. rewrite zero_add at le_total_left_witness
25. split
26. exact le_total_left_witness
27. specialize add_left_cancel (m * q)
28. specialize add_left_cancel r
29. specialize add_left_cancel r2
30. apply add_left_cancel
31. rewrite <- le_total_left_witness at hsum
32. exact hsum
33. cases zero_or_succ_right
34. exfalso
35. specialize positive_quotient_gap_impossible m
36. specialize positive_quotient_gap_impossible q
37. specialize positive_quotient_gap_impossible q2
38. specialize positive_quotient_gap_impossible r
39. specialize positive_quotient_gap_impossible r2
40. specialize positive_quotient_gap_impossible x1
41. apply positive_quotient_gap_impossible
42. exact hr
43. rewrite zero_or_succ_right_witness at le_total_left_witness
44. exact le_total_left_witness
45. exact hsum
46. cases le_total_right
47. specialize zero_or_succ x
48. cases zero_or_succ
49. rewrite zero_or_succ_left at le_total_right_witness
50. specialize zero_add q2
51. rewrite zero_add at le_total_right_witness
52. split
53. symm
54. exact le_total_right_witness
55. specialize add_left_cancel (m * q)
56. specialize add_left_cancel r
57. specialize add_left_cancel r2
58. apply add_left_cancel
59. rewrite le_total_right_witness at hsum
60. exact hsum
61. cases zero_or_succ_right
62. exfalso
63. specialize positive_quotient_gap_impossible m
64. specialize positive_quotient_gap_impossible q2
65. specialize positive_quotient_gap_impossible q
66. specialize positive_quotient_gap_impossible r2
67. specialize positive_quotient_gap_impossible r
68. specialize positive_quotient_gap_impossible x1
69. apply positive_quotient_gap_impossible
70. exact hr2
71. rewrite zero_or_succ_right_witness at le_total_right_witness
72. exact le_total_right_witness
73. symm
74. exact hsum

forall a b. a + b = 0 -> a = 0

1. intro a
2. intro b
3. intro h
4. specialize add_eq_zero_right b
5. specialize add_eq_zero_right a
6. apply add_eq_zero_right
7. trans a + b
8. apply add_comm
9. exact h

forall a b. a * b = 1 -> a = 1 /\ b = 1

1. intro a
2. induction a
3. intro b
4. intro h
5. specialize mul_zero_left b
6. rewrite mul_zero_left at h
7. exfalso
8. apply PA1
9. symm
10. exact h
11. intro b
12. induction b
13. intro h
14. rewrite PA5 at h
15. exfalso
16. apply PA1
17. symm
18. exact h
19. intro h
20. rewrite PA6 at h
21. rewrite PA4 at h
22. have hz : S a * b + a = 0
23. apply PA2
24. exact h
25. specialize add_eq_zero_right (S a * b)
26. specialize add_eq_zero_right a
27. have ha0 : a = 0
28. apply add_eq_zero_right
29. exact hz
30. split
31. congr
32. exact ha0
33. rewrite ha0 at hz
34. rewrite ha0 at hz
35. rewrite PA3 at hz
36. specialize one_mul b
37. rewrite one_mul at hz
38. congr
39. exact hz

forall a b. ~(a = 0) -> ~(b = 0) -> ~(a * b = 0)

1. intro a
2. intro b
3. intro ha
4. intro hb
5. intro hab
6. specialize mul_eq_zero a
7. specialize mul_eq_zero b
8. have hz : a = 0 \/ b = 0
9. apply mul_eq_zero
10. exact hab
11. cases hz
12. apply ha
13. exact hz_left
14. apply hb
15. exact hz_right

forall a. exists q. 0 = a * q

1. intro a
2. exists 0
3. rewrite PA5
4. refl

forall a. exists q. a = a * q

1. intro a
2. exists 1
3. symm
4. apply mul_one

forall a n m. (exists q. n = a * q) -> exists s. n * m = a * s

1. intro a
2. intro n
3. intro m
4. intro hn
5. cases hn
6. exists x * m
7. rewrite hn_witness
8. apply mul_assoc

forall a b n. (exists q. n = a * q) -> (exists r. a = b * r) -> exists s. n = b * s

1. intro a
2. intro b
3. intro n
4. intro hn
5. intro hab
6. cases hn
7. cases hab
8. exists x1 * x
9. rewrite hn_witness
10. rewrite hab_witness
11. apply mul_assoc

forall d n. ~(n = 0) -> (exists q. n = d * q) -> exists k. k + d = n

1. intro d
2. intro n
3. intro hn
4. intro hd
5. cases hd
6. have hq : ~(x = 0)
7. intro hx
8. apply hn
9. trans d * x
10. exact hd_witness
11. rewrite hx
12. apply PA5
13. specialize one_le_of_ne_zero x
14. have h1q : exists k. k + 1 = x
15. apply one_le_of_ne_zero
16. exact hq
17. cases h1q
18. have hs : S x1 = x
19. trans x1 + 1
20. simp
21. exact h1q_witness
22. exists d * x1
23. trans d * S x1
24. symm
25. apply PA6
26. trans d * x
27. congr
28. refl
29. exact hs
30. symm
31. exact hd_witness

forall d. (exists y. 1 = d * y) -> d = 1

1. intro d
2. intro h
3. cases h
4. specialize mul_eq_one_components d
5. specialize mul_eq_one_components x
6. have parts : d = 1 /\ x = 1
7. apply mul_eq_one_components
8. symm
9. exact h_witness
10. cases parts
11. exact parts_left

forall c u v r. c * u = c * v + r -> exists w. r = c * w

1. intro c
2. induction u
3. intro v
4. intro r
5. intro h
6. rewrite PA5 at h
7. have hr : r = 0
8. apply add_eq_zero_right
9. symm
10. exact h
11. exists 0
12. rewrite hr
13. rewrite PA5
14. refl
15. intro v
16. induction v
17. intro r
18. intro h
19. exists S u
20. rewrite PA5 at h
21. specialize zero_add r
22. rewrite zero_add at h
23. symm
24. exact h
25. intro r
26. intro h
27. have hred : c * u = c * v + r
28. specialize add_right_cancel (c * u)
29. specialize add_right_cancel (c * v + r)
30. specialize add_right_cancel c
31. apply add_right_cancel
32. rewrite PA6 at h
33. rewrite PA6 at h
34. trans (c * v + c) + r
35. exact h
36. trans c * v + (c + r)
37. apply add_assoc
38. trans c * v + (r + c)
39. congr
40. refl
41. apply add_comm
42. symm
43. apply add_assoc
44. specialize IH v
45. specialize IH r
46. apply IH
47. exact hred

forall c a b q r. (exists u. a = c * u) -> (exists v. b = c * v) -> a = b * q + r -> exists w. r = c * w

1. intro c
2. intro a
3. intro b
4. intro q
5. intro r
6. intro ha
7. intro hb
8. intro h
9. cases ha
10. cases hb
11. specialize factor_difference c
12. specialize factor_difference x
13. specialize factor_difference (x1 * q)
14. specialize factor_difference r
15. apply factor_difference
16. trans a
17. symm
18. exact ha_witness
19. trans b * q + r
20. exact h
21. congr
22. rewrite hb_witness
23. apply mul_assoc
24. refl

forall c b q r. (exists u. b = c * u) -> (exists v. r = c * v) -> exists w. b * q + r = c * w

1. intro c
2. intro b
3. intro q
4. intro r
5. intro hb
6. intro hr
7. cases hb
8. cases hr
9. exists x * q + x1
10. rewrite hb_witness
11. rewrite hr_witness
12. trans c * (x * q) + c * x1
13. congr
14. apply mul_assoc
15. refl
16. symm
17. apply mul_add

forall a. (((exists x. a = a * x) /\ (exists y. 0 = a * y)) /\ forall c. (exists u. a = c * u) -> (exists v. 0 = c * v) -> exists w. a = c * w)

1. intro a
2. split
3. split
4. specialize multiple_refl a
5. exact multiple_refl
6. specialize multiple_zero a
7. exact multiple_zero
8. intro c
9. intro ha
10. intro hz
11. exact ha

forall d a b q r. a = b * q + r -> (((exists x. b = d * x) /\ (exists y. r = d * y)) /\ forall c. (exists u. b = c * u) -> (exists v. r = c * v) -> exists w. d = c * w) -> (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

1. intro d
2. intro a
3. intro b
4. intro q
5. intro r
6. intro hstep
7. intro hg
8. cases hg
9. cases hg_left
10. split
11. split
12. rewrite hstep
13. specialize divides_linear_step d
14. specialize divides_linear_step b
15. specialize divides_linear_step q
16. specialize divides_linear_step r
17. apply divides_linear_step
18. exact hg_left_left
19. exact hg_left_right
20. exact hg_left_left
21. intro c
22. intro hca
23. intro hcb
24. specialize hg_right c
25. apply hg_right
26. exact hcb
27. specialize divides_remainder c
28. specialize divides_remainder a
29. specialize divides_remainder b
30. specialize divides_remainder q
31. specialize divides_remainder r
32. apply divides_remainder
33. exact hca
34. exact hcb
35. exact hstep

forall B b. (exists t. t + b = B) -> forall a. exists d. (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

1. intro B
2. induction B
3. intro b
4. intro hb
5. intro a
6. have hb0 : b = 0
7. apply le_zero
8. exact hb
9. exists a
10. split
11. split
12. specialize multiple_refl a
13. exact multiple_refl
14. exists 0
15. trans 0
16. exact hb0
17. symm
18. apply PA5
19. intro c
20. intro hca
21. intro hcb
22. exact hca
23. intro b
24. intro hb
25. intro a
26. specialize le_eq_or_lt b
27. specialize le_eq_or_lt (S B)
28. have hsplit : b = S B \/ exists k. k + S b = S B
29. apply le_eq_or_lt
30. exact hb
31. cases hsplit
32. have hb0 : ~(b = 0)
33. intro hzero
34. apply PA1
35. trans b
36. symm
37. exact hsplit_left
38. exact hzero
39. have hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
40. apply division_remainder_exists
41. exact hb0
42. cases hdiv
43. cases hdiv_witness
44. cases hdiv_witness_witness
45. have hrB : exists k. k + x1 = B
46. apply le_of_succ_le_succ
47. rewrite hsplit_left at hdiv_witness_witness_right
48. exact hdiv_witness_witness_right
49. have hsmall : exists d. (((exists u. b = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. b = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
50. specialize IH x1
51. have hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
52. apply IH
53. exact hrB
54. specialize hall b
55. exact hall
56. cases hsmall
57. exists x2
58. specialize is_gcd_euclid_forward x2
59. specialize is_gcd_euclid_forward a
60. specialize is_gcd_euclid_forward b
61. specialize is_gcd_euclid_forward x
62. specialize is_gcd_euclid_forward x1
63. apply is_gcd_euclid_forward
64. exact hdiv_witness_witness_left
65. exact hsmall_witness
66. have hbB : exists k. k + b = B
67. apply le_of_succ_le_succ
68. exact hsplit_right
69. specialize IH b
70. have hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. b = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. b = c * t) -> exists w. d = c * w)
71. apply IH
72. exact hbB
73. specialize hall a
74. exact hall

forall a b. exists d. (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

1. intro a
2. intro b
3. specialize gcd_exists_up_to b
4. specialize gcd_exists_up_to b
5. have hbb : exists t. t + b = b
6. apply le_refl
7. have hall : forall z. exists d. (((exists x. z = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. z = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)
8. apply gcd_exists_up_to
9. exact hbb
10. specialize hall a
11. exact hall

forall a d. (exists x. 1 = d * x) -> (exists y. a = d * y) -> d = 1

1. intro a
2. intro d
3. intro h1
4. intro ha
5. specialize divisor_one d
6. apply divisor_one
7. exact h1

forall a b. (((exists x. a = 1 * x) /\ (exists y. b = 1 * y)) /\ forall d. (exists u. a = d * u) -> (exists v. b = d * v) -> exists w. 1 = d * w) -> forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> c = 1

1. intro a
2. intro b
3. intro hg
4. intro c
5. intro ha
6. intro hb
7. cases hg
8. specialize hg_right c
9. have hd : exists w. 1 = c * w
10. apply hg_right
11. exact ha
12. exact hb
13. specialize divisor_one c
14. apply divisor_one
15. exact hd

forall a b c d. (a + b) + (c + d) = (c + b) + (a + d)

1. intro a
2. intro b
3. intro c
4. intro d
5. trans a + (b + (c + d))
6. apply add_assoc
7. trans a + ((b + c) + d)
8. congr
9. refl
10. symm
11. apply add_assoc
12. trans a + ((c + b) + d)
13. congr
14. refl
15. congr
16. apply add_comm
17. refl
18. trans (a + (c + b)) + d
19. symm
20. apply add_assoc
21. trans ((c + b) + a) + d
22. congr
23. apply add_comm
24. refl
25. apply add_assoc

forall a b q r d xp yp xn yn. a = b * q + r -> b * xp + r * yp = d + (b * xn + r * yn) -> a * yp + b * (xp + q * yn) = d + (a * yn + b * (xn + q * yp))

1. intro a
2. intro b
3. intro q
4. intro r
5. intro d
6. intro xp
7. intro yp
8. intro xn
9. intro yn
10. intro hab
11. intro hbez
12. rewrite hab
13. trans ((b * q) * yp + r * yp) + b * (xp + q * yn)
14. congr
15. apply add_mul
16. refl
17. trans ((b * q) * yp + r * yp) + (b * xp + b * (q * yn))
18. congr
19. refl
20. apply mul_add
21. trans ((b * q) * yp + r * yp) + (b * xp + (b * q) * yn)
22. congr
23. refl
24. congr
25. refl
26. symm
27. apply mul_assoc
28. trans (b * xp + r * yp) + ((b * q) * yp + (b * q) * yn)
29. apply add_permute_outer
30. trans (b * xp + r * yp) + ((b * q) * yn + (b * q) * yp)
31. congr
32. refl
33. apply add_comm
34. trans (d + (b * xn + r * yn)) + ((b * q) * yn + (b * q) * yp)
35. congr
36. exact hbez
37. refl
38. trans d + ((b * xn + r * yn) + ((b * q) * yn + (b * q) * yp))
39. apply add_assoc
40. trans d + (((b * q) * yn + r * yn) + (b * xn + (b * q) * yp))
41. congr
42. refl
43. apply add_permute_outer
44. trans d + ((b * q + r) * yn + (b * xn + (b * q) * yp))
45. congr
46. refl
47. congr
48. symm
49. apply add_mul
50. refl
51. trans d + ((b * q + r) * yn + (b * xn + b * (q * yp)))
52. congr
53. refl
54. congr
55. refl
56. congr
57. refl
58. apply mul_assoc
59. congr
60. refl
61. congr
62. congr
63. symm
64. exact hab
65. refl
66. symm
67. apply mul_add

forall B b. (exists t. t + b = B) -> forall a. exists d. ((((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w) /\ exists xp yp xn yn. a * xp + b * yp = d + (a * xn + b * yn))

1. intro B
2. induction B
3. intro b
4. intro hb
5. intro a
6. have hb0 : b = 0
7. apply le_zero
8. exact hb
9. exists a
10. split
11. rewrite hb0
12. rewrite hb0
13. specialize is_gcd_zero_right a
14. exact is_gcd_zero_right
15. exists 1
16. exists 0
17. exists 0
18. exists 0
19. rewrite hb0
20. simp [zero_add]
21. intro b
22. intro hb
23. intro a
24. specialize le_eq_or_lt b
25. specialize le_eq_or_lt (S B)
26. have hsplit : b = S B \/ exists k. k + S b = S B
27. apply le_eq_or_lt
28. exact hb
29. cases hsplit
30. have hb0 : ~(b = 0)
31. intro hzero
32. apply PA1
33. trans b
34. symm
35. exact hsplit_left
36. exact hzero
37. have hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
38. apply division_remainder_exists
39. exact hb0
40. cases hdiv
41. cases hdiv_witness
42. cases hdiv_witness_witness
43. have hrB : exists k. k + x1 = B
44. apply le_of_succ_le_succ
45. rewrite hsplit_left at hdiv_witness_witness_right
46. exact hdiv_witness_witness_right
47. have hsmall : exists d. ((((exists u. b = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. b = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w) /\ exists xp yp xn yn. b * xp + x1 * yp = d + (b * xn + x1 * yn))
48. specialize IH x1
49. have hall : forall z. exists d. ((((exists u. z = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w) /\ exists xp yp xn yn. z * xp + x1 * yp = d + (z * xn + x1 * yn))
50. apply IH
51. exact hrB
52. specialize hall b
53. exact hall
54. cases hsmall
55. cases hsmall_witness
56. cases hsmall_witness_right
57. cases hsmall_witness_right_witness
58. cases hsmall_witness_right_witness_witness
59. cases hsmall_witness_right_witness_witness_witness
60. exists x2
61. split
62. apply is_gcd_euclid_forward
63. exact hdiv_witness_witness_left
64. exact hsmall_witness_left
65. exists x4
66. exists x3 + x * x6
67. exists x6
68. exists x5 + x * x4
69. apply balanced_bezout_euclid_step
70. exact hdiv_witness_witness_left
71. exact hsmall_witness_right_witness_witness_witness_witness
72. have hbB : exists k. k + b = B
73. apply le_of_succ_le_succ
74. exact hsplit_right
75. specialize IH b
76. have hall : forall z. exists d. ((((exists u. z = d * u) /\ (exists v. b = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. b = c * t) -> exists w. d = c * w) /\ exists xp yp xn yn. z * xp + b * yp = d + (z * xn + b * yn))
77. apply IH
78. exact hbB
79. specialize hall a
80. exact hall

forall a b. exists d. ((((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w) /\ exists xp yp xn yn. a * xp + b * yp = d + (a * xn + b * yn))

1. intro a
2. intro b
3. specialize gcd_balanced_bezout_exists_up_to b
4. specialize gcd_balanced_bezout_exists_up_to b
5. have hbb : exists t. t + b = b
6. apply le_refl
7. have hall : forall z. exists d. ((((exists x. z = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. z = c * u) -> (exists v. b = c * v) -> exists w. d = c * w) /\ exists xp yp xn yn. z * xp + b * yp = d + (z * xn + b * yn))
8. apply gcd_balanced_bezout_exists_up_to
9. exact hbb
10. specialize hall a
11. exact hall

forall a b d xp yp xn yn z. a * xp + b * yp = d + (a * xn + b * yn) -> a * (xp * z) + (b * z) * yp = d * z + (a * (xn * z) + (b * z) * yn)

1. intro a
2. intro b
3. intro d
4. intro xp
5. intro yp
6. intro xn
7. intro yn
8. intro z
9. intro h
10. trans (a * xp) * z + (b * z) * yp
11. congr
12. symm
13. apply mul_assoc
14. refl
15. trans (a * xp) * z + (b * yp) * z
16. congr
17. refl
18. trans b * (z * yp)
19. apply mul_assoc
20. trans b * (yp * z)
21. congr
22. refl
23. apply mul_comm
24. symm
25. apply mul_assoc
26. trans (a * xp + b * yp) * z
27. symm
28. apply add_mul
29. trans (d + (a * xn + b * yn)) * z
30. congr
31. exact h
32. refl
33. trans d * z + (a * xn + b * yn) * z
34. apply add_mul
35. trans d * z + ((a * xn) * z + (b * yn) * z)
36. congr
37. refl
38. apply add_mul
39. trans d * z + (a * (xn * z) + (b * yn) * z)
40. congr
41. refl
42. congr
43. apply mul_assoc
44. refl
45. congr
46. refl
47. congr
48. refl
49. trans b * (yn * z)
50. apply mul_assoc
51. trans b * (z * yn)
52. congr
53. refl
54. apply mul_comm
55. symm
56. apply mul_assoc

forall c a b d xp yp xn yn. (exists u. a = c * u) -> (exists v. b = c * v) -> a * xp + b * yp = d + (a * xn + b * yn) -> exists w. d = c * w

1. intro c
2. intro a
3. intro b
4. intro d
5. intro xp
6. intro yp
7. intro xn
8. intro yn
9. intro ha
10. intro hb
11. intro h
12. cases ha
13. cases hb
14. specialize factor_difference c
15. specialize factor_difference (x * xp + x1 * yp)
16. specialize factor_difference (x * xn + x1 * yn)
17. specialize factor_difference d
18. apply factor_difference
19. trans c * (x * xp) + c * (x1 * yp)
20. apply mul_add
21. trans (c * x) * xp + (c * x1) * yp
22. congr
23. symm
24. apply mul_assoc
25. symm
26. apply mul_assoc
27. trans a * xp + b * yp
28. rewrite ha_witness
29. rewrite hb_witness
30. refl
31. trans d + (a * xn + b * yn)
32. exact h
33. trans (a * xn + b * yn) + d
34. apply add_comm
35. trans ((c * x) * xn + (c * x1) * yn) + d
36. rewrite ha_witness
37. rewrite hb_witness
38. refl
39. trans (c * (x * xn) + c * (x1 * yn)) + d
40. congr
41. congr
42. apply mul_assoc
43. apply mul_assoc
44. refl
45. congr
46. symm
47. apply mul_add
48. refl

forall a b. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> exists xp yp xn yn. a * xp + b * yp = 1 + (a * xn + b * yn)

1. intro a
2. intro b
3. intro hcop
4. have hgb : exists d. ((((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w) /\ exists xp yp xn yn. a * xp + b * yp = d + (a * xn + b * yn))
5. apply gcd_balanced_bezout_exists
6. cases hgb
7. cases hgb_witness
8. cases hgb_witness_left
9. cases hgb_witness_left_left
10. have hd : x = 1
11. specialize hcop x
12. apply hcop
13. exact hgb_witness_left_left_left
14. exact hgb_witness_left_left_right
15. cases hgb_witness_right
16. cases hgb_witness_right_witness
17. cases hgb_witness_right_witness_witness
18. cases hgb_witness_right_witness_witness_witness
19. exists x1
20. exists x2
21. exists x3
22. exists x4
23. rewrite hd at hgb_witness_right_witness_witness_witness_witness
24. exact hgb_witness_right_witness_witness_witness_witness

forall a b z. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> (exists q. b * z = a * q) -> exists w. z = a * w

1. intro a
2. intro b
3. intro z
4. intro hcop
5. intro hdiv
6. have hbez : exists xp yp xn yn. a * xp + b * yp = 1 + (a * xn + b * yn)
7. apply coprime_balanced_bezout
8. exact hcop
9. cases hbez
10. cases hbez_witness
11. cases hbez_witness_witness
12. cases hbez_witness_witness_witness
13. have hscaled : a * (x * z) + (b * z) * x1 = 1 * z + (a * (x2 * z) + (b * z) * x3)
14. apply balanced_combination_scale_right
15. exact hbez_witness_witness_witness_witness
16. specialize one_mul z
17. rewrite one_mul at hscaled
18. specialize common_divisor_divides_balanced_result a
19. specialize common_divisor_divides_balanced_result a
20. specialize common_divisor_divides_balanced_result (b * z)
21. specialize common_divisor_divides_balanced_result z
22. specialize common_divisor_divides_balanced_result (x * z)
23. specialize common_divisor_divides_balanced_result x1
24. specialize common_divisor_divides_balanced_result (x2 * z)
25. specialize common_divisor_divides_balanced_result x3
26. apply common_divisor_divides_balanced_result
27. specialize multiple_refl a
28. exact multiple_refl
29. exact hdiv
30. exact hscaled

forall a b. a = b \/ ~(a = b)

1. intro a
2. induction a
3. intro b
4. induction b
5. left
6. refl
7. right
8. intro h
9. apply PA1
10. symm
11. exact h
12. intro b
13. induction b
14. right
15. intro h
16. apply PA1
17. exact h
18. specialize IH b
19. cases IH
20. left
21. congr
22. exact IH_left
23. right
24. intro h
25. apply IH_right
26. apply PA2
27. exact h

forall p. (~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) -> ~(p = 0)

1. intro p
2. intro hp
3. intro hp0
4. cases hp
5. specialize hp_right 0
6. specialize hp_right 0
7. have hunit : 0 = 1 \/ 0 = 1
8. apply hp_right
9. rewrite hp0
10. symm
11. apply mul_zero_left
12. cases hunit
13. specialize succ_ne_zero 0
14. apply succ_ne_zero
15. symm
16. exact hunit_left
17. specialize succ_ne_zero 0
18. apply succ_ne_zero
19. symm
20. exact hunit_right

forall p g. (~(p = 1) /\ forall c d. p = c * d -> c = 1 \/ d = 1) -> (exists x. p = g * x) -> g = 1 \/ p = g

1. intro p
2. intro g
3. intro hp
4. intro hdiv
5. cases hp
6. cases hdiv
7. specialize hp_right g
8. specialize hp_right x
9. have hfactor : g = 1 \/ x = 1
10. apply hp_right
11. exact hdiv_witness
12. cases hfactor
13. left
14. exact hfactor_left
15. right
16. trans g * x
17. exact hdiv_witness
18. rewrite hfactor_right
19. apply mul_one

forall m a. exists u v. a + m * u = a + m * v

1. intro m
2. intro a
3. exists 0
4. exists 0
5. refl

forall m a b. (exists u v. a + m * u = b + m * v) -> exists r s. b + m * r = a + m * s

1. intro m
2. intro a
3. intro b
4. intro h
5. cases h
6. cases h_witness
7. exists x1
8. exists x
9. symm
10. exact h_witness_witness

forall m a b c. (exists u v. a + m * u = b + m * v) -> (exists r s. b + m * r = c + m * s) -> exists x y. a + m * x = c + m * y

1. intro m
2. intro a
3. intro b
4. intro c
5. intro hab
6. intro hbc
7. cases hab
8. cases hab_witness
9. cases hbc
10. cases hbc_witness
11. exists x + x2
12. exists x3 + x1
13. trans a + (m * x + m * x2)
14. congr
15. refl
16. apply mul_add
17. trans (a + m * x) + m * x2
18. symm
19. apply add_assoc
20. trans (b + m * x1) + m * x2
21. congr
22. exact hab_witness_witness
23. refl
24. trans b + (m * x1 + m * x2)
25. apply add_assoc
26. trans b + (m * x2 + m * x1)
27. congr
28. refl
29. apply add_comm
30. trans (b + m * x2) + m * x1
31. symm
32. apply add_assoc
33. trans (c + m * x3) + m * x1
34. congr
35. exact hbc_witness_witness
36. refl
37. trans c + (m * x3 + m * x1)
38. apply add_assoc
39. congr
40. refl
41. symm
42. apply mul_add

forall m a b c d. (exists u v. a + m * u = b + m * v) -> (exists r s. c + m * r = d + m * s) -> exists x y. (a + c) + m * x = (b + d) + m * y

1. intro m
2. intro a
3. intro b
4. intro c
5. intro d
6. intro hab
7. intro hcd
8. cases hab
9. cases hab_witness
10. cases hcd
11. cases hcd_witness
12. exists x2 + x
13. exists x3 + x1
14. trans (a + c) + (m * x2 + m * x)
15. congr
16. refl
17. apply mul_add
18. trans (m * x2 + c) + (a + m * x)
19. apply add_permute_outer
20. trans (c + m * x2) + (a + m * x)
21. congr
22. apply add_comm
23. refl
24. trans (a + m * x) + (c + m * x2)
25. apply add_comm
26. trans (b + m * x1) + (d + m * x3)
27. congr
28. exact hab_witness_witness
29. exact hcd_witness_witness
30. trans (d + m * x3) + (b + m * x1)
31. apply add_comm
32. trans (m * x3 + d) + (b + m * x1)
33. congr
34. apply add_comm
35. refl
36. trans (b + d) + (m * x3 + m * x1)
37. symm
38. apply add_permute_outer
39. congr
40. refl
41. symm
42. apply mul_add

forall m a b c. (exists u v. a + m * u = b + m * v) -> exists r s. (a * c) + m * r = (b * c) + m * s

1. intro m
2. intro a
3. intro b
4. intro c
5. intro h
6. cases h
7. cases h_witness
8. exists x * c
9. exists x1 * c
10. trans a * c + (m * x) * c
11. congr
12. refl
13. symm
14. apply mul_assoc
15. trans (a + m * x) * c
16. symm
17. apply add_mul
18. trans (b + m * x1) * c
19. congr
20. exact h_witness_witness
21. refl
22. trans b * c + (m * x1) * c
23. apply add_mul
24. congr
25. refl
26. apply mul_assoc

forall m a b c. (exists u v. a + m * u = b + m * v) -> exists r s. (c * a) + m * r = (c * b) + m * s

1. intro m
2. intro a
3. intro b
4. intro c
5. intro h
6. specialize mod_eq_mul_right m
7. specialize mod_eq_mul_right a
8. specialize mod_eq_mul_right b
9. specialize mod_eq_mul_right c
10. have hr : exists r s. (a * c) + m * r = (b * c) + m * s
11. apply mod_eq_mul_right
12. exact h
13. cases hr
14. cases hr_witness
15. exists x
16. exists x1
17. trans a * c + m * x
18. congr
19. apply mul_comm
20. refl
21. trans b * c + m * x1
22. exact hr_witness_witness
23. congr
24. apply mul_comm
25. refl

forall m a b c d. (exists u v. a + m * u = b + m * v) -> (exists r s. c + m * r = d + m * s) -> exists x y. (a * c) + m * x = (b * d) + m * y

1. intro m
2. intro a
3. intro b
4. intro c
5. intro d
6. intro hab
7. intro hcd
8. have hacbc : exists r s. (a * c) + m * r = (b * c) + m * s
9. specialize mod_eq_mul_right m
10. specialize mod_eq_mul_right a
11. specialize mod_eq_mul_right b
12. specialize mod_eq_mul_right c
13. apply mod_eq_mul_right
14. exact hab
15. have hbcbd : exists r s. (b * c) + m * r = (b * d) + m * s
16. specialize mod_eq_mul_left m
17. specialize mod_eq_mul_left c
18. specialize mod_eq_mul_left d
19. specialize mod_eq_mul_left b
20. apply mod_eq_mul_left
21. exact hcd
22. specialize mod_eq_trans m
23. specialize mod_eq_trans (a * c)
24. specialize mod_eq_trans (b * c)
25. specialize mod_eq_trans (b * d)
26. apply mod_eq_trans
27. exact hacbc
28. exact hbcbd

forall m b q x. b = q * m + x -> exists u v. b + m * u = x + m * v

1. intro m
2. intro b
3. intro q
4. intro x
5. intro h
6. exists 0
7. exists q
8. rewrite PA5
9. rewrite PA3
10. trans q * m + x
11. exact h
12. trans x + q * m
13. apply add_comm
14. congr
15. refl
16. apply mul_comm

forall m a b. (exists ha. ha + S a = m) -> (exists hb. hb + S b = m) -> (exists u v. a + m * u = b + m * v) -> a = b

1. intro m
2. intro a
3. intro b
4. intro ha
5. intro hb
6. intro hab
7. cases hab
8. cases hab_witness
9. have hda : a + m * x = m * x + a
10. apply add_comm
11. have hdb : a + m * x = m * x1 + b
12. trans b + m * x1
13. exact hab_witness_witness
14. apply add_comm
15. specialize division_remainder_unique m
16. specialize division_remainder_unique (a + m * x)
17. specialize division_remainder_unique x
18. specialize division_remainder_unique a
19. specialize division_remainder_unique x1
20. specialize division_remainder_unique b
21. have huniq : x = x1 /\ a = b
22. apply division_remainder_unique
23. exact hda
24. exact ha
25. exact hdb
26. exact hb
27. cases huniq
28. exact huniq_right

forall m b x. ~(m = 0) -> (exists h. h + S x = m) -> (exists u v. b + m * u = x + m * v) -> exists q. b = q * m + x

1. intro m
2. intro b
3. intro x
4. intro hm
5. intro hx
6. intro hbx
7. have hdiv : exists q r. b = m * q + r /\ exists h. h + S r = m
8. specialize division_remainder_exists m
9. specialize division_remainder_exists b
10. apply division_remainder_exists
11. exact hm
12. cases hdiv
13. cases hdiv_witness
14. cases hdiv_witness_witness
15. have hremb : exists u v. x2 + m * u = b + m * v
16. exists x1
17. exists 0
18. trans m * x1 + x2
19. apply add_comm
20. trans b
21. symm
22. exact hdiv_witness_witness_left
23. symm
24. rewrite PA5
25. apply PA3
26. have hremx : exists u v. x2 + m * u = x + m * v
27. specialize mod_eq_trans m
28. specialize mod_eq_trans x2
29. specialize mod_eq_trans b
30. specialize mod_eq_trans x
31. apply mod_eq_trans
32. exact hremb
33. exact hbx
34. have hrx : x2 = x
35. specialize mod_eq_bounded_unique m
36. specialize mod_eq_bounded_unique x2
37. specialize mod_eq_bounded_unique x
38. apply mod_eq_bounded_unique
39. exact hdiv_witness_witness_right
40. exact hx
41. exact hremx
42. exists x1
43. trans m * x1 + x2
44. exact hdiv_witness_witness_left
45. trans x1 * m + x2
46. congr
47. apply mul_comm
48. refl
49. congr
50. refl
51. exact hrx

forall c i. ~(S ((S i) * c) = 0)

1. intro c
2. intro i
3. specialize succ_ne_zero ((S i) * c)
4. exact succ_ne_zero

forall c i x. (exists h. h + S x = S ((S i) * c)) -> ((exists h. h + S x = S ((S i) * c)) /\ exists q. x = q * S ((S i) * c) + x)

1. intro c
2. intro i
3. intro x
4. intro hx
5. split
6. exact hx
7. exists 0
8. specialize mul_zero_left (S ((S i) * c))
9. rewrite mul_zero_left
10. specialize zero_add x
11. rewrite zero_add
12. refl

forall b c i. exists x. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x)

1. intro b
2. intro c
3. intro i
4. have hm0 : ~(S ((S i) * c) = 0)
5. specialize beta_modulus_nonzero c
6. specialize beta_modulus_nonzero i
7. exact beta_modulus_nonzero
8. specialize division_remainder_exists (S ((S i) * c))
9. specialize division_remainder_exists b
10. have hdiv : exists q r. b = S ((S i) * c) * q + r /\ exists h. h + S r = S ((S i) * c)
11. apply division_remainder_exists
12. exact hm0
13. cases hdiv
14. cases hdiv_witness
15. cases hdiv_witness_witness
16. exists x1
17. split
18. exact hdiv_witness_witness_right
19. exists x
20. trans S ((S i) * c) * x + x1
21. exact hdiv_witness_witness_left
22. congr
23. apply mul_comm
24. refl

forall b c i x y. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y) -> x = y

1. intro b
2. intro c
3. intro i
4. intro x
5. intro y
6. intro hx
7. intro hy
8. cases hx
9. cases hy
10. cases hx_right
11. cases hy_right
12. have hdx : b = S ((S i) * c) * x1 + x
13. trans x1 * S ((S i) * c) + x
14. exact hx_right_witness
15. congr
16. apply mul_comm
17. refl
18. have hdy : b = S ((S i) * c) * x2 + y
19. trans x2 * S ((S i) * c) + y
20. exact hy_right_witness
21. congr
22. apply mul_comm
23. refl
24. specialize division_remainder_unique (S ((S i) * c))
25. specialize division_remainder_unique b
26. specialize division_remainder_unique x1
27. specialize division_remainder_unique x
28. specialize division_remainder_unique x2
29. specialize division_remainder_unique y
30. have huniq : x1 = x2 /\ x = y
31. apply division_remainder_unique
32. exact hdx
33. exact hx_left
34. exact hdy
35. exact hy_left
36. cases huniq
37. exact huniq_right

forall b c i x. (exists h. h + S x = S ((S i) * c)) -> (exists u v. b + S ((S i) * c) * u = x + S ((S i) * c) * v) -> ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x)

1. intro b
2. intro c
3. intro i
4. intro x
5. intro hx
6. intro hmod
7. split
8. exact hx
9. specialize mod_eq_to_remainder_decomposition (S ((S i) * c))
10. specialize mod_eq_to_remainder_decomposition b
11. specialize mod_eq_to_remainder_decomposition x
12. apply mod_eq_to_remainder_decomposition
13. specialize beta_modulus_nonzero c
14. specialize beta_modulus_nonzero i
15. exact beta_modulus_nonzero
16. exact hx
17. exact hmod

forall m a. (exists k. a = m * k) -> exists u v. a + m * u = 0 + m * v

1. intro m
2. intro a
3. intro h
4. cases h
5. exists 0
6. exists x
7. rewrite h_witness
8. simp [zero_add]

forall m n xp yp xn yn. m * xp + n * yp = 1 + (m * xn + n * yn) -> exists u v. n * yp + m * u = (1 + n * yn) + m * v

1. intro m
2. intro n
3. intro xp
4. intro yp
5. intro xn
6. intro yn
7. intro h
8. exists xp
9. exists xn
10. trans m * xp + n * yp
11. apply add_comm
12. trans 1 + (m * xn + n * yn)
13. exact h
14. trans 1 + (n * yn + m * xn)
15. congr
16. refl
17. apply add_comm
18. symm
19. apply add_assoc

forall m n xp yp xn yn. m * xp + n * yp = 1 + (m * xn + n * yn) -> exists u v. m * xp + n * u = (1 + m * xn) + n * v

1. intro m
2. intro n
3. intro xp
4. intro yp
5. intro xn
6. intro yn
7. intro h
8. exists yp
9. exists yn
10. trans 1 + (m * xn + n * yn)
11. exact h
12. symm
13. apply add_assoc

forall k a z. exists u v. ((a + z) + k * z) + S k * u = a + S k * v

1. intro k
2. intro a
3. intro z
4. exists 0
5. exists z
6. rewrite PA5
7. rewrite PA3
8. specialize mul_succ_left k
9. specialize mul_succ_left z
10. rewrite mul_succ_left
11. trans a + (z + k * z)
12. apply add_assoc
13. congr
14. refl
15. apply add_comm

forall m n a b. ~(m = 0) -> ~(n = 0) -> (forall d. (exists u. m = d * u) -> (exists v. n = d * v) -> d = 1) -> exists x. (exists u v. x + m * u = a + m * v) /\ (exists r s. x + n * r = b + n * s)

1. intro m
2. intro n
3. intro a
4. intro b
5. intro hm
6. intro hn
7. intro hcop
8. have hms : exists k. m = S k
9. specialize nonzero_is_succ m
10. apply nonzero_is_succ
11. exact hm
12. have hns : exists k. n = S k
13. specialize nonzero_is_succ n
14. apply nonzero_is_succ
15. exact hn
16. have hbez : exists xp yp xn yn. m * xp + n * yp = 1 + (m * xn + n * yn)
17. specialize coprime_balanced_bezout m
18. specialize coprime_balanced_bezout n
19. apply coprime_balanced_bezout
20. exact hcop
21. cases hms
22. cases hns
23. cases hbez
24. cases hbez_witness
25. cases hbez_witness_witness
26. cases hbez_witness_witness_witness
27. have hbl : exists u v. n * x3 + m * u = (1 + n * x5) + m * v
28. specialize bezout_mod_left m
29. specialize bezout_mod_left n
30. specialize bezout_mod_left x2
31. specialize bezout_mod_left x3
32. specialize bezout_mod_left x4
33. specialize bezout_mod_left x5
34. apply bezout_mod_left
35. exact hbez_witness_witness_witness_witness
36. have hbr : exists u v. m * x2 + n * u = (1 + m * x4) + n * v
37. specialize bezout_mod_right m
38. specialize bezout_mod_right n
39. specialize bezout_mod_right x2
40. specialize bezout_mod_right x3
41. specialize bezout_mod_right x4
42. specialize bezout_mod_right x5
43. apply bezout_mod_right
44. exact hbez_witness_witness_witness_witness
45. have hal0 : exists u v. (a * (n * x3)) + m * u = (a * (1 + n * x5)) + m * v
46. specialize mod_eq_mul_left m
47. specialize mod_eq_mul_left (n * x3)
48. specialize mod_eq_mul_left (1 + n * x5)
49. specialize mod_eq_mul_left a
50. apply mod_eq_mul_left
51. exact hbl
52. have hal : exists u v. (a * (n * x3)) + m * u = (a + a * (n * x5)) + m * v
53. have haexpand : a * (1 + n * x5) = a + a * (n * x5)
54. trans a * 1 + a * (n * x5)
55. apply mul_add
56. congr
57. apply mul_one
58. refl
59. rewrite <- haexpand
60. exact hal0
61. have hbm : exists u v. (b * (m * x2)) + m * u = 0 + m * v
62. apply dvd_to_mod_zero
63. exists b * x2
64. trans (b * m) * x2
65. symm
66. apply mul_assoc
67. trans (m * b) * x2
68. congr
69. apply mul_comm
70. refl
71. apply mul_assoc
72. have hym : exists u v. ((a * (n * x3)) + (b * (m * x2))) + m * u = ((a + a * (n * x5)) + 0) + m * v
73. specialize mod_eq_add m
74. specialize mod_eq_add (a * (n * x3))
75. specialize mod_eq_add (a + a * (n * x5))
76. specialize mod_eq_add (b * (m * x2))
77. specialize mod_eq_add 0
78. apply mod_eq_add
79. exact hal
80. exact hbm
81. have hym_norm : exists u v. ((a * (n * x3)) + (b * (m * x2))) + m * u = (a + a * (n * x5)) + m * v
82. have hym_zero : (a + a * (n * x5)) + 0 = a + a * (n * x5)
83. rewrite PA3
84. refl
85. rewrite <- hym_zero
86. exact hym
87. have hkm : exists u v. (x * (a * (n * x5))) + m * u = (x * (a * (n * x5))) + m * v
88. specialize mod_eq_refl m
89. specialize mod_eq_refl (x * (a * (n * x5)))
90. apply mod_eq_refl
91. have hymk : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + m * u = ((a + a * (n * x5)) + (x * (a * (n * x5)))) + m * v
92. specialize mod_eq_add m
93. specialize mod_eq_add ((a * (n * x3)) + (b * (m * x2)))
94. specialize mod_eq_add (a + a * (n * x5))
95. specialize mod_eq_add (x * (a * (n * x5)))
96. specialize mod_eq_add (x * (a * (n * x5)))
97. apply mod_eq_add
98. exact hym_norm
99. exact hkm
100. have hcancelm : exists u v. ((a + a * (n * x5)) + x * (a * (n * x5))) + S x * u = a + S x * v
101. specialize mod_eq_predecessor_cancel x
102. specialize mod_eq_predecessor_cancel a
103. specialize mod_eq_predecessor_cancel (a * (n * x5))
104. apply mod_eq_predecessor_cancel
105. rewrite <- hms_witness at hcancelm
106. rewrite <- hms_witness at hcancelm
107. have hbasem : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + m * u = a + m * v
108. specialize mod_eq_trans m
109. specialize mod_eq_trans (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
110. specialize mod_eq_trans ((a + a * (n * x5)) + (x * (a * (n * x5))))
111. specialize mod_eq_trans a
112. apply mod_eq_trans
113. exact hymk
114. exact hcancelm
115. have hknznm : exists u v. (x1 * (b * (m * x4))) + m * u = 0 + m * v
116. apply dvd_to_mod_zero
117. exists x1 * (b * x4)
118. trans x1 * ((b * m) * x4)
119. congr
120. refl
121. symm
122. apply mul_assoc
123. trans x1 * ((m * b) * x4)
124. congr
125. refl
126. congr
127. apply mul_comm
128. refl
129. trans x1 * (m * (b * x4))
130. congr
131. refl
132. apply mul_assoc
133. trans (x1 * m) * (b * x4)
134. symm
135. apply mul_assoc
136. trans (m * x1) * (b * x4)
137. congr
138. apply mul_comm
139. refl
140. apply mul_assoc
141. have hfinalm0 : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + m * u = (a + 0) + m * v
142. specialize mod_eq_add m
143. specialize mod_eq_add (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
144. specialize mod_eq_add a
145. specialize mod_eq_add (x1 * (b * (m * x4)))
146. specialize mod_eq_add 0
147. apply mod_eq_add
148. exact hbasem
149. exact hknznm
150. have hazerom : exists u v. (a + 0) + m * u = a + m * v
151. exists 0
152. exists 0
153. simp
154. have hfinalm : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + m * u = a + m * v
155. specialize mod_eq_trans m
156. specialize mod_eq_trans ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4))))
157. specialize mod_eq_trans (a + 0)
158. specialize mod_eq_trans a
159. apply mod_eq_trans
160. exact hfinalm0
161. exact hazerom
162. have hbn0 : exists u v. (b * (m * x2)) + n * u = (b * (1 + m * x4)) + n * v
163. specialize mod_eq_mul_left n
164. specialize mod_eq_mul_left (m * x2)
165. specialize mod_eq_mul_left (1 + m * x4)
166. specialize mod_eq_mul_left b
167. apply mod_eq_mul_left
168. exact hbr
169. have hbn : exists u v. (b * (m * x2)) + n * u = (b + b * (m * x4)) + n * v
170. have hbexpand : b * (1 + m * x4) = b + b * (m * x4)
171. trans b * 1 + b * (m * x4)
172. apply mul_add
173. congr
174. apply mul_one
175. refl
176. rewrite <- hbexpand
177. exact hbn0
178. have han : exists u v. (a * (n * x3)) + n * u = 0 + n * v
179. apply dvd_to_mod_zero
180. exists a * x3
181. trans (a * n) * x3
182. symm
183. apply mul_assoc
184. trans (n * a) * x3
185. congr
186. apply mul_comm
187. refl
188. apply mul_assoc
189. have hyn0 : exists u v. ((a * (n * x3)) + (b * (m * x2))) + n * u = (0 + (b + b * (m * x4))) + n * v
190. specialize mod_eq_add n
191. specialize mod_eq_add (a * (n * x3))
192. specialize mod_eq_add 0
193. specialize mod_eq_add (b * (m * x2))
194. specialize mod_eq_add (b + b * (m * x4))
195. apply mod_eq_add
196. exact han
197. exact hbn
198. have hyn_norm : exists u v. ((a * (n * x3)) + (b * (m * x2))) + n * u = (b + b * (m * x4)) + n * v
199. have hyn_zero : 0 + (b + b * (m * x4)) = b + b * (m * x4)
200. specialize zero_add (b + b * (m * x4))
201. exact zero_add
202. rewrite <- hyn_zero
203. exact hyn0
204. have hkmz : exists u v. (x * (a * (n * x5))) + n * u = 0 + n * v
205. apply dvd_to_mod_zero
206. exists x * (a * x5)
207. trans x * ((a * n) * x5)
208. congr
209. refl
210. symm
211. apply mul_assoc
212. trans x * ((n * a) * x5)
213. congr
214. refl
215. congr
216. apply mul_comm
217. refl
218. trans x * (n * (a * x5))
219. congr
220. refl
221. apply mul_assoc
222. trans (x * n) * (a * x5)
223. symm
224. apply mul_assoc
225. trans (n * x) * (a * x5)
226. congr
227. apply mul_comm
228. refl
229. apply mul_assoc
230. have hyn1 : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + n * u = ((b + b * (m * x4)) + 0) + n * v
231. specialize mod_eq_add n
232. specialize mod_eq_add ((a * (n * x3)) + (b * (m * x2)))
233. specialize mod_eq_add (b + b * (m * x4))
234. specialize mod_eq_add (x * (a * (n * x5)))
235. specialize mod_eq_add 0
236. apply mod_eq_add
237. exact hyn_norm
238. exact hkmz
239. have hyn1_norm : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + n * u = (b + b * (m * x4)) + n * v
240. have hyn1_zero : (b + b * (m * x4)) + 0 = b + b * (m * x4)
241. rewrite PA3
242. refl
243. rewrite <- hyn1_zero
244. exact hyn1
245. have hkn : exists u v. (x1 * (b * (m * x4))) + n * u = (x1 * (b * (m * x4))) + n * v
246. specialize mod_eq_refl n
247. specialize mod_eq_refl (x1 * (b * (m * x4)))
248. apply mod_eq_refl
249. have hynk : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + n * u = ((b + b * (m * x4)) + (x1 * (b * (m * x4)))) + n * v
250. specialize mod_eq_add n
251. specialize mod_eq_add (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
252. specialize mod_eq_add (b + b * (m * x4))
253. specialize mod_eq_add (x1 * (b * (m * x4)))
254. specialize mod_eq_add (x1 * (b * (m * x4)))
255. apply mod_eq_add
256. exact hyn1_norm
257. exact hkn
258. have hcanceln : exists u v. ((b + b * (m * x4)) + x1 * (b * (m * x4))) + S x1 * u = b + S x1 * v
259. specialize mod_eq_predecessor_cancel x1
260. specialize mod_eq_predecessor_cancel b
261. specialize mod_eq_predecessor_cancel (b * (m * x4))
262. apply mod_eq_predecessor_cancel
263. rewrite <- hns_witness at hcanceln
264. rewrite <- hns_witness at hcanceln
265. have hfinaln : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + n * u = b + n * v
266. specialize mod_eq_trans n
267. specialize mod_eq_trans ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4))))
268. specialize mod_eq_trans ((b + b * (m * x4)) + (x1 * (b * (m * x4))))
269. specialize mod_eq_trans b
270. apply mod_eq_trans
271. exact hynk
272. exact hcanceln
273. exists (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))
274. split
275. exact hfinalm
276. exact hfinaln

forall c k d. (exists u. S (k * c) = d * u) -> (exists v. c = d * v) -> d = 1

1. intro c
2. intro k
3. intro d
4. intro hm
5. intro hc
6. have hstep : S (k * c) = c * k + 1
7. simp [mul_comm]
8. have h1 : exists w. 1 = d * w
9. specialize divides_remainder d
10. specialize divides_remainder (S (k * c))
11. specialize divides_remainder c
12. specialize divides_remainder k
13. specialize divides_remainder 1
14. apply divides_remainder
15. exact hm
16. exact hc
17. exact hstep
18. specialize divisor_one d
19. apply divisor_one
20. exact h1

forall c i j gap d. j = i + gap -> (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> exists w. gap * c = d * w

1. intro c
2. intro i
3. intro j
4. intro gap
5. intro d
6. intro hij
7. intro hmi
8. intro hmj
9. have hstep : S ((S j) * c) = S ((S i) * c) * 1 + gap * c
10. rewrite hij
11. specialize add_succ_left i
12. specialize add_succ_left gap
13. rewrite <- add_succ_left
14. simp [add_mul, zero_add]
15. symm
16. specialize add_succ_left_before (S i * c)
17. specialize add_succ_left_before (gap * c)
18. exact add_succ_left_before
19. specialize divides_remainder d
20. specialize divides_remainder (S ((S j) * c))
21. specialize divides_remainder (S ((S i) * c))
22. specialize divides_remainder 1
23. specialize divides_remainder (gap * c)
24. apply divides_remainder
25. exact hmj
26. exact hmi
27. exact hstep

forall c i j gap. j = i + gap -> (exists k. c = gap * k) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1

1. intro c
2. intro i
3. intro j
4. intro gap
5. intro hij
6. intro hgapc
7. intro d
8. intro hmi
9. intro hmj
10. have hcopdc : forall e. (exists u. d = e * u) -> (exists v. c = e * v) -> e = 1
11. intro e
12. intro hed
13. intro hec
14. have hmei : exists u. S ((S i) * c) = e * u
15. specialize multiple_trans d
16. specialize multiple_trans e
17. specialize multiple_trans (S ((S i) * c))
18. apply multiple_trans
19. exact hmi
20. exact hed
21. specialize beta_modulus_coprime_base c
22. specialize beta_modulus_coprime_base (S i)
23. specialize beta_modulus_coprime_base e
24. apply beta_modulus_coprime_base
25. exact hmei
26. exact hec
27. have hgapprod : exists w. gap * c = d * w
28. specialize common_divisor_beta_moduli_divides_gap_times_c c
29. specialize common_divisor_beta_moduli_divides_gap_times_c i
30. specialize common_divisor_beta_moduli_divides_gap_times_c j
31. specialize common_divisor_beta_moduli_divides_gap_times_c gap
32. specialize common_divisor_beta_moduli_divides_gap_times_c d
33. apply common_divisor_beta_moduli_divides_gap_times_c
34. exact hij
35. exact hmi
36. exact hmj
37. cases hgapprod
38. have hdivgap : exists w. gap = d * w
39. specialize gauss_coprime_cancel d
40. specialize gauss_coprime_cancel c
41. specialize gauss_coprime_cancel gap
42. apply gauss_coprime_cancel
43. exact hcopdc
44. exists x
45. trans gap * c
46. apply mul_comm
47. exact hgapprod_witness
48. have hdc : exists w. c = d * w
49. specialize multiple_trans gap
50. specialize multiple_trans d
51. specialize multiple_trans c
52. apply multiple_trans
53. exact hgapc
54. exact hdivgap
55. specialize hcopdc d
56. apply hcopdc
57. specialize multiple_refl d
58. exact multiple_refl
59. exact hdc

forall B c. ~(c = 0) -> (forall t. (exists h. S t + S h = S B) -> exists k. c = S t * k) -> exists c2. (~(c2 = 0) /\ forall t. (exists h. S t + S h = S (S B)) -> exists k. c2 = S t * k)

1. intro B
2. intro c
3. intro hc
4. intro hall
5. exists c * S B
6. split
7. have hSB : ~(S B = 0)
8. specialize succ_ne_zero B
9. exact succ_ne_zero
10. have hprod : ~(c * S B = 0)
11. intro hzero
12. have hz : c = 0 \/ S B = 0
13. specialize mul_eq_zero c
14. specialize mul_eq_zero (S B)
15. apply mul_eq_zero
16. exact hzero
17. cases hz
18. apply hc
19. exact hz_left
20. apply hSB
21. exact hz_right
22. exact hprod
23. intro t
24. intro ht
25. cases ht
26. specialize zero_or_succ x
27. cases zero_or_succ
28. rewrite zero_or_succ_left at ht_witness
29. have hteq : S t = S B
30. rewrite PA4 at ht_witness
31. rewrite PA3 at ht_witness
32. apply PA2
33. exact ht_witness
34. exists c
35. rewrite hteq
36. apply mul_comm
37. cases zero_or_succ_right
38. have hprev : exists h. S t + S h = S B
39. exists x1
40. rewrite zero_or_succ_right_witness at ht_witness
41. rewrite PA4 at ht_witness
42. apply PA2
43. exact ht_witness
44. have hdivc : exists k. c = S t * k
45. specialize hall t
46. apply hall
47. exact hprev
48. specialize multiple_mul_right (S t)
49. specialize multiple_mul_right c
50. specialize multiple_mul_right (S B)
51. apply multiple_mul_right
52. exact hdivc

forall B. exists c. (~(c = 0) /\ forall t. (exists h. S t + S h = S B) -> exists k. c = S t * k)

1. intro B
2. induction B
3. exists 1
4. split
5. specialize succ_ne_zero 0
6. exact succ_ne_zero
7. intro t
8. intro ht
9. cases ht
10. exfalso
11. have hz : S t + x = 0
12. rewrite PA4 at ht_witness
13. apply PA2
14. exact ht_witness
15. have hst0 : S t = 0
16. specialize add_eq_zero_left (S t)
17. specialize add_eq_zero_left x
18. apply add_eq_zero_left
19. exact hz
20. specialize succ_ne_zero t
21. apply succ_ne_zero
22. exact hst0
23. cases IH
24. cases IH_witness
25. specialize bounded_common_multiple_step B
26. specialize bounded_common_multiple_step x
27. apply bounded_common_multiple_step
28. exact IH_witness_left
29. exact IH_witness_right

forall B c i j. (forall t. (exists h. S t + S h = S B) -> exists k. c = S t * k) -> (exists g. g + S i = j) -> (exists h. h + j = B) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1

1. intro B
2. intro c
3. intro i
4. intro j
5. intro hcm
6. intro hlt
7. intro hjB
8. intro d
9. intro hdi
10. intro hdj
11. cases hlt
12. have hij : j = i + S x
13. symm
14. trans x + S i
15. simp [add_comm]
16. exact hlt_witness
17. have hgaple : exists r. r + S x = B
18. specialize le_trans (S x)
19. specialize le_trans j
20. specialize le_trans B
21. apply le_trans
22. exists i
23. symm
24. exact hij
25. exact hjB
26. cases hgaple
27. have hgapbound : exists h. S x + S h = S B
28. exists x1
29. rewrite PA4
30. congr
31. trans x1 + S x
32. apply add_comm
33. exact hgaple_witness
34. have hgapdvd : exists k. c = S x * k
35. specialize hcm x
36. apply hcm
37. exact hgapbound
38. have hcop : forall e. (exists u. S ((S i) * c) = e * u) -> (exists v. S ((S j) * c) = e * v) -> e = 1
39. specialize beta_moduli_coprime_of_gap_dvd c
40. specialize beta_moduli_coprime_of_gap_dvd i
41. specialize beta_moduli_coprime_of_gap_dvd j
42. specialize beta_moduli_coprime_of_gap_dvd (S x)
43. apply beta_moduli_coprime_of_gap_dvd
44. exact hij
45. exact hgapdvd
46. specialize hcop d
47. apply hcop
48. exact hdi
49. exact hdj

forall B c. (forall t. (exists h. S t + S h = S B) -> exists k. c = S t * k) -> forall i j. ~(i = j) -> (exists hi. hi + i = B) -> (exists hj. hj + j = B) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1

1. intro B
2. intro c
3. intro hcm
4. intro i
5. intro j
6. intro hne
7. intro hiB
8. intro hjB
9. intro d
10. intro hdi
11. intro hdj
12. specialize lt_trichotomy i
13. specialize lt_trichotomy j
14. cases lt_trichotomy
15. exfalso
16. apply hne
17. exact lt_trichotomy_left
18. cases lt_trichotomy_right
19. have hcopij : forall e. (exists u. S ((S i) * c) = e * u) -> (exists v. S ((S j) * c) = e * v) -> e = 1
20. specialize beta_moduli_coprime_of_lt_bounded_common_multiple B
21. specialize beta_moduli_coprime_of_lt_bounded_common_multiple c
22. specialize beta_moduli_coprime_of_lt_bounded_common_multiple i
23. specialize beta_moduli_coprime_of_lt_bounded_common_multiple j
24. apply beta_moduli_coprime_of_lt_bounded_common_multiple
25. exact hcm
26. exact lt_trichotomy_right_left
27. exact hjB
28. specialize hcopij d
29. apply hcopij
30. exact hdi
31. exact hdj
32. have hcopji : forall e. (exists u. S ((S j) * c) = e * u) -> (exists v. S ((S i) * c) = e * v) -> e = 1
33. specialize beta_moduli_coprime_of_lt_bounded_common_multiple B
34. specialize beta_moduli_coprime_of_lt_bounded_common_multiple c
35. specialize beta_moduli_coprime_of_lt_bounded_common_multiple j
36. specialize beta_moduli_coprime_of_lt_bounded_common_multiple i
37. apply beta_moduli_coprime_of_lt_bounded_common_multiple
38. exact hcm
39. exact lt_trichotomy_right_right
40. exact hiB
41. specialize hcopji d
42. apply hcopji
43. exact hdj
44. exact hdi

forall a b n. (forall d. (exists x. a = d * x) -> (exists y. n = d * y) -> d = 1) -> (forall d. (exists x. b = d * x) -> (exists y. n = d * y) -> d = 1) -> forall d. (exists x. a * b = d * x) -> (exists y. n = d * y) -> d = 1

1. intro a
2. intro b
3. intro n
4. intro han
5. intro hbn
6. intro d
7. intro hab
8. intro hdn
9. have hda : forall e. (exists u. d = e * u) -> (exists v. a = e * v) -> e = 1
10. intro e
11. intro hed
12. intro hea
13. have hen : exists q. n = e * q
14. specialize multiple_trans d
15. specialize multiple_trans e
16. specialize multiple_trans n
17. apply multiple_trans
18. exact hdn
19. exact hed
20. specialize han e
21. apply han
22. exact hea
23. exact hen
24. have hdb : exists w. b = d * w
25. specialize gauss_coprime_cancel d
26. specialize gauss_coprime_cancel a
27. specialize gauss_coprime_cancel b
28. apply gauss_coprime_cancel
29. exact hda
30. exact hab
31. specialize hbn d
32. apply hbn
33. exact hdb
34. exact hdn

forall m P x a. (exists k. P = m * k) -> (exists u v. x + P * u = a + P * v) -> exists r s. x + m * r = a + m * s

1. intro m
2. intro P
3. intro x
4. intro a
5. intro hdiv
6. intro hmod
7. cases hdiv
8. cases hmod
9. cases hmod_witness
10. rewrite hdiv_witness at hmod_witness_witness
11. rewrite hdiv_witness at hmod_witness_witness
12. exists x1 * x2
13. exists x1 * x3
14. trans x + (m * x1) * x2
15. congr
16. refl
17. symm
18. apply mul_assoc
19. trans a + (m * x1) * x3
20. exact hmod_witness_witness
21. congr
22. refl
23. apply mul_assoc

forall P n x b. ~(P = 0) -> ~(n = 0) -> (forall d. (exists u. P = d * u) -> (exists v. n = d * v) -> d = 1) -> exists z. ((forall m a. (exists k. P = m * k) -> (exists u v. x + m * u = a + m * v) -> exists r s. z + m * r = a + m * s) /\ exists q r. z + n * q = b + n * r)

1. intro P
2. intro n
3. intro x
4. intro b
5. intro hP
6. intro hn
7. intro hcop
8. have hcrt : exists z. (exists u v. z + P * u = x + P * v) /\ (exists q r. z + n * q = b + n * r)
9. specialize binary_crt P
10. specialize binary_crt n
11. specialize binary_crt x
12. specialize binary_crt b
13. apply binary_crt
14. exact hP
15. exact hn
16. exact hcop
17. cases hcrt
18. cases hcrt_witness
19. exists x1
20. split
21. intro m
22. intro a
23. intro hmP
24. intro hxa
25. have hzx : exists u v. x1 + m * u = x + m * v
26. specialize mod_eq_of_mod_eq_multiple m
27. specialize mod_eq_of_mod_eq_multiple P
28. specialize mod_eq_of_mod_eq_multiple x1
29. specialize mod_eq_of_mod_eq_multiple x
30. apply mod_eq_of_mod_eq_multiple
31. exact hmP
32. exact hcrt_witness_left
33. specialize mod_eq_trans m
34. specialize mod_eq_trans x1
35. specialize mod_eq_trans x
36. specialize mod_eq_trans a
37. apply mod_eq_trans
38. exact hzx
39. exact hxa
40. exact hcrt_witness_right

forall a b. exists k. a * b = b * k

1. intro a
2. intro b
3. exists a
4. apply mul_comm

forall b c i x. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> exists h. h + x = b

1. intro b
2. intro c
3. intro i
4. intro x
5. intro hat
6. cases hat
7. cases hat_right
8. exists x1 * S ((S i) * c)
9. symm
10. exact hat_right_witness

forall c i. exists h. h + c = S ((S i) * c)

1. intro c
2. intro i
3. have hproduct : exists h. h + c = S i * c
4. specialize mul_succ_left i
5. specialize mul_succ_left c
6. rewrite mul_succ_left
7. specialize le_add_left c
8. specialize le_add_left (i * c)
9. exact le_add_left
10. specialize le_succ c
11. specialize le_succ (S i * c)
12. apply le_succ
13. exact hproduct

forall C B. ~(C = 0) -> exists h. h + B = C * B

1. intro C
2. intro B
3. intro hC
4. have h1C : exists h. h + 1 = C
5. specialize one_le_of_ne_zero C
6. apply one_le_of_ne_zero
7. exact hC
8. have hscaled : exists h. h + 1 * B = C * B
9. specialize mul_le_mul_right 1
10. specialize mul_le_mul_right C
11. specialize mul_le_mul_right B
12. apply mul_le_mul_right
13. exact h1C
14. specialize one_mul B
15. rewrite one_mul at hscaled
16. exact hscaled

forall N C B. (forall t. (exists h. S t + S h = S N) -> exists q. C = S t * q) -> forall t. (exists h. S t + S h = S N) -> exists q. C * B = S t * q

1. intro N
2. intro C
3. intro B
4. intro hcm
5. intro t
6. intro ht
7. have htC : exists q. C = S t * q
8. specialize hcm t
9. apply hcm
10. exact ht
11. specialize multiple_mul_right (S t)
12. specialize multiple_mul_right C
13. specialize multiple_mul_right B
14. apply multiple_mul_right
15. exact htC

forall b c i x C s j. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ~(C = 0) -> exists h. h + S x = S ((S j) * (C * S (b + s)))

1. intro b
2. intro c
3. intro i
4. intro x
5. intro C
6. intro s
7. intro j
8. intro hat
9. intro hC
10. have hxb : exists h. h + x = b
11. specialize beta_value_le_code b
12. specialize beta_value_le_code c
13. specialize beta_value_le_code i
14. specialize beta_value_le_code x
15. apply beta_value_le_code
16. exact hat
17. have hbs : exists h. h + b = b + s
18. specialize le_add_right b
19. specialize le_add_right s
20. exact le_add_right
21. have hxs : exists h. h + x = b + s
22. specialize le_trans x
23. specialize le_trans b
24. specialize le_trans (b + s)
25. apply le_trans
26. exact hxb
27. exact hbs
28. have hsx : exists h. h + S x = S (b + s)
29. specialize succ_le_succ x
30. specialize succ_le_succ (b + s)
31. apply succ_le_succ
32. exact hxs
33. have hscale : exists h. h + S (b + s) = C * S (b + s)
34. specialize le_scaled_nonzero C
35. specialize le_scaled_nonzero (S (b + s))
36. apply le_scaled_nonzero
37. exact hC
38. have hxbase : exists h. h + S x = C * S (b + s)
39. specialize le_trans (S x)
40. specialize le_trans (S (b + s))
41. specialize le_trans (C * S (b + s))
42. apply le_trans
43. exact hsx
44. exact hscale
45. have hmod : exists h. h + C * S (b + s) = S ((S j) * (C * S (b + s)))
46. specialize base_le_beta_modulus (C * S (b + s))
47. specialize base_le_beta_modulus j
48. exact base_le_beta_modulus
49. specialize le_trans (S x)
50. specialize le_trans (C * S (b + s))
51. specialize le_trans (S ((S j) * (C * S (b + s))))
52. apply le_trans
53. exact hxbase
54. exact hmod

forall b s C j. ~(C = 0) -> exists h. h + S s = S ((S j) * (C * S (b + s)))

1. intro b
2. intro s
3. intro C
4. intro j
5. intro hC
6. have hsb : exists h. h + s = b + s
7. specialize le_add_left s
8. specialize le_add_left b
9. exact le_add_left
10. have hss : exists h. h + S s = S (b + s)
11. specialize succ_le_succ s
12. specialize succ_le_succ (b + s)
13. apply succ_le_succ
14. exact hsb
15. have hscale : exists h. h + S (b + s) = C * S (b + s)
16. specialize le_scaled_nonzero C
17. specialize le_scaled_nonzero (S (b + s))
18. apply le_scaled_nonzero
19. exact hC
20. have hsbase : exists h. h + S s = C * S (b + s)
21. specialize le_trans (S s)
22. specialize le_trans (S (b + s))
23. specialize le_trans (C * S (b + s))
24. apply le_trans
25. exact hss
26. exact hscale
27. have hmod : exists h. h + C * S (b + s) = S ((S j) * (C * S (b + s)))
28. specialize base_le_beta_modulus (C * S (b + s))
29. specialize base_le_beta_modulus j
30. exact base_le_beta_modulus
31. specialize le_trans (S s)
32. specialize le_trans (C * S (b + s))
33. specialize le_trans (S ((S j) * (C * S (b + s))))
34. apply le_trans
35. exact hsbase
36. exact hmod

forall N c k P. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1))

1. intro N
2. intro c
3. intro k
4. intro P
5. intro hcm
6. intro hkN
7. intro hP
8. intro hdiv
9. intro hfuture
10. have hnew : ~(S ((S k) * c) = 0)
11. specialize beta_modulus_nonzero c
12. specialize beta_modulus_nonzero k
13. exact beta_modulus_nonzero
14. split
15. specialize mul_ne_zero P
16. specialize mul_ne_zero (S ((S k) * c))
17. intro hzero
18. apply mul_ne_zero
19. exact hP
20. exact hnew
21. exact hzero
22. split
23. intro i
24. intro hi
25. have hik : exists r. r + i = k
26. specialize le_of_succ_le_succ i
27. specialize le_of_succ_le_succ k
28. apply le_of_succ_le_succ
29. exact hi
30. have hsplit : i = k \/ exists r. r + S i = k
31. specialize le_eq_or_lt i
32. specialize le_eq_or_lt k
33. apply le_eq_or_lt
34. exact hik
35. cases hsplit
36. rewrite hsplit_left
37. specialize right_factor_divides_product P
38. specialize right_factor_divides_product (S ((S k) * c))
39. exact right_factor_divides_product
40. have hiP : exists q. P = S ((S i) * c) * q
41. specialize hdiv i
42. apply hdiv
43. exact hsplit_right
44. specialize multiple_mul_right (S ((S i) * c))
45. specialize multiple_mul_right P
46. specialize multiple_mul_right (S ((S k) * c))
47. apply multiple_mul_right
48. exact hiP
49. intro j
50. intro hSkj
51. intro hjN
52. have hkj : exists r. r + k = j
53. have hkSk : exists r. r + k = S k
54. specialize le_succ_self k
55. exact le_succ_self
56. specialize le_trans k
57. specialize le_trans (S k)
58. specialize le_trans j
59. apply le_trans
60. exact hkSk
61. exact hSkj
62. have hPj : forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
63. specialize hfuture j
64. apply hfuture
65. exact hkj
66. exact hjN
67. have hneq : ~(k = j)
68. intro heq
69. rewrite <- heq at hSkj
70. specialize lt_irrefl_expanded k
71. apply lt_irrefl_expanded
72. exact hSkj
73. have hkbound : exists r. r + k = N
74. specialize lt_to_le k
75. specialize lt_to_le N
76. apply lt_to_le
77. exact hkN
78. have hpairs : forall i j. ~(i = j) -> (exists hi. hi + i = N) -> (exists hj. hj + j = N) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
79. specialize beta_moduli_pairwise_coprime_bounded N
80. specialize beta_moduli_pairwise_coprime_bounded c
81. apply beta_moduli_pairwise_coprime_bounded
82. exact hcm
83. have hnewj : forall d. (exists u. S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
84. specialize hpairs k
85. specialize hpairs j
86. apply hpairs
87. exact hneq
88. exact hkbound
89. exact hjN
90. specialize coprime_mul_left P
91. specialize coprime_mul_left (S ((S k) * c))
92. specialize coprime_mul_left (S ((S j) * c))
93. apply coprime_mul_left
94. exact hPj
95. exact hnewj

forall N c b e k P z. (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> exists z2. forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v

1. intro N
2. intro c
3. intro b
4. intro e
5. intro k
6. intro P
7. intro z
8. intro hkN
9. intro hP
10. intro hdiv
11. intro hcong
12. intro hfuture
13. have hnew : ~(S ((S k) * c) = 0)
14. specialize beta_modulus_nonzero c
15. specialize beta_modulus_nonzero k
16. exact beta_modulus_nonzero
17. have hkbound : exists h. h + k = N
18. specialize lt_to_le k
19. specialize lt_to_le N
20. apply lt_to_le
21. exact hkN
22. have hcop : forall d. (exists u. P = d * u) -> (exists v. S ((S k) * c) = d * v) -> d = 1
23. specialize hfuture k
24. apply hfuture
25. specialize le_refl k
26. exact le_refl
27. exact hkbound
28. have hvalue : exists a. ((exists h. h + S a = S ((S k) * e)) /\ exists q. b = q * S ((S k) * e) + a)
29. specialize beta_at_exists b
30. specialize beta_at_exists e
31. specialize beta_at_exists k
32. exact beta_at_exists
33. cases hvalue
34. have hfold : exists z2. ((forall m a. (exists q. P = m * q) -> (exists u v. z + m * u = a + m * v) -> exists r s. z2 + m * r = a + m * s) /\ exists q r. z2 + S ((S k) * c) * q = x + S ((S k) * c) * r)
35. specialize binary_crt_fold_step P
36. specialize binary_crt_fold_step (S ((S k) * c))
37. specialize binary_crt_fold_step z
38. specialize binary_crt_fold_step x
39. apply binary_crt_fold_step
40. exact hP
41. exact hnew
42. exact hcop
43. cases hfold
44. cases hfold_witness
45. exists x1
46. intro i
47. intro a
48. intro hi
49. intro hati
50. have hik : exists r. r + i = k
51. specialize le_of_succ_le_succ i
52. specialize le_of_succ_le_succ k
53. apply le_of_succ_le_succ
54. exact hi
55. have hsplit : i = k \/ exists r. r + S i = k
56. specialize le_eq_or_lt i
57. specialize le_eq_or_lt k
58. apply le_eq_or_lt
59. exact hik
60. cases hsplit
61. have hati_new : ((exists h. h + S a = S ((S k) * e)) /\ exists q. b = q * S ((S k) * e) + a)
62. rewrite <- hsplit_left
63. rewrite <- hsplit_left
64. exact hati
65. have haeq : a = x
66. specialize beta_at_unique b
67. specialize beta_at_unique e
68. specialize beta_at_unique k
69. specialize beta_at_unique a
70. specialize beta_at_unique x
71. apply beta_at_unique
72. exact hati_new
73. exact hvalue_witness
74. rewrite hsplit_left
75. rewrite hsplit_left
76. rewrite haeq
77. exact hfold_witness_right
78. have hmiP : exists q. P = S ((S i) * c) * q
79. specialize hdiv i
80. apply hdiv
81. exact hsplit_right
82. have hzold : exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v
83. specialize hcong i
84. specialize hcong a
85. apply hcong
86. exact hsplit_right
87. exact hati
88. specialize hfold_witness_left (S ((S i) * c))
89. specialize hfold_witness_left a
90. apply hfold_witness_left
91. exact hmiP
92. exact hzold

forall N c b e k P z. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> exists z2. (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))

1. intro N
2. intro c
3. intro b
4. intro e
5. intro k
6. intro P
7. intro z
8. intro hcm
9. intro hkN
10. intro hP
11. intro hdiv
12. intro hcong
13. intro hfuture
14. have hproduct : (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1))
15. specialize beta_exclusive_accumulated_product_step N
16. specialize beta_exclusive_accumulated_product_step c
17. specialize beta_exclusive_accumulated_product_step k
18. specialize beta_exclusive_accumulated_product_step P
19. apply beta_exclusive_accumulated_product_step
20. exact hcm
21. exact hkN
22. exact hP
23. exact hdiv
24. exact hfuture
25. have hcodes : exists z2. forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v
26. specialize beta_exclusive_recode_congruence_step N
27. specialize beta_exclusive_recode_congruence_step c
28. specialize beta_exclusive_recode_congruence_step b
29. specialize beta_exclusive_recode_congruence_step e
30. specialize beta_exclusive_recode_congruence_step k
31. specialize beta_exclusive_recode_congruence_step P
32. specialize beta_exclusive_recode_congruence_step z
33. apply beta_exclusive_recode_congruence_step
34. exact hkN
35. exact hP
36. exact hdiv
37. exact hcong
38. exact hfuture
39. cases hcodes
40. cases hproduct
41. cases hproduct_right
42. exists x
43. split
44. exact hproduct_left
45. split
46. exact hproduct_right_left
47. split
48. exact hcodes_witness
49. exact hproduct_right_right

forall N c b e. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> forall k. (exists h. h + k = N) -> exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))

1. intro N
2. intro c
3. intro b
4. intro e
5. intro hcm
6. induction k
7. intro hkN
8. exists 1
9. exists 0
10. split
11. specialize succ_ne_zero 0
12. exact succ_ne_zero
13. split
14. intro i
15. intro hi
16. exfalso
17. cases hi
18. have hsi0 : S i = 0
19. specialize add_eq_zero_right x
20. specialize add_eq_zero_right (S i)
21. apply add_eq_zero_right
22. exact hi_witness
23. specialize succ_ne_zero i
24. apply succ_ne_zero
25. exact hsi0
26. split
27. intro i
28. intro a
29. intro hi
30. intro hati
31. exfalso
32. cases hi
33. have hsi0 : S i = 0
34. specialize add_eq_zero_right x
35. specialize add_eq_zero_right (S i)
36. apply add_eq_zero_right
37. exact hi_witness
38. specialize succ_ne_zero i
39. apply succ_ne_zero
40. exact hsi0
41. intro j
42. intro h0j
43. intro hjN
44. intro d
45. intro h1
46. intro hm
47. specialize coprime_one_left (S ((S j) * c))
48. specialize coprime_one_left d
49. apply coprime_one_left
50. exact h1
51. exact hm
52. intro hkN
53. have hkprev : exists h. h + k = N
54. have hkstep : exists h. h + k = S k
55. specialize le_succ_self k
56. exact le_succ_self
57. specialize le_trans k
58. specialize le_trans (S k)
59. specialize le_trans N
60. apply le_trans
61. exact hkstep
62. exact hkN
63. have hprev : exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))
64. apply IH
65. exact hkprev
66. cases hprev
67. cases hprev_witness
68. cases hprev_witness_witness
69. cases hprev_witness_witness_right
70. cases hprev_witness_witness_right_right
71. have hnext : exists z2. (~(x * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. x * S ((S k) * c) = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. x * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))
72. specialize beta_exclusive_recode_invariant_step N
73. specialize beta_exclusive_recode_invariant_step c
74. specialize beta_exclusive_recode_invariant_step b
75. specialize beta_exclusive_recode_invariant_step e
76. specialize beta_exclusive_recode_invariant_step k
77. specialize beta_exclusive_recode_invariant_step x
78. specialize beta_exclusive_recode_invariant_step x1
79. apply beta_exclusive_recode_invariant_step
80. exact hcm
81. exact hkN
82. exact hprev_witness_witness_left
83. exact hprev_witness_witness_right_left
84. exact hprev_witness_witness_right_right_left
85. exact hprev_witness_witness_right_right_right
86. cases hnext
87. exists x * S ((S k) * c)
88. exists x2
89. exact hnext_witness

forall k b e s. exists z c. (((exists h. h + S s = S ((S k) * c)) /\ exists q. z = q * S ((S k) * c) + s) /\ forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. z = q * S ((S i) * c) + a))

1. intro k
2. intro b
3. intro e
4. intro s
5. have hC : exists C. (~(C = 0) /\ forall t. (exists h. S t + S h = S k) -> exists q. C = S t * q)
6. specialize bounded_common_multiple_exists k
7. exact bounded_common_multiple_exists
8. cases hC
9. cases hC_witness
10. have hcm2 : forall t. (exists h. S t + S h = S k) -> exists q. x * S (b + s) = S t * q
11. specialize scaled_bounded_common_multiple k
12. specialize scaled_bounded_common_multiple x
13. specialize scaled_bounded_common_multiple (S (b + s))
14. apply scaled_bounded_common_multiple
15. exact hC_witness_right
16. have hall : forall n. (exists h. h + n = k) -> exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = n) -> exists q. P = S ((S i) * (x * S (b + s))) * q) /\ ((forall i a. (exists h. h + S i = n) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v) /\ forall j. (exists g. g + n = j) -> (exists h. h + j = k) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * (x * S (b + s))) = d * v) -> d = 1)))
17. specialize bounded_beta_exclusive_recode_invariant k
18. specialize bounded_beta_exclusive_recode_invariant (x * S (b + s))
19. specialize bounded_beta_exclusive_recode_invariant b
20. specialize bounded_beta_exclusive_recode_invariant e
21. apply bounded_beta_exclusive_recode_invariant
22. exact hcm2
23. have hinv : exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * (x * S (b + s))) * q) /\ ((forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v) /\ forall j. (exists g. g + k = j) -> (exists h. h + j = k) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * (x * S (b + s))) = d * v) -> d = 1)))
24. specialize hall k
25. apply hall
26. specialize le_refl k
27. exact le_refl
28. cases hinv
29. cases hinv_witness
30. cases hinv_witness_witness
31. cases hinv_witness_witness_right
32. cases hinv_witness_witness_right_right
33. have hcop : forall d. (exists u. x1 = d * u) -> (exists v. S ((S k) * (x * S (b + s))) = d * v) -> d = 1
34. specialize hinv_witness_witness_right_right_right k
35. apply hinv_witness_witness_right_right_right
36. specialize le_refl k
37. exact le_refl
38. specialize le_refl k
39. exact le_refl
40. have hnew0 : ~(S ((S k) * (x * S (b + s))) = 0)
41. specialize beta_modulus_nonzero (x * S (b + s))
42. specialize beta_modulus_nonzero k
43. exact beta_modulus_nonzero
44. have hfold : exists z2. ((forall m a. (exists q. x1 = m * q) -> (exists u v. x2 + m * u = a + m * v) -> exists r t. z2 + m * r = a + m * t) /\ exists q r. z2 + S ((S k) * (x * S (b + s))) * q = s + S ((S k) * (x * S (b + s))) * r)
45. specialize binary_crt_fold_step x1
46. specialize binary_crt_fold_step (S ((S k) * (x * S (b + s))))
47. specialize binary_crt_fold_step x2
48. specialize binary_crt_fold_step s
49. apply binary_crt_fold_step
50. exact hinv_witness_witness_left
51. exact hnew0
52. exact hcop
53. cases hfold
54. cases hfold_witness
55. exists x3
56. exists x * S (b + s)
57. split
58. specialize beta_at_of_mod_eq_bound x3
59. specialize beta_at_of_mod_eq_bound (x * S (b + s))
60. specialize beta_at_of_mod_eq_bound k
61. specialize beta_at_of_mod_eq_bound s
62. apply beta_at_of_mod_eq_bound
63. specialize new_value_lt_scaled_base b
64. specialize new_value_lt_scaled_base s
65. specialize new_value_lt_scaled_base x
66. specialize new_value_lt_scaled_base k
67. apply new_value_lt_scaled_base
68. exact hC_witness_left
69. exact hfold_witness_right
70. intro i
71. intro a
72. intro hi
73. intro hati
74. have hmi : exists q. x1 = S ((S i) * (x * S (b + s))) * q
75. specialize hinv_witness_witness_right_left i
76. apply hinv_witness_witness_right_left
77. exact hi
78. have hzold : exists u v. x2 + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v
79. specialize hinv_witness_witness_right_right_left i
80. specialize hinv_witness_witness_right_right_left a
81. apply hinv_witness_witness_right_right_left
82. exact hi
83. exact hati
84. have hznew : exists u v. x3 + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v
85. specialize hfold_witness_left (S ((S i) * (x * S (b + s))))
86. specialize hfold_witness_left a
87. apply hfold_witness_left
88. exact hmi
89. exact hzold
90. specialize beta_at_of_mod_eq_bound x3
91. specialize beta_at_of_mod_eq_bound (x * S (b + s))
92. specialize beta_at_of_mod_eq_bound i
93. specialize beta_at_of_mod_eq_bound a
94. apply beta_at_of_mod_eq_bound
95. specialize beta_value_lt_scaled_base b
96. specialize beta_value_lt_scaled_base e
97. specialize beta_value_lt_scaled_base i
98. specialize beta_value_lt_scaled_base a
99. specialize beta_value_lt_scaled_base x
100. specialize beta_value_lt_scaled_base s
101. specialize beta_value_lt_scaled_base i
102. apply beta_value_lt_scaled_base
103. exact hati
104. exact hC_witness_left
105. exact hznew

forall b c a l. l = 0 -> (forall ff_i_empty. (exists ff_lt_empty_bound. ff_lt_empty_bound + S ff_i_empty = l) -> (((exists ff_h_empty_decoded. ff_h_empty_decoded + S (a) = S ((S (ff_i_empty)) * c)) /\ exists ff_q_empty_decoded. b = ff_q_empty_decoded * S ((S (ff_i_empty)) * c) + (a))))

1. intro b
2. intro c
3. intro a
4. intro l
5. intro hl
6. intro i
7. intro hi
8. rewrite hl at hi
9. exfalso
10. cases hi
11. have hsi : S i = 0
12. specialize add_eq_zero_right x
13. specialize add_eq_zero_right (S i)
14. apply add_eq_zero_right
15. exact hi_witness
16. specialize succ_ne_zero i
17. apply succ_ne_zero
18. exact hsi

forall b c a l sl. sl = S l -> (forall ff_i_before. (exists ff_lt_before_bound. ff_lt_before_bound + S ff_i_before = l) -> (((exists ff_h_before_decoded. ff_h_before_decoded + S (a) = S ((S (ff_i_before)) * c)) /\ exists ff_q_before_decoded. b = ff_q_before_decoded * S ((S (ff_i_before)) * c) + (a)))) -> exists z d. (forall ff_i_after. (exists ff_lt_after_bound. ff_lt_after_bound + S ff_i_after = sl) -> (((exists ff_h_after_decoded. ff_h_after_decoded + S (a) = S ((S (ff_i_after)) * d)) /\ exists ff_q_after_decoded. z = ff_q_after_decoded * S ((S (ff_i_after)) * d) + (a))))

1. intro b
2. intro c
3. intro a
4. intro l
5. intro sl
6. intro hsl
7. intro hrepeat
8. specialize beta_prefix_extend l
9. specialize beta_prefix_extend b
10. specialize beta_prefix_extend c
11. specialize beta_prefix_extend a
12. cases beta_prefix_extend
13. cases beta_prefix_extend_witness
14. cases beta_prefix_extend_witness_witness
15. exists x
16. exists x1
17. intro i
18. intro hi
19. rewrite hsl at hi
20. have hil : exists h. h + i = l
21. specialize le_of_succ_le_succ i
22. specialize le_of_succ_le_succ l
23. apply le_of_succ_le_succ
24. exact hi
25. have hsplit : i = l \/ exists h. h + S i = l
26. specialize le_eq_or_lt i
27. specialize le_eq_or_lt l
28. apply le_eq_or_lt
29. exact hil
30. cases hsplit
31. rewrite hsplit_left
32. rewrite hsplit_left
33. exact beta_prefix_extend_witness_witness_left
34. specialize beta_prefix_extend_witness_witness_right i
35. specialize beta_prefix_extend_witness_witness_right a
36. apply beta_prefix_extend_witness_witness_right
37. exact hsplit_right
38. specialize hrepeat i
39. apply hrepeat
40. exact hsplit_right

forall a l. exists b c. (forall ff_i_r. (exists ff_lt_r_bound. ff_lt_r_bound + S ff_i_r = l) -> (((exists ff_h_r_decoded. ff_h_r_decoded + S (a) = S ((S (ff_i_r)) * c)) /\ exists ff_q_r_decoded. b = ff_q_r_decoded * S ((S (ff_i_r)) * c) + (a))))

1. intro a
2. induction l
3. exists 0
4. exists 0
5. specialize beta_repeat_empty 0
6. specialize beta_repeat_empty 0
7. specialize beta_repeat_empty a
8. specialize beta_repeat_empty 0
9. apply beta_repeat_empty
10. refl
11. cases IH
12. cases IH_witness
13. specialize beta_repeat_succ_extend x
14. specialize beta_repeat_succ_extend x1
15. specialize beta_repeat_succ_extend a
16. specialize beta_repeat_succ_extend l
17. specialize beta_repeat_succ_extend (S l)
18. apply beta_repeat_succ_extend
19. refl
20. exact IH_witness_witness

forall b c a l i x. (forall ff_i_entry. (exists ff_lt_entry_bound. ff_lt_entry_bound + S ff_i_entry = l) -> (((exists ff_h_entry_decoded. ff_h_entry_decoded + S (a) = S ((S (ff_i_entry)) * c)) /\ exists ff_q_entry_decoded. b = ff_q_entry_decoded * S ((S (ff_i_entry)) * c) + (a)))) -> (exists h. h + S i = l) -> (((exists ff_h_entry_x. ff_h_entry_x + S (x) = S ((S (i)) * c)) /\ exists ff_q_entry_x. b = ff_q_entry_x * S ((S (i)) * c) + (x))) -> x = a

1. intro b
2. intro c
3. intro a
4. intro l
5. intro i
6. intro x
7. intro hrepeat
8. intro hi
9. intro hx
10. have ha : ((exists h. h + S a = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + a)
11. specialize hrepeat i
12. apply hrepeat
13. exact hi
14. specialize beta_at_unique b
15. specialize beta_at_unique c
16. specialize beta_at_unique i
17. specialize beta_at_unique x
18. specialize beta_at_unique a
19. apply beta_at_unique
20. exact hx
21. exact ha

forall b c l. exists fs_u_trace fs_v_trace. ((((exists fs_h_trace_start. fs_h_trace_start + S (0) = S ((S (0)) * fs_v_trace)) /\ exists fs_q_trace_start. fs_u_trace = fs_q_trace_start * S ((S (0)) * fs_v_trace) + (0))) /\ forall fs_i_trace_steps. (exists fs_lt_trace_steps_bound. fs_lt_trace_steps_bound + S fs_i_trace_steps = l) -> exists fs_a_trace_steps fs_r_trace_steps fs_s_trace_steps. ((((exists fs_h_trace_steps_summand. fs_h_trace_steps_summand + S (fs_a_trace_steps) = S ((S (fs_i_trace_steps)) * c)) /\ exists fs_q_trace_steps_summand. b = fs_q_trace_steps_summand * S ((S (fs_i_trace_steps)) * c) + (fs_a_trace_steps))) /\ ((((exists fs_h_trace_steps_partial. fs_h_trace_steps_partial + S (fs_r_trace_steps) = S ((S (fs_i_trace_steps)) * fs_v_trace)) /\ exists fs_q_trace_steps_partial. fs_u_trace = fs_q_trace_steps_partial * S ((S (fs_i_trace_steps)) * fs_v_trace) + (fs_r_trace_steps))) /\ ((((exists fs_h_trace_steps_successor. fs_h_trace_steps_successor + S (fs_s_trace_steps) = S ((S (S fs_i_trace_steps)) * fs_v_trace)) /\ exists fs_q_trace_steps_successor. fs_u_trace = fs_q_trace_steps_successor * S ((S (S fs_i_trace_steps)) * fs_v_trace) + (fs_s_trace_steps))) /\ fs_s_trace_steps = fs_r_trace_steps + fs_a_trace_steps))))

1. intro b
2. intro c
3. induction l
4. exists 0
5. exists 1
6. split
7. specialize beta_at_self_of_bound 1
8. specialize beta_at_self_of_bound 0
9. specialize beta_at_self_of_bound 0
10. apply beta_at_self_of_bound
11. specialize one_mul 1
12. rewrite one_mul
13. specialize succ_le_succ 0
14. specialize succ_le_succ (S 0)
15. apply succ_le_succ
16. specialize zero_le (S 0)
17. exact zero_le
18. intro i
19. intro hi
20. exfalso
21. cases hi
22. have hsi0 : S i = 0
23. specialize add_eq_zero_right x
24. specialize add_eq_zero_right (S i)
25. apply add_eq_zero_right
26. exact hi_witness
27. specialize succ_ne_zero i
28. apply succ_ne_zero
29. exact hsi0
30. have htrace : exists fs_u_induction fs_v_induction. ((((exists fs_h_induction_start. fs_h_induction_start + S (0) = S ((S (0)) * fs_v_induction)) /\ exists fs_q_induction_start. fs_u_induction = fs_q_induction_start * S ((S (0)) * fs_v_induction) + (0))) /\ forall fs_i_induction_steps. (exists fs_lt_induction_steps_bound. fs_lt_induction_steps_bound + S fs_i_induction_steps = l) -> exists fs_a_induction_steps fs_r_induction_steps fs_s_induction_steps. ((((exists fs_h_induction_steps_summand. fs_h_induction_steps_summand + S (fs_a_induction_steps) = S ((S (fs_i_induction_steps)) * c)) /\ exists fs_q_induction_steps_summand. b = fs_q_induction_steps_summand * S ((S (fs_i_induction_steps)) * c) + (fs_a_induction_steps))) /\ ((((exists fs_h_induction_steps_partial. fs_h_induction_steps_partial + S (fs_r_induction_steps) = S ((S (fs_i_induction_steps)) * fs_v_induction)) /\ exists fs_q_induction_steps_partial. fs_u_induction = fs_q_induction_steps_partial * S ((S (fs_i_induction_steps)) * fs_v_induction) + (fs_r_induction_steps))) /\ ((((exists fs_h_induction_steps_successor. fs_h_induction_steps_successor + S (fs_s_induction_steps) = S ((S (S fs_i_induction_steps)) * fs_v_induction)) /\ exists fs_q_induction_steps_successor. fs_u_induction = fs_q_induction_steps_successor * S ((S (S fs_i_induction_steps)) * fs_v_induction) + (fs_s_induction_steps))) /\ fs_s_induction_steps = fs_r_induction_steps + fs_a_induction_steps))))
31. apply IH
32. cases htrace
33. cases htrace_witness
34. cases htrace_witness_witness
35. have hfactor : exists p. ((exists fs_h_trace_factor. fs_h_trace_factor + S (p) = S ((S (l)) * c)) /\ exists fs_q_trace_factor. b = fs_q_trace_factor * S ((S (l)) * c) + (p))
36. specialize beta_at_exists b
37. specialize beta_at_exists c
38. specialize beta_at_exists l
39. exact beta_at_exists
40. cases hfactor
41. have hlast : exists r. ((exists fs_h_trace_last. fs_h_trace_last + S (r) = S ((S (l)) * x1)) /\ exists fs_q_trace_last. x = fs_q_trace_last * S ((S (l)) * x1) + (r))
42. specialize beta_at_exists x
43. specialize beta_at_exists x1
44. specialize beta_at_exists l
45. exact beta_at_exists
46. cases hlast
47. have hext : exists z v. ((((exists fs_h_trace_extension. fs_h_trace_extension + S (x3 + x2) = S ((S (S l)) * v)) /\ exists fs_q_trace_extension. z = fs_q_trace_extension * S ((S (S l)) * v) + (x3 + x2))) /\ forall i a. (exists h. h + S i = S l) -> (((exists fs_h_trace_old. fs_h_trace_old + S (a) = S ((S (i)) * x1)) /\ exists fs_q_trace_old. x = fs_q_trace_old * S ((S (i)) * x1) + (a))) -> (((exists fs_h_trace_new. fs_h_trace_new + S (a) = S ((S (i)) * v)) /\ exists fs_q_trace_new. z = fs_q_trace_new * S ((S (i)) * v) + (a))))
48. specialize beta_prefix_extend (S l)
49. specialize beta_prefix_extend x
50. specialize beta_prefix_extend x1
51. specialize beta_prefix_extend (x3 + x2)
52. exact beta_prefix_extend
53. cases hext
54. cases hext_witness
55. cases hext_witness_witness
56. exists x4
57. exists x5
58. split
59. specialize hext_witness_witness_right 0
60. specialize hext_witness_witness_right 0
61. apply hext_witness_witness_right
62. have h0 : exists h. h + S 0 = S l
63. have hzero : exists h. h + 0 = l
64. specialize zero_le l
65. exact zero_le
66. specialize succ_le_succ 0
67. specialize succ_le_succ l
68. apply succ_le_succ
69. exact hzero
70. exact h0
71. exact htrace_witness_witness_left
72. intro i
73. intro hi
74. have hil : exists h. h + i = l
75. specialize le_of_succ_le_succ i
76. specialize le_of_succ_le_succ l
77. apply le_of_succ_le_succ
78. exact hi
79. have hsplit : i = l \/ exists h. h + S i = l
80. specialize le_eq_or_lt i
81. specialize le_eq_or_lt l
82. apply le_eq_or_lt
83. exact hil
84. cases hsplit
85. exists x2
86. exists x3
87. exists x3 + x2
88. split
89. rewrite hsplit_left
90. rewrite hsplit_left
91. exact hfactor_witness
92. split
93. rewrite hsplit_left
94. rewrite hsplit_left
95. specialize hext_witness_witness_right l
96. specialize hext_witness_witness_right x3
97. apply hext_witness_witness_right
98. specialize le_refl (S l)
99. exact le_refl
100. exact hlast_witness
101. split
102. rewrite hsplit_left
103. rewrite hsplit_left
104. exact hext_witness_witness_left
105. refl
106. have hold : exists p r s. ((((exists fs_h_trace_hold_factor. fs_h_trace_hold_factor + S (p) = S ((S (i)) * c)) /\ exists fs_q_trace_hold_factor. b = fs_q_trace_hold_factor * S ((S (i)) * c) + (p))) /\ ((((exists fs_h_trace_hold_partial. fs_h_trace_hold_partial + S (r) = S ((S (i)) * x1)) /\ exists fs_q_trace_hold_partial. x = fs_q_trace_hold_partial * S ((S (i)) * x1) + (r))) /\ ((((exists fs_h_trace_hold_successor. fs_h_trace_hold_successor + S (s) = S ((S (S i)) * x1)) /\ exists fs_q_trace_hold_successor. x = fs_q_trace_hold_successor * S ((S (S i)) * x1) + (s))) /\ s = r + p)))
107. specialize htrace_witness_witness_right i
108. apply htrace_witness_witness_right
109. exact hsplit_right
110. cases hold
111. cases hold_witness
112. cases hold_witness_witness
113. cases hold_witness_witness_witness
114. cases hold_witness_witness_witness_right
115. cases hold_witness_witness_witness_right_right
116. exists x6
117. exists x7
118. exists x8
119. split
120. exact hold_witness_witness_witness_left
121. split
122. specialize hext_witness_witness_right i
123. specialize hext_witness_witness_right x7
124. apply hext_witness_witness_right
125. exact hi
126. exact hold_witness_witness_witness_right_left
127. split
128. specialize hext_witness_witness_right (S i)
129. specialize hext_witness_witness_right x8
130. apply hext_witness_witness_right
131. specialize succ_le_succ (S i)
132. specialize succ_le_succ l
133. apply succ_le_succ
134. exact hsplit_right
135. exact hold_witness_witness_witness_right_right_left
136. exact hold_witness_witness_witness_right_right_right

forall b c l. exists n. (exists ff_u_x ff_v_x. ((((exists ff_h_x_start. ff_h_x_start + S (0) = S ((S (0)) * ff_v_x)) /\ exists ff_q_x_start. ff_u_x = ff_q_x_start * S ((S (0)) * ff_v_x) + (0))) /\ ((((exists ff_h_x_terminal. ff_h_x_terminal + S (n) = S ((S (l)) * ff_v_x)) /\ exists ff_q_x_terminal. ff_u_x = ff_q_x_terminal * S ((S (l)) * ff_v_x) + (n))) /\ forall ff_i_x. (exists ff_lt_x_bound. ff_lt_x_bound + S ff_i_x = l) -> exists ff_a_x ff_r_x ff_s_x. ((((exists ff_h_x_summand. ff_h_x_summand + S (ff_a_x) = S ((S (ff_i_x)) * c)) /\ exists ff_q_x_summand. b = ff_q_x_summand * S ((S (ff_i_x)) * c) + (ff_a_x))) /\ ((((exists ff_h_x_partial. ff_h_x_partial + S (ff_r_x) = S ((S (ff_i_x)) * ff_v_x)) /\ exists ff_q_x_partial. ff_u_x = ff_q_x_partial * S ((S (ff_i_x)) * ff_v_x) + (ff_r_x))) /\ ((((exists ff_h_x_successor. ff_h_x_successor + S (ff_s_x) = S ((S (S ff_i_x)) * ff_v_x)) /\ exists ff_q_x_successor. ff_u_x = ff_q_x_successor * S ((S (S ff_i_x)) * ff_v_x) + (ff_s_x))) /\ ff_s_x = ff_r_x + ff_a_x))))))

1. intro b
2. intro c
3. intro l
4. have htrace : exists fs_u_exists_trace fs_v_exists_trace. ((((exists fs_h_exists_trace_start. fs_h_exists_trace_start + S (0) = S ((S (0)) * fs_v_exists_trace)) /\ exists fs_q_exists_trace_start. fs_u_exists_trace = fs_q_exists_trace_start * S ((S (0)) * fs_v_exists_trace) + (0))) /\ forall fs_i_exists_trace_steps. (exists fs_lt_exists_trace_steps_bound. fs_lt_exists_trace_steps_bound + S fs_i_exists_trace_steps = l) -> exists fs_a_exists_trace_steps fs_r_exists_trace_steps fs_s_exists_trace_steps. ((((exists fs_h_exists_trace_steps_summand. fs_h_exists_trace_steps_summand + S (fs_a_exists_trace_steps) = S ((S (fs_i_exists_trace_steps)) * c)) /\ exists fs_q_exists_trace_steps_summand. b = fs_q_exists_trace_steps_summand * S ((S (fs_i_exists_trace_steps)) * c) + (fs_a_exists_trace_steps))) /\ ((((exists fs_h_exists_trace_steps_partial. fs_h_exists_trace_steps_partial + S (fs_r_exists_trace_steps) = S ((S (fs_i_exists_trace_steps)) * fs_v_exists_trace)) /\ exists fs_q_exists_trace_steps_partial. fs_u_exists_trace = fs_q_exists_trace_steps_partial * S ((S (fs_i_exists_trace_steps)) * fs_v_exists_trace) + (fs_r_exists_trace_steps))) /\ ((((exists fs_h_exists_trace_steps_successor. fs_h_exists_trace_steps_successor + S (fs_s_exists_trace_steps) = S ((S (S fs_i_exists_trace_steps)) * fs_v_exists_trace)) /\ exists fs_q_exists_trace_steps_successor. fs_u_exists_trace = fs_q_exists_trace_steps_successor * S ((S (S fs_i_exists_trace_steps)) * fs_v_exists_trace) + (fs_s_exists_trace_steps))) /\ fs_s_exists_trace_steps = fs_r_exists_trace_steps + fs_a_exists_trace_steps))))
5. specialize beta_prefix_sum_trace_exists b
6. specialize beta_prefix_sum_trace_exists c
7. specialize beta_prefix_sum_trace_exists l
8. exact beta_prefix_sum_trace_exists
9. cases htrace
10. cases htrace_witness
11. cases htrace_witness_witness
12. have hterminal : exists n. ((exists fs_h_sum_terminal. fs_h_sum_terminal + S (n) = S ((S (l)) * x1)) /\ exists fs_q_sum_terminal. x = fs_q_sum_terminal * S ((S (l)) * x1) + (n))
13. specialize beta_at_exists x
14. specialize beta_at_exists x1
15. specialize beta_at_exists l
16. exact beta_at_exists
17. cases hterminal
18. exists x2
19. exists x
20. exists x1
21. split
22. exact htrace_witness_witness_left
23. split
24. exact hterminal_witness
25. exact htrace_witness_witness_right

forall b c l n u v m w d. (((((exists fs_h_functional_left_start. fs_h_functional_left_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_functional_left_start. u = fs_q_functional_left_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_functional_left_terminal. fs_h_functional_left_terminal + S (n) = S ((S (l)) * v)) /\ exists fs_q_functional_left_terminal. u = fs_q_functional_left_terminal * S ((S (l)) * v) + (n))) /\ forall fs_i_functional_left_steps. (exists fs_lt_functional_left_steps_bound. fs_lt_functional_left_steps_bound + S fs_i_functional_left_steps = l) -> exists fs_a_functional_left_steps fs_r_functional_left_steps fs_s_functional_left_steps. ((((exists fs_h_functional_left_steps_summand. fs_h_functional_left_steps_summand + S (fs_a_functional_left_steps) = S ((S (fs_i_functional_left_steps)) * c)) /\ exists fs_q_functional_left_steps_summand. b = fs_q_functional_left_steps_summand * S ((S (fs_i_functional_left_steps)) * c) + (fs_a_functional_left_steps))) /\ ((((exists fs_h_functional_left_steps_partial. fs_h_functional_left_steps_partial + S (fs_r_functional_left_steps) = S ((S (fs_i_functional_left_steps)) * v)) /\ exists fs_q_functional_left_steps_partial. u = fs_q_functional_left_steps_partial * S ((S (fs_i_functional_left_steps)) * v) + (fs_r_functional_left_steps))) /\ ((((exists fs_h_functional_left_steps_successor. fs_h_functional_left_steps_successor + S (fs_s_functional_left_steps) = S ((S (S fs_i_functional_left_steps)) * v)) /\ exists fs_q_functional_left_steps_successor. u = fs_q_functional_left_steps_successor * S ((S (S fs_i_functional_left_steps)) * v) + (fs_s_functional_left_steps))) /\ fs_s_functional_left_steps = fs_r_functional_left_steps + fs_a_functional_left_steps)))))) -> (((((exists fs_h_functional_right_start. fs_h_functional_right_start + S (0) = S ((S (0)) * d)) /\ exists fs_q_functional_right_start. w = fs_q_functional_right_start * S ((S (0)) * d) + (0))) /\ ((((exists fs_h_functional_right_terminal. fs_h_functional_right_terminal + S (m) = S ((S (l)) * d)) /\ exists fs_q_functional_right_terminal. w = fs_q_functional_right_terminal * S ((S (l)) * d) + (m))) /\ forall fs_i_functional_right_steps. (exists fs_lt_functional_right_steps_bound. fs_lt_functional_right_steps_bound + S fs_i_functional_right_steps = l) -> exists fs_a_functional_right_steps fs_r_functional_right_steps fs_s_functional_right_steps. ((((exists fs_h_functional_right_steps_summand. fs_h_functional_right_steps_summand + S (fs_a_functional_right_steps) = S ((S (fs_i_functional_right_steps)) * c)) /\ exists fs_q_functional_right_steps_summand. b = fs_q_functional_right_steps_summand * S ((S (fs_i_functional_right_steps)) * c) + (fs_a_functional_right_steps))) /\ ((((exists fs_h_functional_right_steps_partial. fs_h_functional_right_steps_partial + S (fs_r_functional_right_steps) = S ((S (fs_i_functional_right_steps)) * d)) /\ exists fs_q_functional_right_steps_partial. w = fs_q_functional_right_steps_partial * S ((S (fs_i_functional_right_steps)) * d) + (fs_r_functional_right_steps))) /\ ((((exists fs_h_functional_right_steps_successor. fs_h_functional_right_steps_successor + S (fs_s_functional_right_steps) = S ((S (S fs_i_functional_right_steps)) * d)) /\ exists fs_q_functional_right_steps_successor. w = fs_q_functional_right_steps_successor * S ((S (S fs_i_functional_right_steps)) * d) + (fs_s_functional_right_steps))) /\ fs_s_functional_right_steps = fs_r_functional_right_steps + fs_a_functional_right_steps)))))) -> n = m

1. intro b
2. intro c
3. induction l
4. intro n
5. intro u
6. intro v
7. intro m
8. intro w
9. intro d
10. intro h1
11. intro h2
12. cases h1
13. cases h1_right
14. cases h2
15. cases h2_right
16. have hn : n = 0
17. specialize beta_at_unique u
18. specialize beta_at_unique v
19. specialize beta_at_unique 0
20. specialize beta_at_unique n
21. specialize beta_at_unique 0
22. apply beta_at_unique
23. exact h1_right_left
24. exact h1_left
25. have hm : m = 0
26. specialize beta_at_unique w
27. specialize beta_at_unique d
28. specialize beta_at_unique 0
29. specialize beta_at_unique m
30. specialize beta_at_unique 0
31. apply beta_at_unique
32. exact h2_right_left
33. exact h2_left
34. trans 0
35. exact hn
36. symm
37. exact hm
38. intro n
39. intro u
40. intro v
41. intro m
42. intro w
43. intro d
44. intro h1
45. intro h2
46. cases h1
47. cases h1_right
48. cases h2
49. cases h2_right
50. have hstep1 : exists a r s. ((((exists fs_h_functional_step1_factor. fs_h_functional_step1_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_functional_step1_factor. b = fs_q_functional_step1_factor * S ((S (l)) * c) + (a))) /\ ((((exists fs_h_functional_step1_partial. fs_h_functional_step1_partial + S (r) = S ((S (l)) * v)) /\ exists fs_q_functional_step1_partial. u = fs_q_functional_step1_partial * S ((S (l)) * v) + (r))) /\ ((((exists fs_h_functional_step1_successor. fs_h_functional_step1_successor + S (s) = S ((S (S l)) * v)) /\ exists fs_q_functional_step1_successor. u = fs_q_functional_step1_successor * S ((S (S l)) * v) + (s))) /\ s = r + a)))
51. specialize h1_right_right l
52. apply h1_right_right
53. specialize le_refl (S l)
54. exact le_refl
55. cases hstep1
56. cases hstep1_witness
57. cases hstep1_witness_witness
58. cases hstep1_witness_witness_witness
59. cases hstep1_witness_witness_witness_right
60. cases hstep1_witness_witness_witness_right_right
61. have hstep2 : exists a r s. ((((exists fs_h_functional_step2_factor. fs_h_functional_step2_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_functional_step2_factor. b = fs_q_functional_step2_factor * S ((S (l)) * c) + (a))) /\ ((((exists fs_h_functional_step2_partial. fs_h_functional_step2_partial + S (r) = S ((S (l)) * d)) /\ exists fs_q_functional_step2_partial. w = fs_q_functional_step2_partial * S ((S (l)) * d) + (r))) /\ ((((exists fs_h_functional_step2_successor. fs_h_functional_step2_successor + S (s) = S ((S (S l)) * d)) /\ exists fs_q_functional_step2_successor. w = fs_q_functional_step2_successor * S ((S (S l)) * d) + (s))) /\ s = r + a)))
62. specialize h2_right_right l
63. apply h2_right_right
64. specialize le_refl (S l)
65. exact le_refl
66. cases hstep2
67. cases hstep2_witness
68. cases hstep2_witness_witness
69. cases hstep2_witness_witness_witness
70. cases hstep2_witness_witness_witness_right
71. cases hstep2_witness_witness_witness_right_right
72. have hn : n = x2
73. specialize beta_at_unique u
74. specialize beta_at_unique v
75. specialize beta_at_unique (S l)
76. specialize beta_at_unique n
77. specialize beta_at_unique x2
78. apply beta_at_unique
79. exact h1_right_left
80. exact hstep1_witness_witness_witness_right_right_left
81. have hm : m = x5
82. specialize beta_at_unique w
83. specialize beta_at_unique d
84. specialize beta_at_unique (S l)
85. specialize beta_at_unique m
86. specialize beta_at_unique x5
87. apply beta_at_unique
88. exact h2_right_left
89. exact hstep2_witness_witness_witness_right_right_left
90. have ha : x = x3
91. specialize beta_at_unique b
92. specialize beta_at_unique c
93. specialize beta_at_unique l
94. specialize beta_at_unique x
95. specialize beta_at_unique x3
96. apply beta_at_unique
97. exact hstep1_witness_witness_witness_left
98. exact hstep2_witness_witness_witness_left
99. have hsum1 : ((((exists fs_h_functional_prefix1_start. fs_h_functional_prefix1_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_functional_prefix1_start. u = fs_q_functional_prefix1_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_functional_prefix1_terminal. fs_h_functional_prefix1_terminal + S (x1) = S ((S (l)) * v)) /\ exists fs_q_functional_prefix1_terminal. u = fs_q_functional_prefix1_terminal * S ((S (l)) * v) + (x1))) /\ forall fs_i_functional_prefix1_steps. (exists fs_lt_functional_prefix1_steps_bound. fs_lt_functional_prefix1_steps_bound + S fs_i_functional_prefix1_steps = l) -> exists fs_a_functional_prefix1_steps fs_r_functional_prefix1_steps fs_s_functional_prefix1_steps. ((((exists fs_h_functional_prefix1_steps_summand. fs_h_functional_prefix1_steps_summand + S (fs_a_functional_prefix1_steps) = S ((S (fs_i_functional_prefix1_steps)) * c)) /\ exists fs_q_functional_prefix1_steps_summand. b = fs_q_functional_prefix1_steps_summand * S ((S (fs_i_functional_prefix1_steps)) * c) + (fs_a_functional_prefix1_steps))) /\ ((((exists fs_h_functional_prefix1_steps_partial. fs_h_functional_prefix1_steps_partial + S (fs_r_functional_prefix1_steps) = S ((S (fs_i_functional_prefix1_steps)) * v)) /\ exists fs_q_functional_prefix1_steps_partial. u = fs_q_functional_prefix1_steps_partial * S ((S (fs_i_functional_prefix1_steps)) * v) + (fs_r_functional_prefix1_steps))) /\ ((((exists fs_h_functional_prefix1_steps_successor. fs_h_functional_prefix1_steps_successor + S (fs_s_functional_prefix1_steps) = S ((S (S fs_i_functional_prefix1_steps)) * v)) /\ exists fs_q_functional_prefix1_steps_successor. u = fs_q_functional_prefix1_steps_successor * S ((S (S fs_i_functional_prefix1_steps)) * v) + (fs_s_functional_prefix1_steps))) /\ fs_s_functional_prefix1_steps = fs_r_functional_prefix1_steps + fs_a_functional_prefix1_steps)))))
100. split
101. exact h1_left
102. split
103. exact hstep1_witness_witness_witness_right_left
104. intro i
105. intro hi
106. specialize h1_right_right i
107. apply h1_right_right
108. specialize le_succ (S i)
109. specialize le_succ l
110. apply le_succ
111. exact hi
112. have hsum2 : ((((exists fs_h_functional_prefix2_start. fs_h_functional_prefix2_start + S (0) = S ((S (0)) * d)) /\ exists fs_q_functional_prefix2_start. w = fs_q_functional_prefix2_start * S ((S (0)) * d) + (0))) /\ ((((exists fs_h_functional_prefix2_terminal. fs_h_functional_prefix2_terminal + S (x4) = S ((S (l)) * d)) /\ exists fs_q_functional_prefix2_terminal. w = fs_q_functional_prefix2_terminal * S ((S (l)) * d) + (x4))) /\ forall fs_i_functional_prefix2_steps. (exists fs_lt_functional_prefix2_steps_bound. fs_lt_functional_prefix2_steps_bound + S fs_i_functional_prefix2_steps = l) -> exists fs_a_functional_prefix2_steps fs_r_functional_prefix2_steps fs_s_functional_prefix2_steps. ((((exists fs_h_functional_prefix2_steps_summand. fs_h_functional_prefix2_steps_summand + S (fs_a_functional_prefix2_steps) = S ((S (fs_i_functional_prefix2_steps)) * c)) /\ exists fs_q_functional_prefix2_steps_summand. b = fs_q_functional_prefix2_steps_summand * S ((S (fs_i_functional_prefix2_steps)) * c) + (fs_a_functional_prefix2_steps))) /\ ((((exists fs_h_functional_prefix2_steps_partial. fs_h_functional_prefix2_steps_partial + S (fs_r_functional_prefix2_steps) = S ((S (fs_i_functional_prefix2_steps)) * d)) /\ exists fs_q_functional_prefix2_steps_partial. w = fs_q_functional_prefix2_steps_partial * S ((S (fs_i_functional_prefix2_steps)) * d) + (fs_r_functional_prefix2_steps))) /\ ((((exists fs_h_functional_prefix2_steps_successor. fs_h_functional_prefix2_steps_successor + S (fs_s_functional_prefix2_steps) = S ((S (S fs_i_functional_prefix2_steps)) * d)) /\ exists fs_q_functional_prefix2_steps_successor. w = fs_q_functional_prefix2_steps_successor * S ((S (S fs_i_functional_prefix2_steps)) * d) + (fs_s_functional_prefix2_steps))) /\ fs_s_functional_prefix2_steps = fs_r_functional_prefix2_steps + fs_a_functional_prefix2_steps)))))
113. split
114. exact h2_left
115. split
116. exact hstep2_witness_witness_witness_right_left
117. intro i
118. intro hi
119. specialize h2_right_right i
120. apply h2_right_right
121. specialize le_succ (S i)
122. specialize le_succ l
123. apply le_succ
124. exact hi
125. have hprev : x1 = x4
126. specialize IH x1
127. specialize IH u
128. specialize IH v
129. specialize IH x4
130. specialize IH w
131. specialize IH d
132. apply IH
133. exact hsum1
134. exact hsum2
135. have hadd : x1 + x = x4 + x3
136. specialize add_congr x1
137. specialize add_congr x4
138. specialize add_congr x
139. specialize add_congr x3
140. apply add_congr
141. exact hprev
142. exact ha
143. trans x2
144. exact hn
145. trans x1 + x
146. exact hstep1_witness_witness_witness_right_right_right
147. trans x4 + x3
148. exact hadd
149. trans x5
150. symm
151. exact hstep2_witness_witness_witness_right_right_right
152. symm
153. exact hm

forall b c l n m. (exists ff_u_l ff_v_l. ((((exists ff_h_l_start. ff_h_l_start + S (0) = S ((S (0)) * ff_v_l)) /\ exists ff_q_l_start. ff_u_l = ff_q_l_start * S ((S (0)) * ff_v_l) + (0))) /\ ((((exists ff_h_l_terminal. ff_h_l_terminal + S (n) = S ((S (l)) * ff_v_l)) /\ exists ff_q_l_terminal. ff_u_l = ff_q_l_terminal * S ((S (l)) * ff_v_l) + (n))) /\ forall ff_i_l. (exists ff_lt_l_bound. ff_lt_l_bound + S ff_i_l = l) -> exists ff_a_l ff_r_l ff_s_l. ((((exists ff_h_l_summand. ff_h_l_summand + S (ff_a_l) = S ((S (ff_i_l)) * c)) /\ exists ff_q_l_summand. b = ff_q_l_summand * S ((S (ff_i_l)) * c) + (ff_a_l))) /\ ((((exists ff_h_l_partial. ff_h_l_partial + S (ff_r_l) = S ((S (ff_i_l)) * ff_v_l)) /\ exists ff_q_l_partial. ff_u_l = ff_q_l_partial * S ((S (ff_i_l)) * ff_v_l) + (ff_r_l))) /\ ((((exists ff_h_l_successor. ff_h_l_successor + S (ff_s_l) = S ((S (S ff_i_l)) * ff_v_l)) /\ exists ff_q_l_successor. ff_u_l = ff_q_l_successor * S ((S (S ff_i_l)) * ff_v_l) + (ff_s_l))) /\ ff_s_l = ff_r_l + ff_a_l)))))) -> (exists ff_u_r ff_v_r. ((((exists ff_h_r_start. ff_h_r_start + S (0) = S ((S (0)) * ff_v_r)) /\ exists ff_q_r_start. ff_u_r = ff_q_r_start * S ((S (0)) * ff_v_r) + (0))) /\ ((((exists ff_h_r_terminal. ff_h_r_terminal + S (m) = S ((S (l)) * ff_v_r)) /\ exists ff_q_r_terminal. ff_u_r = ff_q_r_terminal * S ((S (l)) * ff_v_r) + (m))) /\ forall ff_i_r. (exists ff_lt_r_bound. ff_lt_r_bound + S ff_i_r = l) -> exists ff_a_r ff_r_r ff_s_r. ((((exists ff_h_r_summand. ff_h_r_summand + S (ff_a_r) = S ((S (ff_i_r)) * c)) /\ exists ff_q_r_summand. b = ff_q_r_summand * S ((S (ff_i_r)) * c) + (ff_a_r))) /\ ((((exists ff_h_r_partial. ff_h_r_partial + S (ff_r_r) = S ((S (ff_i_r)) * ff_v_r)) /\ exists ff_q_r_partial. ff_u_r = ff_q_r_partial * S ((S (ff_i_r)) * ff_v_r) + (ff_r_r))) /\ ((((exists ff_h_r_successor. ff_h_r_successor + S (ff_s_r) = S ((S (S ff_i_r)) * ff_v_r)) /\ exists ff_q_r_successor. ff_u_r = ff_q_r_successor * S ((S (S ff_i_r)) * ff_v_r) + (ff_s_r))) /\ ff_s_r = ff_r_r + ff_a_r)))))) -> n = m

1. intro b
2. intro c
3. intro l
4. intro n
5. intro m
6. intro hn
7. intro hm
8. cases hn
9. cases hn_witness
10. cases hm
11. cases hm_witness
12. specialize beta_sum_trace_functional b
13. specialize beta_sum_trace_functional c
14. specialize beta_sum_trace_functional l
15. specialize beta_sum_trace_functional n
16. specialize beta_sum_trace_functional x
17. specialize beta_sum_trace_functional x1
18. specialize beta_sum_trace_functional m
19. specialize beta_sum_trace_functional x2
20. specialize beta_sum_trace_functional x3
21. apply beta_sum_trace_functional
22. exact hn_witness_witness
23. exact hm_witness_witness

forall b c n. (exists fs_u_zero fs_v_zero. ((((exists fs_h_zero_body_start. fs_h_zero_body_start + S (0) = S ((S (0)) * fs_v_zero)) /\ exists fs_q_zero_body_start. fs_u_zero = fs_q_zero_body_start * S ((S (0)) * fs_v_zero) + (0))) /\ ((((exists fs_h_zero_body_terminal. fs_h_zero_body_terminal + S (n) = S ((S (0)) * fs_v_zero)) /\ exists fs_q_zero_body_terminal. fs_u_zero = fs_q_zero_body_terminal * S ((S (0)) * fs_v_zero) + (n))) /\ forall fs_i_zero_body_steps. (exists fs_lt_zero_body_steps_bound. fs_lt_zero_body_steps_bound + S fs_i_zero_body_steps = 0) -> exists fs_a_zero_body_steps fs_r_zero_body_steps fs_s_zero_body_steps. ((((exists fs_h_zero_body_steps_summand. fs_h_zero_body_steps_summand + S (fs_a_zero_body_steps) = S ((S (fs_i_zero_body_steps)) * c)) /\ exists fs_q_zero_body_steps_summand. b = fs_q_zero_body_steps_summand * S ((S (fs_i_zero_body_steps)) * c) + (fs_a_zero_body_steps))) /\ ((((exists fs_h_zero_body_steps_partial. fs_h_zero_body_steps_partial + S (fs_r_zero_body_steps) = S ((S (fs_i_zero_body_steps)) * fs_v_zero)) /\ exists fs_q_zero_body_steps_partial. fs_u_zero = fs_q_zero_body_steps_partial * S ((S (fs_i_zero_body_steps)) * fs_v_zero) + (fs_r_zero_body_steps))) /\ ((((exists fs_h_zero_body_steps_successor. fs_h_zero_body_steps_successor + S (fs_s_zero_body_steps) = S ((S (S fs_i_zero_body_steps)) * fs_v_zero)) /\ exists fs_q_zero_body_steps_successor. fs_u_zero = fs_q_zero_body_steps_successor * S ((S (S fs_i_zero_body_steps)) * fs_v_zero) + (fs_s_zero_body_steps))) /\ fs_s_zero_body_steps = fs_r_zero_body_steps + fs_a_zero_body_steps)))))) -> n = 0

1. intro b
2. intro c
3. intro n
4. intro hsum
5. cases hsum
6. cases hsum_witness
7. cases hsum_witness_witness
8. cases hsum_witness_witness_right
9. specialize beta_at_unique x
10. specialize beta_at_unique x1
11. specialize beta_at_unique 0
12. specialize beta_at_unique n
13. specialize beta_at_unique 0
14. apply beta_at_unique
15. exact hsum_witness_witness_right_left
16. exact hsum_witness_witness_left

forall b c l n. (exists fs_u_succ fs_v_succ. ((((exists fs_h_succ_body_start. fs_h_succ_body_start + S (0) = S ((S (0)) * fs_v_succ)) /\ exists fs_q_succ_body_start. fs_u_succ = fs_q_succ_body_start * S ((S (0)) * fs_v_succ) + (0))) /\ ((((exists fs_h_succ_body_terminal. fs_h_succ_body_terminal + S (n) = S ((S (S l)) * fs_v_succ)) /\ exists fs_q_succ_body_terminal. fs_u_succ = fs_q_succ_body_terminal * S ((S (S l)) * fs_v_succ) + (n))) /\ forall fs_i_succ_body_steps. (exists fs_lt_succ_body_steps_bound. fs_lt_succ_body_steps_bound + S fs_i_succ_body_steps = S l) -> exists fs_a_succ_body_steps fs_r_succ_body_steps fs_s_succ_body_steps. ((((exists fs_h_succ_body_steps_summand. fs_h_succ_body_steps_summand + S (fs_a_succ_body_steps) = S ((S (fs_i_succ_body_steps)) * c)) /\ exists fs_q_succ_body_steps_summand. b = fs_q_succ_body_steps_summand * S ((S (fs_i_succ_body_steps)) * c) + (fs_a_succ_body_steps))) /\ ((((exists fs_h_succ_body_steps_partial. fs_h_succ_body_steps_partial + S (fs_r_succ_body_steps) = S ((S (fs_i_succ_body_steps)) * fs_v_succ)) /\ exists fs_q_succ_body_steps_partial. fs_u_succ = fs_q_succ_body_steps_partial * S ((S (fs_i_succ_body_steps)) * fs_v_succ) + (fs_r_succ_body_steps))) /\ ((((exists fs_h_succ_body_steps_successor. fs_h_succ_body_steps_successor + S (fs_s_succ_body_steps) = S ((S (S fs_i_succ_body_steps)) * fs_v_succ)) /\ exists fs_q_succ_body_steps_successor. fs_u_succ = fs_q_succ_body_steps_successor * S ((S (S fs_i_succ_body_steps)) * fs_v_succ) + (fs_s_succ_body_steps))) /\ fs_s_succ_body_steps = fs_r_succ_body_steps + fs_a_succ_body_steps)))))) -> exists a r. (((exists fs_h_succ_factor. fs_h_succ_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_succ_factor. b = fs_q_succ_factor * S ((S (l)) * c) + (a))) /\ ((exists ff_u_prefix ff_v_prefix. ((((exists ff_h_prefix_start. ff_h_prefix_start + S (0) = S ((S (0)) * ff_v_prefix)) /\ exists ff_q_prefix_start. ff_u_prefix = ff_q_prefix_start * S ((S (0)) * ff_v_prefix) + (0))) /\ ((((exists ff_h_prefix_terminal. ff_h_prefix_terminal + S (r) = S ((S (l)) * ff_v_prefix)) /\ exists ff_q_prefix_terminal. ff_u_prefix = ff_q_prefix_terminal * S ((S (l)) * ff_v_prefix) + (r))) /\ forall ff_i_prefix. (exists ff_lt_prefix_bound. ff_lt_prefix_bound + S ff_i_prefix = l) -> exists ff_a_prefix ff_r_prefix ff_s_prefix. ((((exists ff_h_prefix_summand. ff_h_prefix_summand + S (ff_a_prefix) = S ((S (ff_i_prefix)) * c)) /\ exists ff_q_prefix_summand. b = ff_q_prefix_summand * S ((S (ff_i_prefix)) * c) + (ff_a_prefix))) /\ ((((exists ff_h_prefix_partial. ff_h_prefix_partial + S (ff_r_prefix) = S ((S (ff_i_prefix)) * ff_v_prefix)) /\ exists ff_q_prefix_partial. ff_u_prefix = ff_q_prefix_partial * S ((S (ff_i_prefix)) * ff_v_prefix) + (ff_r_prefix))) /\ ((((exists ff_h_prefix_successor. ff_h_prefix_successor + S (ff_s_prefix) = S ((S (S ff_i_prefix)) * ff_v_prefix)) /\ exists ff_q_prefix_successor. ff_u_prefix = ff_q_prefix_successor * S ((S (S ff_i_prefix)) * ff_v_prefix) + (ff_s_prefix))) /\ ff_s_prefix = ff_r_prefix + ff_a_prefix)))))) /\ n = r + a)

1. intro b
2. intro c
3. intro l
4. intro n
5. intro hsum
6. cases hsum
7. cases hsum_witness
8. cases hsum_witness_witness
9. cases hsum_witness_witness_right
10. have hstep : exists a r s. ((((exists fs_h_decomp_factor. fs_h_decomp_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_decomp_factor. b = fs_q_decomp_factor * S ((S (l)) * c) + (a))) /\ ((((exists fs_h_decomp_partial. fs_h_decomp_partial + S (r) = S ((S (l)) * x1)) /\ exists fs_q_decomp_partial. x = fs_q_decomp_partial * S ((S (l)) * x1) + (r))) /\ ((((exists fs_h_decomp_successor. fs_h_decomp_successor + S (s) = S ((S (S l)) * x1)) /\ exists fs_q_decomp_successor. x = fs_q_decomp_successor * S ((S (S l)) * x1) + (s))) /\ s = r + a)))
11. specialize hsum_witness_witness_right_right l
12. apply hsum_witness_witness_right_right
13. specialize le_refl (S l)
14. exact le_refl
15. cases hstep
16. cases hstep_witness
17. cases hstep_witness_witness
18. cases hstep_witness_witness_witness
19. cases hstep_witness_witness_witness_right
20. cases hstep_witness_witness_witness_right_right
21. have hn : n = x4
22. specialize beta_at_unique x
23. specialize beta_at_unique x1
24. specialize beta_at_unique (S l)
25. specialize beta_at_unique n
26. specialize beta_at_unique x4
27. apply beta_at_unique
28. exact hsum_witness_witness_right_left
29. exact hstep_witness_witness_witness_right_right_left
30. exists x2
31. exists x3
32. split
33. exact hstep_witness_witness_witness_left
34. split
35. exists x
36. exists x1
37. split
38. exact hsum_witness_witness_left
39. split
40. exact hstep_witness_witness_witness_right_left
41. intro i
42. intro hi
43. specialize hsum_witness_witness_right_right i
44. apply hsum_witness_witness_right_right
45. specialize le_succ (S i)
46. specialize le_succ l
47. apply le_succ
48. exact hi
49. trans x4
50. exact hn
51. exact hstep_witness_witness_witness_right_right_right

forall p a. (~(p = 1) /\ forall c e. p = c * e -> c = 1 \/ e = 1) -> (forall d. (exists x. p = d * x) -> (exists y. a = d * y) -> d = 1) \/ exists k. a = p * k

1. intro p
2. intro a
3. intro hp
4. have hg : exists g. (((exists x. p = g * x) /\ (exists y. a = g * y)) /\ forall c. (exists u. p = c * u) -> (exists v. a = c * v) -> exists w. g = c * w)
5. apply gcd_exists_relational
6. cases hg
7. have hgfull : (((exists u. p = x * u) /\ (exists v. a = x * v)) /\ forall c. (exists s. p = c * s) -> (exists t. a = c * t) -> exists w. x = c * w)
8. exact hg_witness
9. cases hg_witness
10. cases hg_witness_left
11. have hfactor : x = 1 \/ p = x
12. specialize prime_divisor_eq_one_or_self p
13. specialize prime_divisor_eq_one_or_self x
14. apply prime_divisor_eq_one_or_self
15. exact hp
16. exact hg_witness_left_left
17. cases hfactor
18. left
19. apply is_gcd_one_to_coprime
20. have hg1 : (((exists u. p = 1 * u) /\ (exists v. a = 1 * v)) /\ forall c. (exists s. p = c * s) -> (exists t. a = c * t) -> exists w. 1 = c * w)
21. rewrite <- hfactor_left
22. rewrite <- hfactor_left
23. rewrite <- hfactor_left
24. exact hgfull
25. exact hg1
26. right
27. cases hg_witness_left_right
28. exists x1
29. rewrite hfactor_right
30. exact hg_witness_left_right_witness

forall p a. (~(p = 1) /\ forall c e. p = c * e -> c = 1 \/ e = 1) -> ~(exists k. a = p * k) -> forall d. (exists x. p = d * x) -> (exists y. a = d * y) -> d = 1

1. intro p
2. intro a
3. intro hp
4. intro hnot
5. specialize prime_coprime_or_divides p
6. specialize prime_coprime_or_divides a
7. have hsplit : (forall d. (exists x. p = d * x) -> (exists y. a = d * y) -> d = 1) \/ exists k. a = p * k
8. apply prime_coprime_or_divides
9. exact hp
10. cases hsplit
11. exact hsplit_left
12. exfalso
13. apply hnot
14. exact hsplit_right

forall a m. (forall d. (exists x. a = d * x) -> (exists y. m = d * y) -> d = 1) -> exists xp xn u v. a * xp + m * u = (1 + a * xn) + m * v

1. intro a
2. intro m
3. intro hcop
4. have hbez : exists xp yp xn yn. a * xp + m * yp = 1 + (a * xn + m * yn)
5. specialize coprime_balanced_bezout a
6. specialize coprime_balanced_bezout m
7. apply coprime_balanced_bezout
8. exact hcop
9. cases hbez
10. cases hbez_witness
11. cases hbez_witness_witness
12. cases hbez_witness_witness_witness
13. exists x
14. exists x2
15. exists x1
16. exists x3
17. trans 1 + (a * x2 + m * x3)
18. exact hbez_witness_witness_witness_witness
19. symm
20. apply add_assoc

forall a m. ~(m = 0) -> (forall d. (exists x. a = d * x) -> (exists y. m = d * y) -> d = 1) -> exists z u v. a * z + m * u = 1 + m * v

1. intro a
2. intro m
3. intro hm
4. intro hcop
5. have hms : exists k. m = S k
6. specialize nonzero_is_succ m
7. apply nonzero_is_succ
8. exact hm
9. have hbal : exists xp xn u v. a * xp + m * u = (1 + a * xn) + m * v
10. specialize coprime_balanced_mod_inverse a
11. specialize coprime_balanced_mod_inverse m
12. apply coprime_balanced_mod_inverse
13. exact hcop
14. cases hms
15. cases hbal
16. cases hbal_witness
17. cases hbal_witness_witness
18. cases hbal_witness_witness_witness
19. have hself : exists u v. (x * (a * x2)) + m * u = (x * (a * x2)) + m * v
20. specialize mod_eq_refl m
21. specialize mod_eq_refl (x * (a * x2))
22. apply mod_eq_refl
23. have hadd : exists u v. ((a * x1) + x * (a * x2)) + m * u = ((1 + a * x2) + x * (a * x2)) + m * v
24. specialize mod_eq_add m
25. specialize mod_eq_add (a * x1)
26. specialize mod_eq_add (1 + a * x2)
27. specialize mod_eq_add (x * (a * x2))
28. specialize mod_eq_add (x * (a * x2))
29. apply mod_eq_add
30. exists x3
31. exists x4
32. exact hbal_witness_witness_witness_witness
33. exact hself
34. have hcancel : exists u v. ((1 + a * x2) + x * (a * x2)) + m * u = 1 + m * v
35. specialize mod_eq_predecessor_cancel x
36. specialize mod_eq_predecessor_cancel 1
37. specialize mod_eq_predecessor_cancel (a * x2)
38. have hkcancel : exists u v. ((1 + a * x2) + x * (a * x2)) + S x * u = 1 + S x * v
39. apply mod_eq_predecessor_cancel
40. rewrite <- hms_witness at hkcancel
41. rewrite <- hms_witness at hkcancel
42. exact hkcancel
43. have hfinal : exists u v. ((a * x1) + x * (a * x2)) + m * u = 1 + m * v
44. specialize mod_eq_trans m
45. specialize mod_eq_trans ((a * x1) + x * (a * x2))
46. specialize mod_eq_trans ((1 + a * x2) + x * (a * x2))
47. specialize mod_eq_trans 1
48. apply mod_eq_trans
49. exact hadd
50. exact hcancel
51. have hnorm : a * (x1 + x * x2) = (a * x1) + x * (a * x2)
52. trans a * x1 + a * (x * x2)
53. apply mul_add
54. congr
55. refl
56. trans (a * x) * x2
57. symm
58. apply mul_assoc
59. trans (x * a) * x2
60. congr
61. apply mul_comm
62. refl
63. apply mul_assoc
64. exists x1 + x * x2
65. rewrite hnorm
66. exact hfinal