Congruence Arithmetic — 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 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 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 b c. ~(a = 0) -> a * b = a * c -> b = c

1. intro a
2. induction b
3. intro c
4. intro ha
5. intro h
6. have hz : a * c = 0
7. symm
8. rewrite PA5 at h
9. exact h
10. have factors : a = 0 \/ c = 0
11. specialize mul_eq_zero a
12. specialize mul_eq_zero c
13. apply mul_eq_zero
14. exact hz
15. cases factors
16. exfalso
17. apply ha
18. exact factors_left
19. symm
20. exact factors_right
21. intro c
22. induction c
23. intro ha
24. intro h
25. exfalso
26. specialize mul_ne_zero a
27. specialize mul_ne_zero (S b)
28. apply mul_ne_zero
29. exact ha
30. specialize succ_ne_zero b
31. exact succ_ne_zero
32. rewrite PA5 at h
33. exact h
34. intro ha
35. intro h
36. congr
37. apply IH
38. exact ha
39. apply add_right_cancel
40. rewrite PA6 at h
41. rewrite PA6 at h
42. exact h

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 n m. (exists q. n = a * q) -> exists s. m * n = a * s

1. intro a
2. intro n
3. intro m
4. intro hn
5. suffices hswap : m * n = n * m
6. rewrite hswap
7. apply multiple_mul_right
8. exact hn
9. apply mul_comm

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 a b. (exists x. b = a * x) -> (exists y. a = b * y) -> a = b

1. intro a
2. intro b
3. intro hab
4. intro hba
5. cases hab
6. cases hba
7. specialize zero_or_succ a
8. cases zero_or_succ
9. rewrite zero_or_succ_left
10. rewrite zero_or_succ_left at hab_witness
11. specialize mul_zero_left x
12. rewrite mul_zero_left at hab_witness
13. symm
14. exact hab_witness
15. cases zero_or_succ_right
16. have ha : ~(a = 0)
17. intro ha0
18. rewrite zero_or_succ_right_witness at ha0
19. apply PA1
20. exact ha0
21. have hcycle : a = a * (x * x1)
22. trans b * x1
23. exact hba_witness
24. trans (a * x) * x1
25. congr
26. exact hab_witness
27. refl
28. apply mul_assoc
29. specialize mul_left_cancel_nonzero a
30. specialize mul_left_cancel_nonzero 1
31. specialize mul_left_cancel_nonzero (x * x1)
32. have hunit : 1 = x * x1
33. apply mul_left_cancel_nonzero
34. exact ha
35. specialize mul_one a
36. trans a
37. apply mul_one
38. exact hcycle
39. specialize mul_eq_one_components x
40. specialize mul_eq_one_components x1
41. have hparts : x = 1 /\ x1 = 1
42. apply mul_eq_one_components
43. symm
44. exact hunit
45. cases hparts
46. symm
47. trans a * x
48. exact hab_witness
49. rewrite hparts_left
50. apply mul_one

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 g a b. (((exists x. a = g * x) /\ (exists y. b = g * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. g = c * w) -> ((exists x. b = g * x) /\ (exists y. a = g * y)) /\ forall c. (exists u. b = c * u) -> (exists v. a = c * v) -> exists w. g = c * w

1. intro g
2. intro a
3. intro b
4. intro h
5. cases h
6. cases h_left
7. split
8. split
9. exact h_left_right
10. exact h_left_left
11. intro c
12. intro hb
13. intro ha
14. specialize h_right c
15. apply h_right
16. exact ha
17. exact hb

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

1. intro g
2. intro a
3. intro b
4. intro h
5. cases h
6. cases h_left
7. exact h_left_left

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

1. intro g
2. intro a
3. intro b
4. intro h
5. cases h
6. cases h_left
7. exact h_left_right

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

1. intro g
2. intro a
3. intro b
4. intro c
5. intro h
6. intro ha
7. intro hb
8. cases h
9. specialize h_right c
10. apply h_right
11. exact ha
12. exact hb

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

1. intro g
2. intro h
3. intro a
4. intro b
5. intro hg
6. intro hh
7. cases hg
8. cases hg_left
9. cases hh
10. cases hh_left
11. specialize hg_right h
12. have hdg : exists w. g = h * w
13. apply hg_right
14. exact hh_left_left
15. exact hh_left_right
16. specialize hh_right g
17. have gdh : exists w. h = g * w
18. apply hh_right
19. exact hg_left_left
20. exact hg_left_right
21. specialize multiple_antisymm g
22. specialize multiple_antisymm h
23. apply multiple_antisymm
24. exact gdh
25. exact hdg

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 b. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> forall c. (exists u. b = c * u) -> (exists v. a = c * v) -> c = 1

1. intro a
2. intro b
3. intro h
4. intro c
5. intro hb
6. intro ha
7. specialize h c
8. apply h
9. exact ha
10. exact hb

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 p a b. (~(p = 1) /\ forall c d. p = c * d -> c = 1 \/ d = 1) -> (exists k. a * b = p * k) -> (exists u. a = p * u) \/ exists v. b = p * v

1. intro p
2. intro a
3. intro b
4. intro hp
5. intro hab
6. 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)
7. apply gcd_exists_relational
8. cases hg
9. 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)
10. exact hg_witness
11. cases hg_witness
12. cases hg_witness_left
13. have hfactor : x = 1 \/ p = x
14. specialize prime_divisor_eq_one_or_self p
15. specialize prime_divisor_eq_one_or_self x
16. apply prime_divisor_eq_one_or_self
17. exact hp
18. exact hg_witness_left_left
19. cases hfactor
20. right
21. apply gauss_coprime_cancel
22. have hcop : forall d. (exists u. p = d * u) -> (exists v. a = d * v) -> d = 1
23. apply is_gcd_one_to_coprime
24. 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)
25. rewrite <- hfactor_left
26. rewrite <- hfactor_left
27. rewrite <- hfactor_left
28. exact hgfull
29. exact hg1
30. exact hcop
31. exact hab
32. left
33. cases hg_witness_left_right
34. exists x1
35. rewrite hfactor_right
36. exact hg_witness_left_right_witness

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 l. exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S (S i)) * v)) /\ exists q. u = q * S ((S (S i)) * v) + s) /\ s = r * p))))

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

