FC000B

crt_prefix_gcd_congruences_lcm

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

Induction over every finite decoded modulus list lifts pointwise gcd congruences to congruence modulo the gcd of its exact list LCM; zero moduli and the empty list are included.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall b c l n u v L g. (((forall gcrt_common_index_gfull_prefix_lcm_own gcrt_common_modulus_gfull_prefix_lcm_own. (exists ff_lt_gcrt_gfull_prefix_lcm_own_bound. ff_lt_gcrt_gfull_prefix_lcm_own_bound + S gcrt_common_index_gfull_prefix_lcm_own = l) -> (((exists ff_h_gcrt_gfull_prefix_lcm_own_entry. ff_h_gcrt_gfull_prefix_lcm_own_entry + S (gcrt_common_modulus_gfull_prefix_lcm_own) = S ((S (gcrt_common_index_gfull_prefix_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_prefix_lcm_own_entry. b = ff_q_gcrt_gfull_prefix_lcm_own_entry * S ((S (gcrt_common_index_gfull_prefix_lcm_own)) * c) + (gcrt_common_modulus_gfull_prefix_lcm_own))) -> exists gcrt_common_quotient_gfull_prefix_lcm_own. L = gcrt_common_modulus_gfull_prefix_lcm_own * gcrt_common_quotient_gfull_prefix_lcm_own) /\ forall gcrt_lcm_common_gfull_prefix_lcm. (forall gcrt_common_index_gfull_prefix_lcm_other gcrt_common_modulus_gfull_prefix_lcm_other. (exists ff_lt_gcrt_gfull_prefix_lcm_other_bound. ff_lt_gcrt_gfull_prefix_lcm_other_bound + S gcrt_common_index_gfull_prefix_lcm_other = l) -> (((exists ff_h_gcrt_gfull_prefix_lcm_other_entry. ff_h_gcrt_gfull_prefix_lcm_other_entry + S (gcrt_common_modulus_gfull_prefix_lcm_other) = S ((S (gcrt_common_index_gfull_prefix_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_prefix_lcm_other_entry. b = ff_q_gcrt_gfull_prefix_lcm_other_entry * S ((S (gcrt_common_index_gfull_prefix_lcm_other)) * c) + (gcrt_common_modulus_gfull_prefix_lcm_other))) -> exists gcrt_common_quotient_gfull_prefix_lcm_other. gcrt_lcm_common_gfull_prefix_lcm = gcrt_common_modulus_gfull_prefix_lcm_other * gcrt_common_quotient_gfull_prefix_lcm_other) -> exists gcrt_lcm_quotient_gfull_prefix_lcm. gcrt_lcm_common_gfull_prefix_lcm = L * gcrt_lcm_quotient_gfull_prefix_lcm)) -> (forall gfull_index_prefix_pointwise gfull_modulus_prefix_pointwise gfull_gcd_prefix_pointwise. (exists ff_lt_gcrt_gfull_prefix_pointwise_bound. ff_lt_gcrt_gfull_prefix_pointwise_bound + S gfull_index_prefix_pointwise = l) -> (((exists ff_h_gcrt_gfull_prefix_pointwise_entry. ff_h_gcrt_gfull_prefix_pointwise_entry + S (gfull_modulus_prefix_pointwise) = S ((S (gfull_index_prefix_pointwise)) * c)) /\ exists ff_q_gcrt_gfull_prefix_pointwise_entry. b = ff_q_gcrt_gfull_prefix_pointwise_entry * S ((S (gfull_index_prefix_pointwise)) * c) + (gfull_modulus_prefix_pointwise))) -> ((((exists ec_gcd_left_gfull_prefix_pointwise_gcd. gfull_modulus_prefix_pointwise = gfull_gcd_prefix_pointwise * ec_gcd_left_gfull_prefix_pointwise_gcd) /\ (exists ec_gcd_right_gfull_prefix_pointwise_gcd. n = gfull_gcd_prefix_pointwise * ec_gcd_right_gfull_prefix_pointwise_gcd)) /\ forall ec_gcd_common_gfull_prefix_pointwise_gcd. (exists ec_gcd_common_left_gfull_prefix_pointwise_gcd. gfull_modulus_prefix_pointwise = ec_gcd_common_gfull_prefix_pointwise_gcd * ec_gcd_common_left_gfull_prefix_pointwise_gcd) -> (exists ec_gcd_common_right_gfull_prefix_pointwise_gcd. n = ec_gcd_common_gfull_prefix_pointwise_gcd * ec_gcd_common_right_gfull_prefix_pointwise_gcd) -> exists ec_gcd_greatest_gfull_prefix_pointwise_gcd. gfull_gcd_prefix_pointwise = ec_gcd_common_gfull_prefix_pointwise_gcd * ec_gcd_greatest_gfull_prefix_pointwise_gcd)) -> (exists hgcrt_mod_left_gfull_prefix_pointwise_mod hgcrt_mod_right_gfull_prefix_pointwise_mod. u + gfull_gcd_prefix_pointwise * hgcrt_mod_left_gfull_prefix_pointwise_mod = v + gfull_gcd_prefix_pointwise * hgcrt_mod_right_gfull_prefix_pointwise_mod)) -> ((((exists ec_gcd_left_gfull_prefix_final_gcd. L = g * ec_gcd_left_gfull_prefix_final_gcd) /\ (exists ec_gcd_right_gfull_prefix_final_gcd. n = g * ec_gcd_right_gfull_prefix_final_gcd)) /\ forall ec_gcd_common_gfull_prefix_final_gcd. (exists ec_gcd_common_left_gfull_prefix_final_gcd. L = ec_gcd_common_gfull_prefix_final_gcd * ec_gcd_common_left_gfull_prefix_final_gcd) -> (exists ec_gcd_common_right_gfull_prefix_final_gcd. n = ec_gcd_common_gfull_prefix_final_gcd * ec_gcd_common_right_gfull_prefix_final_gcd) -> exists ec_gcd_greatest_gfull_prefix_final_gcd. g = ec_gcd_common_gfull_prefix_final_gcd * ec_gcd_greatest_gfull_prefix_final_gcd)) -> (exists hgcrt_mod_left_gfull_prefix_final_mod hgcrt_mod_right_gfull_prefix_final_mod. u + g * hgcrt_mod_left_gfull_prefix_final_mod = v + g * hgcrt_mod_right_gfull_prefix_final_mod)

Constructive proof overview

Generated structural guide

Induction over every finite decoded modulus list lifts pointwise gcd congruences to congruence modulo the gcd of its exact list LCM; zero moduli and the empty list are included.

The unchanged tactic script uses 13 declared prerequisites and contains 135 exact native proof lines.

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

Proof neighborhood

Direct dependencies

crt_prefix_lcm_unique Alpha theorem; checked-use authorized crt_prefix_lcm_empty Alpha theorem; checked-use authorized canonical_gcd_one_left_iff Alpha theorem; checked-use authorized crt_mod_one_universal Alpha theorem; checked-use authorized crt_prefix_lcm_exists_unique Alpha theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized lcm_exists_relational Stable theorem; checked-use authorized crt_prefix_lcm_successor_intro Alpha theorem; checked-use authorized canonical_gcd_exists Alpha theorem; checked-use authorized FC000A crt_prefix_gcd_congruences_drop_last FC0009 crt_gcd_lcm_distributes mod_eq_lcm_merge Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized

Direct dependents

FC000D crt_pairwise_compatible_prefix_implies_merge_compatible

Formal native tactic body

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

Read the argument

Proof checkpoints

135 script commands · 31 reading checkpoints · 9 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
crt prefix gcd congruences drop lastcrt gcd lcm distributes

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

01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–11

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

  1. L3
    induction l
  2. L4
    intro n
  3. L5
    intro u
  4. L6
    intro v
  5. L7
    intro L
  6. L8
    intro g
  7. L9
    intro hL
  8. L10
    intro hp
  9. L11
    intro hg
03Establish hLoneL12–21

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

  1. L12
    have hLone : L = 1
  2. L13
    specialize crt_prefix_lcm_unique b
  3. L14
    specialize crt_prefix_lcm_unique c
  4. L15
    specialize crt_prefix_lcm_unique 0
  5. L16
    specialize crt_prefix_lcm_unique L
  6. L17
    specialize crt_prefix_lcm_unique 1
  7. L18
    apply crt_prefix_lcm_unique
  8. L19
    exact hL
  9. L20
    specialize crt_prefix_lcm_empty b
  10. L21
    specialize crt_prefix_lcm_empty c
04Use earlier factsL22–22

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

  1. L22
    apply crt_prefix_lcm_empty
05Establish hgoneL23–25

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

  1. L23
    have hgone : g = 1
  2. L24
    specialize canonical_gcd_one_left_iff n
  3. L25
    specialize canonical_gcd_one_left_iff g
06Separate the logical casesL26–26

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

  1. L26
    cases canonical_gcd_one_left_iff
07Use earlier factsL27–27

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

  1. L27
    apply canonical_gcd_one_left_iff_left
08Calculate and transport equalitiesL28–29

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

  1. L28
    rewrite <- hLone
  2. L29
    rewrite <- hLone
09Use earlier factsL30–30

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

  1. L30
    exact hg
10Calculate and transport equalitiesL31–32

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

  1. L31
    rewrite hgone
  2. L32
    rewrite hgone
11Use earlier factsL33–35

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

  1. L33
    specialize crt_mod_one_universal u
  2. L34
    specialize crt_mod_one_universal v
  3. L35
    apply crt_mod_one_universal
12Fix variables and assumptionsL36–43

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

  1. L36
    intro n
  2. L37
    intro u
  3. L38
    intro v
  4. L39
    intro L
  5. L40
    intro g
  6. L41
    intro hL
  7. L42
    intro hp
  8. L43
    intro hg
13Use earlier factsL44–46

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

  1. L44
    specialize crt_prefix_lcm_exists_unique b
  2. L45
    specialize crt_prefix_lcm_exists_unique c
  3. L46
    specialize crt_prefix_lcm_exists_unique l
14Separate the logical casesL47–48

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

  1. L47
    cases crt_prefix_lcm_exists_unique
  2. L48
    cases crt_prefix_lcm_exists_unique_witness
15Establish hmL49–53

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

  1. L49
    have hm : exists m. ((exists ff_h_gcrt_gfull_prefix_actual_last. ff_h_gcrt_gfull_prefix_actual_last + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_gfull_prefix_actual_last. b = ff_q_gcrt_gfull_prefix_actual_last * S ((S (l)) * c) + (m))
  2. L50
    specialize beta_at_exists b
  3. L51
    specialize beta_at_exists c
  4. L52
    specialize beta_at_exists l
  5. L53
    apply beta_at_exists
16Separate the logical casesL54–54

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

  1. L54
    cases hm
17Establish hKL55–58

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

  1. L55
    have hK : ∃ K. Dvd(x,K) ∧ Dvd(x1,K) ∧ (∀ y. Dvd(x,y) → Dvd(x1,y) → Dvd(K,y))Definitions: Dvd
  2. L56
    specialize lcm_exists_relational x
  3. L57
    specialize lcm_exists_relational x1
  4. L58
    apply lcm_exists_relational
18Separate the logical casesL59–59

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

  1. L59
    cases hK
19Establish hLeqL60–69

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

  1. L60
    have hLeq : L = x2
  2. L61
    specialize crt_prefix_lcm_unique b
  3. L62
    specialize crt_prefix_lcm_unique c
  4. L63
    specialize crt_prefix_lcm_unique (S l)
  5. L64
    specialize crt_prefix_lcm_unique L
  6. L65
    specialize crt_prefix_lcm_unique x2
  7. L66
    apply crt_prefix_lcm_unique
  8. L67
    exact hL
  9. L68
    specialize crt_prefix_lcm_successor_intro b
  10. L69
    specialize crt_prefix_lcm_successor_intro c
20Use earlier factsL70–77

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

  1. L70
    specialize crt_prefix_lcm_successor_intro l
  2. L71
    specialize crt_prefix_lcm_successor_intro x
  3. L72
    specialize crt_prefix_lcm_successor_intro x1
  4. L73
    specialize crt_prefix_lcm_successor_intro x2
  5. L74
    apply crt_prefix_lcm_successor_intro
  6. L75
    exact crt_prefix_lcm_exists_unique_witness_left
  7. L76
    exact hm_witness
  8. L77
    exact hK_witness
21Establish hdL78–81

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

  1. L78
    have hd : ∃ d. IsGCD(d,x,n)Definitions: IsGCD
  2. L79
    specialize canonical_gcd_exists x
  3. L80
    specialize canonical_gcd_exists n
  4. L81
    apply canonical_gcd_exists
22Separate the logical casesL82–82

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

  1. L82
    cases hd
23Establish heL83–86

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

  1. L83
    have he : ∃ e. IsGCD(e,x1,n)Definitions: IsGCD
  2. L84
    specialize canonical_gcd_exists x1
  3. L85
    specialize canonical_gcd_exists n
  4. L86
    apply canonical_gcd_exists
24Separate the logical casesL87–87

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

  1. L87
    cases he
25Establish hmodL88–97

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

  1. L88
    have hmod : exists hgcrt_mod_left_gfull_prefix_old_mod hgcrt_mod_right_gfull_prefix_old_mod. u + x3 * hgcrt_mod_left_gfull_prefix_old_mod = v + x3 * hgcrt_mod_right_gfull_prefix_old_mod
  2. L89
    specialize IH n
  3. L90
    specialize IH u
  4. L91
    specialize IH v
  5. L92
    specialize IH x
  6. L93
    specialize IH x3
  7. L94
    apply IH
  8. L95
    exact crt_prefix_lcm_exists_unique_witness_left
  9. L96
    specialize crt_prefix_gcd_congruences_drop_last b
  10. L97
    specialize crt_prefix_gcd_congruences_drop_last c
26Use earlier factsL98–104

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

  1. L98
    specialize crt_prefix_gcd_congruences_drop_last l
  2. L99
    specialize crt_prefix_gcd_congruences_drop_last n
  3. L100
    specialize crt_prefix_gcd_congruences_drop_last u
  4. L101
    specialize crt_prefix_gcd_congruences_drop_last v
  5. L102
    apply crt_prefix_gcd_congruences_drop_last
  6. L103
    exact hp
  7. L104
    exact hd_witness
27Establish hlatL105–114

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt gcd lcm distributes.

  1. L105
    have hlat : Dvd(x3,g) ∧ Dvd(x4,g) ∧ (∀ x. Dvd(x3,x) → Dvd(x4,x) → Dvd(g,x))Definitions: Dvd
  2. L106
    specialize crt_gcd_lcm_distributes x
  3. L107
    specialize crt_gcd_lcm_distributes x1
  4. L108
    specialize crt_gcd_lcm_distributes n
  5. L109
    specialize crt_gcd_lcm_distributes x2
  6. L110
    specialize crt_gcd_lcm_distributes x3
  7. L111
    specialize crt_gcd_lcm_distributes x4
  8. L112
    specialize crt_gcd_lcm_distributes g
  9. L113
    apply crt_gcd_lcm_distributes
  10. L114
    exact hK_witness
28Use earlier factsL115–116

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

  1. L115
    exact hd_witness
  2. L116
    exact he_witness
29Calculate and transport equalitiesL117–118

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

  1. L117
    rewrite <- hLeq
  2. L118
    rewrite <- hLeq
30Use earlier factsL119–128

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

  1. L119
    exact hg
  2. L120
    specialize mod_eq_lcm_merge g
  3. L121
    specialize mod_eq_lcm_merge x3
  4. L122
    specialize mod_eq_lcm_merge x4
  5. L123
    specialize mod_eq_lcm_merge u
  6. L124
    specialize mod_eq_lcm_merge v
  7. L125
    apply mod_eq_lcm_merge
  8. L126
    exact hlat
  9. L127
    exact hmod
  10. L128
    specialize hp l
31Use earlier factsL129–135

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

  1. L129
    specialize hp x1
  2. L130
    specialize hp x4
  3. L131
    apply hp
  4. L132
    specialize le_refl (S l)
  5. L133
    apply le_refl
  6. L134
    exact hm_witness
  7. L135
    exact he_witness

Library-wide reading audit

Original exact command ledger · 135 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro n
  5. 0005intro u
  6. 0006intro v
  7. 0007intro L
  8. 0008intro g
  9. 0009intro hL
  10. 0010intro hp
  11. 0011intro hg
  12. 0012have hLone : L = 1
  13. 0013specialize crt_prefix_lcm_unique b
  14. 0014specialize crt_prefix_lcm_unique c
  15. 0015specialize crt_prefix_lcm_unique 0
  16. 0016specialize crt_prefix_lcm_unique L
  17. 0017specialize crt_prefix_lcm_unique 1
  18. 0018apply crt_prefix_lcm_unique
  19. 0019exact hL
  20. 0020specialize crt_prefix_lcm_empty b
  21. 0021specialize crt_prefix_lcm_empty c
  22. 0022apply crt_prefix_lcm_empty
  23. 0023have hgone : g = 1
  24. 0024specialize canonical_gcd_one_left_iff n
  25. 0025specialize canonical_gcd_one_left_iff g
  26. 0026cases canonical_gcd_one_left_iff
  27. 0027apply canonical_gcd_one_left_iff_left
  28. 0028rewrite <- hLone
  29. 0029rewrite <- hLone
  30. 0030exact hg
  31. 0031rewrite hgone
  32. 0032rewrite hgone
  33. 0033specialize crt_mod_one_universal u
  34. 0034specialize crt_mod_one_universal v
  35. 0035apply crt_mod_one_universal
  36. 0036intro n
  37. 0037intro u
  38. 0038intro v
  39. 0039intro L
  40. 0040intro g
  41. 0041intro hL
  42. 0042intro hp
  43. 0043intro hg
  44. 0044specialize crt_prefix_lcm_exists_unique b
  45. 0045specialize crt_prefix_lcm_exists_unique c
  46. 0046specialize crt_prefix_lcm_exists_unique l
  47. 0047cases crt_prefix_lcm_exists_unique
  48. 0048cases crt_prefix_lcm_exists_unique_witness
  49. 0049have hm : exists m. ((exists ff_h_gcrt_gfull_prefix_actual_last. ff_h_gcrt_gfull_prefix_actual_last + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_gfull_prefix_actual_last. b = ff_q_gcrt_gfull_prefix_actual_last * S ((S (l)) * c) + (m))
  50. 0050specialize beta_at_exists b
  51. 0051specialize beta_at_exists c
  52. 0052specialize beta_at_exists l
  53. 0053apply beta_at_exists
  54. 0054cases hm
  55. 0055have hK : exists K. (((exists hscale_left_factor_gfull_prefix_binary_lcm. K = x * hscale_left_factor_gfull_prefix_binary_lcm) /\ (exists hscale_right_factor_gfull_prefix_binary_lcm. K = x1 * hscale_right_factor_gfull_prefix_binary_lcm)) /\ forall hscale_common_gfull_prefix_binary_lcm. (exists hscale_left_common_gfull_prefix_binary_lcm. hscale_common_gfull_prefix_binary_lcm = x * hscale_left_common_gfull_prefix_binary_lcm) -> (exists hscale_right_common_gfull_prefix_binary_lcm. hscale_common_gfull_prefix_binary_lcm = x1 * hscale_right_common_gfull_prefix_binary_lcm) -> exists hscale_least_factor_gfull_prefix_binary_lcm. hscale_common_gfull_prefix_binary_lcm = K * hscale_least_factor_gfull_prefix_binary_lcm)
  56. 0056specialize lcm_exists_relational x
  57. 0057specialize lcm_exists_relational x1
  58. 0058apply lcm_exists_relational
  59. 0059cases hK
  60. 0060have hLeq : L = x2
  61. 0061specialize crt_prefix_lcm_unique b
  62. 0062specialize crt_prefix_lcm_unique c
  63. 0063specialize crt_prefix_lcm_unique (S l)
  64. 0064specialize crt_prefix_lcm_unique L
  65. 0065specialize crt_prefix_lcm_unique x2
  66. 0066apply crt_prefix_lcm_unique
  67. 0067exact hL
  68. 0068specialize crt_prefix_lcm_successor_intro b
  69. 0069specialize crt_prefix_lcm_successor_intro c
  70. 0070specialize crt_prefix_lcm_successor_intro l
  71. 0071specialize crt_prefix_lcm_successor_intro x
  72. 0072specialize crt_prefix_lcm_successor_intro x1
  73. 0073specialize crt_prefix_lcm_successor_intro x2
  74. 0074apply crt_prefix_lcm_successor_intro
  75. 0075exact crt_prefix_lcm_exists_unique_witness_left
  76. 0076exact hm_witness
  77. 0077exact hK_witness
  78. 0078have hd : exists d. (((exists ec_gcd_left_gfull_prefix_old_gcd. x = d * ec_gcd_left_gfull_prefix_old_gcd) /\ (exists ec_gcd_right_gfull_prefix_old_gcd. n = d * ec_gcd_right_gfull_prefix_old_gcd)) /\ forall ec_gcd_common_gfull_prefix_old_gcd. (exists ec_gcd_common_left_gfull_prefix_old_gcd. x = ec_gcd_common_gfull_prefix_old_gcd * ec_gcd_common_left_gfull_prefix_old_gcd) -> (exists ec_gcd_common_right_gfull_prefix_old_gcd. n = ec_gcd_common_gfull_prefix_old_gcd * ec_gcd_common_right_gfull_prefix_old_gcd) -> exists ec_gcd_greatest_gfull_prefix_old_gcd. d = ec_gcd_common_gfull_prefix_old_gcd * ec_gcd_greatest_gfull_prefix_old_gcd)
  79. 0079specialize canonical_gcd_exists x
  80. 0080specialize canonical_gcd_exists n
  81. 0081apply canonical_gcd_exists
  82. 0082cases hd
  83. 0083have he : exists e. (((exists ec_gcd_left_gfull_prefix_new_gcd. x1 = e * ec_gcd_left_gfull_prefix_new_gcd) /\ (exists ec_gcd_right_gfull_prefix_new_gcd. n = e * ec_gcd_right_gfull_prefix_new_gcd)) /\ forall ec_gcd_common_gfull_prefix_new_gcd. (exists ec_gcd_common_left_gfull_prefix_new_gcd. x1 = ec_gcd_common_gfull_prefix_new_gcd * ec_gcd_common_left_gfull_prefix_new_gcd) -> (exists ec_gcd_common_right_gfull_prefix_new_gcd. n = ec_gcd_common_gfull_prefix_new_gcd * ec_gcd_common_right_gfull_prefix_new_gcd) -> exists ec_gcd_greatest_gfull_prefix_new_gcd. e = ec_gcd_common_gfull_prefix_new_gcd * ec_gcd_greatest_gfull_prefix_new_gcd)
  84. 0084specialize canonical_gcd_exists x1
  85. 0085specialize canonical_gcd_exists n
  86. 0086apply canonical_gcd_exists
  87. 0087cases he
  88. 0088have hmod : exists hgcrt_mod_left_gfull_prefix_old_mod hgcrt_mod_right_gfull_prefix_old_mod. u + x3 * hgcrt_mod_left_gfull_prefix_old_mod = v + x3 * hgcrt_mod_right_gfull_prefix_old_mod
  89. 0089specialize IH n
  90. 0090specialize IH u
  91. 0091specialize IH v
  92. 0092specialize IH x
  93. 0093specialize IH x3
  94. 0094apply IH
  95. 0095exact crt_prefix_lcm_exists_unique_witness_left
  96. 0096specialize crt_prefix_gcd_congruences_drop_last b
  97. 0097specialize crt_prefix_gcd_congruences_drop_last c
  98. 0098specialize crt_prefix_gcd_congruences_drop_last l
  99. 0099specialize crt_prefix_gcd_congruences_drop_last n
  100. 0100specialize crt_prefix_gcd_congruences_drop_last u
  101. 0101specialize crt_prefix_gcd_congruences_drop_last v
  102. 0102apply crt_prefix_gcd_congruences_drop_last
  103. 0103exact hp
  104. 0104exact hd_witness
  105. 0105have hlat : (((exists hscale_left_factor_gfull_prefix_lattice_result. g = x3 * hscale_left_factor_gfull_prefix_lattice_result) /\ (exists hscale_right_factor_gfull_prefix_lattice_result. g = x4 * hscale_right_factor_gfull_prefix_lattice_result)) /\ forall hscale_common_gfull_prefix_lattice_result. (exists hscale_left_common_gfull_prefix_lattice_result. hscale_common_gfull_prefix_lattice_result = x3 * hscale_left_common_gfull_prefix_lattice_result) -> (exists hscale_right_common_gfull_prefix_lattice_result. hscale_common_gfull_prefix_lattice_result = x4 * hscale_right_common_gfull_prefix_lattice_result) -> exists hscale_least_factor_gfull_prefix_lattice_result. hscale_common_gfull_prefix_lattice_result = g * hscale_least_factor_gfull_prefix_lattice_result)
  106. 0106specialize crt_gcd_lcm_distributes x
  107. 0107specialize crt_gcd_lcm_distributes x1
  108. 0108specialize crt_gcd_lcm_distributes n
  109. 0109specialize crt_gcd_lcm_distributes x2
  110. 0110specialize crt_gcd_lcm_distributes x3
  111. 0111specialize crt_gcd_lcm_distributes x4
  112. 0112specialize crt_gcd_lcm_distributes g
  113. 0113apply crt_gcd_lcm_distributes
  114. 0114exact hK_witness
  115. 0115exact hd_witness
  116. 0116exact he_witness
  117. 0117rewrite <- hLeq
  118. 0118rewrite <- hLeq
  119. 0119exact hg
  120. 0120specialize mod_eq_lcm_merge g
  121. 0121specialize mod_eq_lcm_merge x3
  122. 0122specialize mod_eq_lcm_merge x4
  123. 0123specialize mod_eq_lcm_merge u
  124. 0124specialize mod_eq_lcm_merge v
  125. 0125apply mod_eq_lcm_merge
  126. 0126exact hlat
  127. 0127exact hmod
  128. 0128specialize hp l
  129. 0129specialize hp x1
  130. 0130specialize hp x4
  131. 0131apply hp
  132. 0132specialize le_refl (S l)
  133. 0133apply le_refl
  134. 0134exact hm_witness
  135. 0135exact he_witness