forall b c l. exists n u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S (S i)) * v)) /\ exists q. u = q * S ((S (S i)) * v) + s) /\ s = r * p)))))

1. intro b
2. intro c
3. intro l
4. have htrace : exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S (S i)) * v)) /\ exists q. u = q * S ((S (S i)) * v) + s) /\ s = r * p))))
5. specialize beta_prefix_product_trace_exists b
6. specialize beta_prefix_product_trace_exists c
7. specialize beta_prefix_product_trace_exists l
8. exact beta_prefix_product_trace_exists
9. cases htrace
10. cases htrace_witness
11. cases htrace_witness_witness
12. have hterminal : exists n. ((exists h. h + S n = S ((S l) * x1)) /\ exists q. x = q * 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 h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p))))) -> (((exists h. h + S 1 = S ((S 0) * d)) /\ exists q. w = q * S ((S 0) * d) + 1) /\ (((exists h. h + S m = S ((S l) * d)) /\ exists q. w = q * S ((S l) * d) + m) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * d)) /\ exists q. w = q * S ((S i) * d) + r) /\ (((exists h. h + S s = S ((S S i) * d)) /\ exists q. w = q * S ((S S i) * d) + s) /\ s = r * p))))) -> 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 = 1
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 1
22. apply beta_at_unique
23. exact h1_right_left
24. exact h1_left
25. have hm : m = 1
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 1
31. apply beta_at_unique
32. exact h2_right_left
33. exact h2_left
34. trans 1
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 p r s. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ (((exists h. h + S r = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + r) /\ (((exists h. h + S s = S ((S S l) * v)) /\ exists q. u = q * S ((S S l) * v) + s) /\ s = r * p)))
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 p r s. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ (((exists h. h + S r = S ((S l) * d)) /\ exists q. w = q * S ((S l) * d) + r) /\ (((exists h. h + S s = S ((S S l) * d)) /\ exists q. w = q * S ((S S l) * d) + s) /\ s = r * p)))
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 hp : 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 hprod1 : (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S x1 = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + x1) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))
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 hprod2 : (((exists h. h + S 1 = S ((S 0) * d)) /\ exists q. w = q * S ((S 0) * d) + 1) /\ (((exists h. h + S x4 = S ((S l) * d)) /\ exists q. w = q * S ((S l) * d) + x4) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * d)) /\ exists q. w = q * S ((S i) * d) + r) /\ (((exists h. h + S s = S ((S S i) * d)) /\ exists q. w = q * S ((S S i) * d) + s) /\ s = r * p)))))
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 hprod1
134. exact hprod2
135. have hmul : x1 * x = x4 * x3
136. specialize mul_congr x1
137. specialize mul_congr x4
138. specialize mul_congr x
139. specialize mul_congr x3
140. apply mul_congr
141. exact hprev
142. exact hp
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 hmul
149. trans x5
150. symm
151. exact hstep2_witness_witness_witness_right_right_right
152. symm
153. exact hm

forall b c n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + n) /\ forall i. (exists h. h + S i = 0) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> n = 1

1. intro b
2. intro c
3. intro n
4. intro hproduct
5. cases hproduct
6. cases hproduct_witness
7. cases hproduct_witness_witness
8. cases hproduct_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 1
14. apply beta_at_unique
15. exact hproduct_witness_witness_right_left
16. exact hproduct_witness_witness_left

forall b c l n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S S l) * v)) /\ exists q. u = q * S ((S S l) * v) + n) /\ forall i. (exists h. h + S i = S l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> exists p r. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ ((exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S r = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + r) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) /\ n = r * p))

1. intro b
2. intro c
3. intro l
4. intro n
5. intro hproduct
6. cases hproduct
7. cases hproduct_witness
8. cases hproduct_witness_witness
9. cases hproduct_witness_witness_right
10. have hstep : exists p r s. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ (((exists h. h + S r = S ((S l) * x1)) /\ exists q. x = q * S ((S l) * x1) + r) /\ (((exists h. h + S s = S ((S S l) * x1)) /\ exists q. x = q * S ((S S l) * x1) + s) /\ s = r * p)))
11. specialize hproduct_witness_witness_right_right l
12. apply hproduct_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 hproduct_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 hproduct_witness_witness_left
39. split
40. exact hstep_witness_witness_witness_right_left
41. intro i
42. intro hi
43. specialize hproduct_witness_witness_right_right i
44. apply hproduct_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 b c z e l n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> (forall i a. (exists h. h + S i = l) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + a) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + a)) -> (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p))))))

1. intro b
2. intro c
3. intro z
4. intro e
5. intro l
6. intro n
7. intro hproduct
8. intro hpres
9. cases hproduct
10. cases hproduct_witness
11. cases hproduct_witness_witness
12. cases hproduct_witness_witness_right
13. exists x
14. exists x1
15. split
16. exact hproduct_witness_witness_left
17. split
18. exact hproduct_witness_witness_right_left
19. intro i
20. intro hi
21. have hstep : exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + r) /\ (((exists h. h + S s = S ((S S i) * x1)) /\ exists q. x = q * S ((S S i) * x1) + s) /\ s = r * p)))
22. specialize hproduct_witness_witness_right_right i
23. apply hproduct_witness_witness_right_right
24. exact hi
25. cases hstep
26. cases hstep_witness
27. cases hstep_witness_witness
28. cases hstep_witness_witness_witness
29. cases hstep_witness_witness_witness_right
30. cases hstep_witness_witness_witness_right_right
31. exists x2
32. exists x3
33. exists x4
34. split
35. specialize hpres i
36. specialize hpres x2
37. apply hpres
38. exact hi
39. exact hstep_witness_witness_witness_left
40. split
41. exact hstep_witness_witness_witness_right_left
42. split
43. exact hstep_witness_witness_witness_right_right_left
44. exact hstep_witness_witness_witness_right_right_right

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 a e n. e = 0 -> (exists ff_b_z ff_c_z. ((forall ff_i_z_repeat. (exists ff_lt_z_repeat_bound. ff_lt_z_repeat_bound + S ff_i_z_repeat = e) -> (((exists ff_h_z_repeat_decoded. ff_h_z_repeat_decoded + S (a) = S ((S (ff_i_z_repeat)) * ff_c_z)) /\ exists ff_q_z_repeat_decoded. ff_b_z = ff_q_z_repeat_decoded * S ((S (ff_i_z_repeat)) * ff_c_z) + (a)))) /\ (exists ff_u_z_product ff_v_z_product. ((((exists ff_h_z_product_start. ff_h_z_product_start + S (1) = S ((S (0)) * ff_v_z_product)) /\ exists ff_q_z_product_start. ff_u_z_product = ff_q_z_product_start * S ((S (0)) * ff_v_z_product) + (1))) /\ ((((exists ff_h_z_product_terminal. ff_h_z_product_terminal + S (n) = S ((S (e)) * ff_v_z_product)) /\ exists ff_q_z_product_terminal. ff_u_z_product = ff_q_z_product_terminal * S ((S (e)) * ff_v_z_product) + (n))) /\ forall ff_i_z_product. (exists ff_lt_z_product_bound. ff_lt_z_product_bound + S ff_i_z_product = e) -> exists ff_p_z_product ff_r_z_product ff_s_z_product. ((((exists ff_h_z_product_factor. ff_h_z_product_factor + S (ff_p_z_product) = S ((S (ff_i_z_product)) * ff_c_z)) /\ exists ff_q_z_product_factor. ff_b_z = ff_q_z_product_factor * S ((S (ff_i_z_product)) * ff_c_z) + (ff_p_z_product))) /\ ((((exists ff_h_z_product_partial. ff_h_z_product_partial + S (ff_r_z_product) = S ((S (ff_i_z_product)) * ff_v_z_product)) /\ exists ff_q_z_product_partial. ff_u_z_product = ff_q_z_product_partial * S ((S (ff_i_z_product)) * ff_v_z_product) + (ff_r_z_product))) /\ ((((exists ff_h_z_product_successor. ff_h_z_product_successor + S (ff_s_z_product) = S ((S (S ff_i_z_product)) * ff_v_z_product)) /\ exists ff_q_z_product_successor. ff_u_z_product = ff_q_z_product_successor * S ((S (S ff_i_z_product)) * ff_v_z_product) + (ff_s_z_product))) /\ ff_s_z_product = ff_r_z_product * ff_p_z_product)))))))) -> n = 1

1. intro a
2. intro e
3. intro n
4. intro he
5. intro hpow
6. rewrite he at hpow
7. rewrite he at hpow
8. rewrite he at hpow
9. rewrite he at hpow
10. cases hpow
11. cases hpow_witness
12. cases hpow_witness_witness
13. specialize beta_product_zero x
14. specialize beta_product_zero x1
15. specialize beta_product_zero n
16. apply beta_product_zero
17. exact hpow_witness_witness_right