CR001B

crt_pairwise_coprime_prefix_canonical_exists_unique

Every arbitrary finite list of positive pairwise-coprime moduli has its exact lcm and a unique actual bounded CRT solution.

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

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.

Historical partial components only: this chapter proves canonical solutions for finite positive pairwise-coprime systems and exact LCM solution classes. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible systems, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. CRTPositiveModuliPrefix(b,c,l) → CRTPairwiseCoprimePrefix(b,c,l) → ∃ x. ∃ y. CRTCanonicalPrefixSolution(r,s,b,c,l,x,y) ∧ (∀ z. CRTCanonicalPrefixSolution(r,s,b,c,l,z,y) → z = x)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

CRTPositiveModuliPrefix(b,c,l) · 1CRTPairwiseCoprimePrefix(b,c,l) · 1CRTCanonicalPrefixSolution(r,s,b,c,l,x,M) · 2

Actual proof prerequisites

beta_product_exists_unique · checked external prerequisitecrt_positive_moduli_prefix_product_nonzerocrt_pairwise_coprime_prefix_product_is_lcmcrt_pairwise_coprime_prefix_solution_existscrt_prefix_solution_canonical_remaindercrt_canonical_prefix_solution_unique
Original expanded first-order statement 
forall r s b c l. (forall gcrt_positive_index_final_positive gcrt_positive_value_final_positive. (exists ff_lt_gcrt_final_positive_bound. ff_lt_gcrt_final_positive_bound + S gcrt_positive_index_final_positive = l) -> (((exists ff_h_gcrt_final_positive_entry. ff_h_gcrt_final_positive_entry + S (gcrt_positive_value_final_positive) = S ((S (gcrt_positive_index_final_positive)) * c)) /\ exists ff_q_gcrt_final_positive_entry. b = ff_q_gcrt_final_positive_entry * S ((S (gcrt_positive_index_final_positive)) * c) + (gcrt_positive_value_final_positive))) -> ~(gcrt_positive_value_final_positive = 0)) -> (forall bpr_left_index_gcrt_final_pairwise bpr_right_index_gcrt_final_pairwise bpr_left_value_gcrt_final_pairwise bpr_right_value_gcrt_final_pairwise. (exists bpr_gap_gcrt_final_pairwise_left_bound. bpr_gap_gcrt_final_pairwise_left_bound + S (bpr_left_index_gcrt_final_pairwise) = l) -> (exists bpr_gap_gcrt_final_pairwise_right_bound. bpr_gap_gcrt_final_pairwise_right_bound + S (bpr_right_index_gcrt_final_pairwise) = l) -> (((exists bpr_height_gcrt_final_pairwise_left_at. bpr_height_gcrt_final_pairwise_left_at + S (bpr_left_value_gcrt_final_pairwise) = S ((S (bpr_left_index_gcrt_final_pairwise)) * c)) /\ exists bpr_quotient_gcrt_final_pairwise_left_at. b = bpr_quotient_gcrt_final_pairwise_left_at * S ((S (bpr_left_index_gcrt_final_pairwise)) * c) + (bpr_left_value_gcrt_final_pairwise))) -> (((exists bpr_height_gcrt_final_pairwise_right_at. bpr_height_gcrt_final_pairwise_right_at + S (bpr_right_value_gcrt_final_pairwise) = S ((S (bpr_right_index_gcrt_final_pairwise)) * c)) /\ exists bpr_quotient_gcrt_final_pairwise_right_at. b = bpr_quotient_gcrt_final_pairwise_right_at * S ((S (bpr_right_index_gcrt_final_pairwise)) * c) + (bpr_right_value_gcrt_final_pairwise))) -> ~(bpr_left_index_gcrt_final_pairwise = bpr_right_index_gcrt_final_pairwise) -> (forall bpr_coprime_divisor_gcrt_final_pairwise_coprime. (exists bpr_coprime_left_factor_gcrt_final_pairwise_coprime. bpr_left_value_gcrt_final_pairwise = bpr_coprime_divisor_gcrt_final_pairwise_coprime * bpr_coprime_left_factor_gcrt_final_pairwise_coprime) -> (exists bpr_coprime_right_factor_gcrt_final_pairwise_coprime. bpr_right_value_gcrt_final_pairwise = bpr_coprime_divisor_gcrt_final_pairwise_coprime * bpr_coprime_right_factor_gcrt_final_pairwise_coprime) -> bpr_coprime_divisor_gcrt_final_pairwise_coprime = 1)) -> exists x M. ((((((forall gcrt_common_index_final_chosen_lcm_own gcrt_common_modulus_final_chosen_lcm_own. (exists ff_lt_gcrt_final_chosen_lcm_own_bound. ff_lt_gcrt_final_chosen_lcm_own_bound + S gcrt_common_index_final_chosen_lcm_own = l) -> (((exists ff_h_gcrt_final_chosen_lcm_own_entry. ff_h_gcrt_final_chosen_lcm_own_entry + S (gcrt_common_modulus_final_chosen_lcm_own) = S ((S (gcrt_common_index_final_chosen_lcm_own)) * c)) /\ exists ff_q_gcrt_final_chosen_lcm_own_entry. b = ff_q_gcrt_final_chosen_lcm_own_entry * S ((S (gcrt_common_index_final_chosen_lcm_own)) * c) + (gcrt_common_modulus_final_chosen_lcm_own))) -> exists gcrt_common_quotient_final_chosen_lcm_own. M = gcrt_common_modulus_final_chosen_lcm_own * gcrt_common_quotient_final_chosen_lcm_own) /\ forall gcrt_lcm_common_final_chosen_lcm. (forall gcrt_common_index_final_chosen_lcm_other gcrt_common_modulus_final_chosen_lcm_other. (exists ff_lt_gcrt_final_chosen_lcm_other_bound. ff_lt_gcrt_final_chosen_lcm_other_bound + S gcrt_common_index_final_chosen_lcm_other = l) -> (((exists ff_h_gcrt_final_chosen_lcm_other_entry. ff_h_gcrt_final_chosen_lcm_other_entry + S (gcrt_common_modulus_final_chosen_lcm_other) = S ((S (gcrt_common_index_final_chosen_lcm_other)) * c)) /\ exists ff_q_gcrt_final_chosen_lcm_other_entry. b = ff_q_gcrt_final_chosen_lcm_other_entry * S ((S (gcrt_common_index_final_chosen_lcm_other)) * c) + (gcrt_common_modulus_final_chosen_lcm_other))) -> exists gcrt_common_quotient_final_chosen_lcm_other. gcrt_lcm_common_final_chosen_lcm = gcrt_common_modulus_final_chosen_lcm_other * gcrt_common_quotient_final_chosen_lcm_other) -> exists gcrt_lcm_quotient_final_chosen_lcm. gcrt_lcm_common_final_chosen_lcm = M * gcrt_lcm_quotient_final_chosen_lcm)) /\ ((exists ff_lt_gcrt_final_chosen_bounded. ff_lt_gcrt_final_chosen_bounded + S x = M) /\ (forall gcrt_solution_index_final_chosen_solution gcrt_solution_residue_final_chosen_solution gcrt_solution_modulus_final_chosen_solution. (exists ff_lt_gcrt_final_chosen_solution_bound. ff_lt_gcrt_final_chosen_solution_bound + S gcrt_solution_index_final_chosen_solution = l) -> (((exists ff_h_gcrt_final_chosen_solution_residue. ff_h_gcrt_final_chosen_solution_residue + S (gcrt_solution_residue_final_chosen_solution) = S ((S (gcrt_solution_index_final_chosen_solution)) * s)) /\ exists ff_q_gcrt_final_chosen_solution_residue. r = ff_q_gcrt_final_chosen_solution_residue * S ((S (gcrt_solution_index_final_chosen_solution)) * s) + (gcrt_solution_residue_final_chosen_solution))) -> (((exists ff_h_gcrt_final_chosen_solution_modulus. ff_h_gcrt_final_chosen_solution_modulus + S (gcrt_solution_modulus_final_chosen_solution) = S ((S (gcrt_solution_index_final_chosen_solution)) * c)) /\ exists ff_q_gcrt_final_chosen_solution_modulus. b = ff_q_gcrt_final_chosen_solution_modulus * S ((S (gcrt_solution_index_final_chosen_solution)) * c) + (gcrt_solution_modulus_final_chosen_solution))) -> (exists hgcrt_mod_left_gcrt_final_chosen_solution_congruence hgcrt_mod_right_gcrt_final_chosen_solution_congruence. x + gcrt_solution_modulus_final_chosen_solution * hgcrt_mod_left_gcrt_final_chosen_solution_congruence = gcrt_solution_residue_final_chosen_solution + gcrt_solution_modulus_final_chosen_solution * hgcrt_mod_right_gcrt_final_chosen_solution_congruence))))) /\ forall y. (((((forall gcrt_common_index_final_compared_lcm_own gcrt_common_modulus_final_compared_lcm_own. (exists ff_lt_gcrt_final_compared_lcm_own_bound. ff_lt_gcrt_final_compared_lcm_own_bound + S gcrt_common_index_final_compared_lcm_own = l) -> (((exists ff_h_gcrt_final_compared_lcm_own_entry. ff_h_gcrt_final_compared_lcm_own_entry + S (gcrt_common_modulus_final_compared_lcm_own) = S ((S (gcrt_common_index_final_compared_lcm_own)) * c)) /\ exists ff_q_gcrt_final_compared_lcm_own_entry. b = ff_q_gcrt_final_compared_lcm_own_entry * S ((S (gcrt_common_index_final_compared_lcm_own)) * c) + (gcrt_common_modulus_final_compared_lcm_own))) -> exists gcrt_common_quotient_final_compared_lcm_own. M = gcrt_common_modulus_final_compared_lcm_own * gcrt_common_quotient_final_compared_lcm_own) /\ forall gcrt_lcm_common_final_compared_lcm. (forall gcrt_common_index_final_compared_lcm_other gcrt_common_modulus_final_compared_lcm_other. (exists ff_lt_gcrt_final_compared_lcm_other_bound. ff_lt_gcrt_final_compared_lcm_other_bound + S gcrt_common_index_final_compared_lcm_other = l) -> (((exists ff_h_gcrt_final_compared_lcm_other_entry. ff_h_gcrt_final_compared_lcm_other_entry + S (gcrt_common_modulus_final_compared_lcm_other) = S ((S (gcrt_common_index_final_compared_lcm_other)) * c)) /\ exists ff_q_gcrt_final_compared_lcm_other_entry. b = ff_q_gcrt_final_compared_lcm_other_entry * S ((S (gcrt_common_index_final_compared_lcm_other)) * c) + (gcrt_common_modulus_final_compared_lcm_other))) -> exists gcrt_common_quotient_final_compared_lcm_other. gcrt_lcm_common_final_compared_lcm = gcrt_common_modulus_final_compared_lcm_other * gcrt_common_quotient_final_compared_lcm_other) -> exists gcrt_lcm_quotient_final_compared_lcm. gcrt_lcm_common_final_compared_lcm = M * gcrt_lcm_quotient_final_compared_lcm)) /\ ((exists ff_lt_gcrt_final_compared_bounded. ff_lt_gcrt_final_compared_bounded + S y = M) /\ (forall gcrt_solution_index_final_compared_solution gcrt_solution_residue_final_compared_solution gcrt_solution_modulus_final_compared_solution. (exists ff_lt_gcrt_final_compared_solution_bound. ff_lt_gcrt_final_compared_solution_bound + S gcrt_solution_index_final_compared_solution = l) -> (((exists ff_h_gcrt_final_compared_solution_residue. ff_h_gcrt_final_compared_solution_residue + S (gcrt_solution_residue_final_compared_solution) = S ((S (gcrt_solution_index_final_compared_solution)) * s)) /\ exists ff_q_gcrt_final_compared_solution_residue. r = ff_q_gcrt_final_compared_solution_residue * S ((S (gcrt_solution_index_final_compared_solution)) * s) + (gcrt_solution_residue_final_compared_solution))) -> (((exists ff_h_gcrt_final_compared_solution_modulus. ff_h_gcrt_final_compared_solution_modulus + S (gcrt_solution_modulus_final_compared_solution) = S ((S (gcrt_solution_index_final_compared_solution)) * c)) /\ exists ff_q_gcrt_final_compared_solution_modulus. b = ff_q_gcrt_final_compared_solution_modulus * S ((S (gcrt_solution_index_final_compared_solution)) * c) + (gcrt_solution_modulus_final_compared_solution))) -> (exists hgcrt_mod_left_gcrt_final_compared_solution_congruence hgcrt_mod_right_gcrt_final_compared_solution_congruence. y + gcrt_solution_modulus_final_compared_solution * hgcrt_mod_left_gcrt_final_compared_solution_congruence = gcrt_solution_residue_final_compared_solution + gcrt_solution_modulus_final_compared_solution * hgcrt_mod_right_gcrt_final_compared_solution_congruence))))) -> y = x)

Complete unchanged native tactic proof

All 70 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

70 script commands · 16 reading checkpoints · 4 local claims

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (5)
crt positive moduli prefix product nonzerocrt pairwise coprime prefix product is lcmcrt pairwise coprime prefix solution existscrt prefix solution canonical remaindercrt canonical prefix solution unique

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–7

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro l
  6. L6
    intro hpositive
  7. L7
    intro hpairs
02Use earlier factsL8–10

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

  1. L8
    specialize beta_product_exists_unique b
  2. L9
    specialize beta_product_exists_unique c
  3. L10
    specialize beta_product_exists_unique l
03Separate the logical casesL11–12

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

  1. L11
    cases beta_product_exists_unique
  2. L12
    cases beta_product_exists_unique_witness
04Establish hnonzeroL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt positive moduli prefix product nonzero.

  1. L13
    have hnonzero : ~(x = 0)
  2. L14
    specialize crt_positive_moduli_prefix_product_nonzero b
  3. L15
    specialize crt_positive_moduli_prefix_product_nonzero c
  4. L16
    specialize crt_positive_moduli_prefix_product_nonzero l
  5. L17
    specialize crt_positive_moduli_prefix_product_nonzero x
  6. L18
    intro hzero
  7. L19
    apply crt_positive_moduli_prefix_product_nonzero
  8. L20
    exact hpositive
  9. L21
    exact beta_product_exists_unique_witness_left
  10. L22
    exact hzero
05Establish hlcmL23–30

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

  1. L23
    have hlcm : CRTPrefixLCM(b,c,l,x)Definitions: CRTPrefixLCMOriginal native command in the exact edition
  2. L24
    specialize crt_pairwise_coprime_prefix_product_is_lcm b
  3. L25
    specialize crt_pairwise_coprime_prefix_product_is_lcm c
  4. L26
    specialize crt_pairwise_coprime_prefix_product_is_lcm l
  5. L27
    specialize crt_pairwise_coprime_prefix_product_is_lcm x
  6. L28
    apply crt_pairwise_coprime_prefix_product_is_lcm
  7. L29
    exact hpairs
  8. L30
    exact beta_product_exists_unique_witness_left
06Establish hsolutionL31–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt pairwise coprime prefix solution exists.

  1. L31
    have hsolution : ∃ y. CRTPrefixSolution(r,s,b,c,l,y)Definitions: CRTPrefixSolutionOriginal native command in the exact edition
  2. L32
    specialize crt_pairwise_coprime_prefix_solution_exists r
  3. L33
    specialize crt_pairwise_coprime_prefix_solution_exists s
  4. L34
    specialize crt_pairwise_coprime_prefix_solution_exists b
  5. L35
    specialize crt_pairwise_coprime_prefix_solution_exists c
  6. L36
    specialize crt_pairwise_coprime_prefix_solution_exists l
  7. L37
    apply crt_pairwise_coprime_prefix_solution_exists
  8. L38
    exact hpositive
  9. L39
    exact hpairs
07Separate the logical casesL40–40

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

  1. L40
    cases hsolution
08Establish hcanonicalL41–50

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

  1. L41
    have hcanonical : ∃ z. CRTCanonicalPrefixSolution(r,s,b,c,l,z,x)Definitions: CRTCanonicalPrefixSolutionOriginal native command in the exact edition
  2. L42
    specialize crt_prefix_solution_canonical_remainder r
  3. L43
    specialize crt_prefix_solution_canonical_remainder s
  4. L44
    specialize crt_prefix_solution_canonical_remainder b
  5. L45
    specialize crt_prefix_solution_canonical_remainder c
  6. L46
    specialize crt_prefix_solution_canonical_remainder l
  7. L47
    specialize crt_prefix_solution_canonical_remainder x
  8. L48
    specialize crt_prefix_solution_canonical_remainder x1
  9. L49
    apply crt_prefix_solution_canonical_remainder
  10. L50
    exact hnonzero
09Use earlier factsL51–52

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

  1. L51
    exact hlcm
  2. L52
    exact hsolution_witness
10Separate the logical casesL53–53

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

  1. L53
    cases hcanonical
11Construct an explicit witnessL54–55

Supply the displayed value, then prove that it has the required property.

  1. L54
    exists x2
  2. L55
    exists x
12Separate the logical casesL56–56

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

  1. L56
    split
13Use earlier factsL57–57

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

  1. L57
    exact hcanonical_witness
14Fix variables and assumptionsL58–59

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

  1. L58
    intro y
  2. L59
    intro hy
15Use earlier factsL60–69

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

  1. L60
    specialize crt_canonical_prefix_solution_unique r
  2. L61
    specialize crt_canonical_prefix_solution_unique s
  3. L62
    specialize crt_canonical_prefix_solution_unique b
  4. L63
    specialize crt_canonical_prefix_solution_unique c
  5. L64
    specialize crt_canonical_prefix_solution_unique l
  6. L65
    specialize crt_canonical_prefix_solution_unique x
  7. L66
    specialize crt_canonical_prefix_solution_unique x2
  8. L67
    specialize crt_canonical_prefix_solution_unique y
  9. L68
    apply crt_canonical_prefix_solution_unique
  10. L69
    exact hcanonical_witness
16Use earlier factsL70–70

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

  1. L70
    exact hy

Library-wide reading audit

Original defined command ledger · 70 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro hpositive
  7. 0007intro hpairs
  8. 0008specialize beta_product_exists_unique b
  9. 0009specialize beta_product_exists_unique c
  10. 0010specialize beta_product_exists_unique l
  11. 0011cases beta_product_exists_unique
  12. 0012cases beta_product_exists_unique_witness
  13. 0013have hnonzero : ~(x = 0)
  14. 0014specialize crt_positive_moduli_prefix_product_nonzero b
  15. 0015specialize crt_positive_moduli_prefix_product_nonzero c
  16. 0016specialize crt_positive_moduli_prefix_product_nonzero l
  17. 0017specialize crt_positive_moduli_prefix_product_nonzero x
  18. 0018intro hzero
  19. 0019apply crt_positive_moduli_prefix_product_nonzero
  20. 0020exact hpositive
  21. 0021exact beta_product_exists_unique_witness_left
  22. 0022exact hzero
  23. 0023have hlcm : ((forall gcrt_common_index_final_actual_lcm_own gcrt_common_modulus_final_actual_lcm_own. (exists ff_lt_gcrt_final_actual_lcm_own_bound. ff_lt_gcrt_final_actual_lcm_own_bound + S gcrt_common_index_final_actual_lcm_own = l) -> (((exists ff_h_gcrt_final_actual_lcm_own_entry. ff_h_gcrt_final_actual_lcm_own_entry + S (gcrt_common_modulus_final_actual_lcm_own) = S ((S (gcrt_common_index_final_actual_lcm_own)) * c)) /\ exists ff_q_gcrt_final_actual_lcm_own_entry. b = ff_q_gcrt_final_actual_lcm_own_entry * S ((S (gcrt_common_index_final_actual_lcm_own)) * c) + (gcrt_common_modulus_final_actual_lcm_own))) -> exists gcrt_common_quotient_final_actual_lcm_own. x = gcrt_common_modulus_final_actual_lcm_own * gcrt_common_quotient_final_actual_lcm_own) /\ forall gcrt_lcm_common_final_actual_lcm. (forall gcrt_common_index_final_actual_lcm_other gcrt_common_modulus_final_actual_lcm_other. (exists ff_lt_gcrt_final_actual_lcm_other_bound. ff_lt_gcrt_final_actual_lcm_other_bound + S gcrt_common_index_final_actual_lcm_other = l) -> (((exists ff_h_gcrt_final_actual_lcm_other_entry. ff_h_gcrt_final_actual_lcm_other_entry + S (gcrt_common_modulus_final_actual_lcm_other) = S ((S (gcrt_common_index_final_actual_lcm_other)) * c)) /\ exists ff_q_gcrt_final_actual_lcm_other_entry. b = ff_q_gcrt_final_actual_lcm_other_entry * S ((S (gcrt_common_index_final_actual_lcm_other)) * c) + (gcrt_common_modulus_final_actual_lcm_other))) -> exists gcrt_common_quotient_final_actual_lcm_other. gcrt_lcm_common_final_actual_lcm = gcrt_common_modulus_final_actual_lcm_other * gcrt_common_quotient_final_actual_lcm_other) -> exists gcrt_lcm_quotient_final_actual_lcm. gcrt_lcm_common_final_actual_lcm = x * gcrt_lcm_quotient_final_actual_lcm)
  24. 0024specialize crt_pairwise_coprime_prefix_product_is_lcm b
  25. 0025specialize crt_pairwise_coprime_prefix_product_is_lcm c
  26. 0026specialize crt_pairwise_coprime_prefix_product_is_lcm l
  27. 0027specialize crt_pairwise_coprime_prefix_product_is_lcm x
  28. 0028apply crt_pairwise_coprime_prefix_product_is_lcm
  29. 0029exact hpairs
  30. 0030exact beta_product_exists_unique_witness_left
  31. 0031have hsolution : exists y. (forall gcrt_solution_index_final_unbounded gcrt_solution_residue_final_unbounded gcrt_solution_modulus_final_unbounded. (exists ff_lt_gcrt_final_unbounded_bound. ff_lt_gcrt_final_unbounded_bound + S gcrt_solution_index_final_unbounded = l) -> (((exists ff_h_gcrt_final_unbounded_residue. ff_h_gcrt_final_unbounded_residue + S (gcrt_solution_residue_final_unbounded) = S ((S (gcrt_solution_index_final_unbounded)) * s)) /\ exists ff_q_gcrt_final_unbounded_residue. r = ff_q_gcrt_final_unbounded_residue * S ((S (gcrt_solution_index_final_unbounded)) * s) + (gcrt_solution_residue_final_unbounded))) -> (((exists ff_h_gcrt_final_unbounded_modulus. ff_h_gcrt_final_unbounded_modulus + S (gcrt_solution_modulus_final_unbounded) = S ((S (gcrt_solution_index_final_unbounded)) * c)) /\ exists ff_q_gcrt_final_unbounded_modulus. b = ff_q_gcrt_final_unbounded_modulus * S ((S (gcrt_solution_index_final_unbounded)) * c) + (gcrt_solution_modulus_final_unbounded))) -> (exists hgcrt_mod_left_gcrt_final_unbounded_congruence hgcrt_mod_right_gcrt_final_unbounded_congruence. y + gcrt_solution_modulus_final_unbounded * hgcrt_mod_left_gcrt_final_unbounded_congruence = gcrt_solution_residue_final_unbounded + gcrt_solution_modulus_final_unbounded * hgcrt_mod_right_gcrt_final_unbounded_congruence))
  32. 0032specialize crt_pairwise_coprime_prefix_solution_exists r
  33. 0033specialize crt_pairwise_coprime_prefix_solution_exists s
  34. 0034specialize crt_pairwise_coprime_prefix_solution_exists b
  35. 0035specialize crt_pairwise_coprime_prefix_solution_exists c
  36. 0036specialize crt_pairwise_coprime_prefix_solution_exists l
  37. 0037apply crt_pairwise_coprime_prefix_solution_exists
  38. 0038exact hpositive
  39. 0039exact hpairs
  40. 0040cases hsolution
  41. 0041have hcanonical : exists z. (((((forall gcrt_common_index_final_canonical_lcm_own gcrt_common_modulus_final_canonical_lcm_own. (exists ff_lt_gcrt_final_canonical_lcm_own_bound. ff_lt_gcrt_final_canonical_lcm_own_bound + S gcrt_common_index_final_canonical_lcm_own = l) -> (((exists ff_h_gcrt_final_canonical_lcm_own_entry. ff_h_gcrt_final_canonical_lcm_own_entry + S (gcrt_common_modulus_final_canonical_lcm_own) = S ((S (gcrt_common_index_final_canonical_lcm_own)) * c)) /\ exists ff_q_gcrt_final_canonical_lcm_own_entry. b = ff_q_gcrt_final_canonical_lcm_own_entry * S ((S (gcrt_common_index_final_canonical_lcm_own)) * c) + (gcrt_common_modulus_final_canonical_lcm_own))) -> exists gcrt_common_quotient_final_canonical_lcm_own. x = gcrt_common_modulus_final_canonical_lcm_own * gcrt_common_quotient_final_canonical_lcm_own) /\ forall gcrt_lcm_common_final_canonical_lcm. (forall gcrt_common_index_final_canonical_lcm_other gcrt_common_modulus_final_canonical_lcm_other. (exists ff_lt_gcrt_final_canonical_lcm_other_bound. ff_lt_gcrt_final_canonical_lcm_other_bound + S gcrt_common_index_final_canonical_lcm_other = l) -> (((exists ff_h_gcrt_final_canonical_lcm_other_entry. ff_h_gcrt_final_canonical_lcm_other_entry + S (gcrt_common_modulus_final_canonical_lcm_other) = S ((S (gcrt_common_index_final_canonical_lcm_other)) * c)) /\ exists ff_q_gcrt_final_canonical_lcm_other_entry. b = ff_q_gcrt_final_canonical_lcm_other_entry * S ((S (gcrt_common_index_final_canonical_lcm_other)) * c) + (gcrt_common_modulus_final_canonical_lcm_other))) -> exists gcrt_common_quotient_final_canonical_lcm_other. gcrt_lcm_common_final_canonical_lcm = gcrt_common_modulus_final_canonical_lcm_other * gcrt_common_quotient_final_canonical_lcm_other) -> exists gcrt_lcm_quotient_final_canonical_lcm. gcrt_lcm_common_final_canonical_lcm = x * gcrt_lcm_quotient_final_canonical_lcm)) /\ ((exists ff_lt_gcrt_final_canonical_bounded. ff_lt_gcrt_final_canonical_bounded + S z = x) /\ (forall gcrt_solution_index_final_canonical_solution gcrt_solution_residue_final_canonical_solution gcrt_solution_modulus_final_canonical_solution. (exists ff_lt_gcrt_final_canonical_solution_bound. ff_lt_gcrt_final_canonical_solution_bound + S gcrt_solution_index_final_canonical_solution = l) -> (((exists ff_h_gcrt_final_canonical_solution_residue. ff_h_gcrt_final_canonical_solution_residue + S (gcrt_solution_residue_final_canonical_solution) = S ((S (gcrt_solution_index_final_canonical_solution)) * s)) /\ exists ff_q_gcrt_final_canonical_solution_residue. r = ff_q_gcrt_final_canonical_solution_residue * S ((S (gcrt_solution_index_final_canonical_solution)) * s) + (gcrt_solution_residue_final_canonical_solution))) -> (((exists ff_h_gcrt_final_canonical_solution_modulus. ff_h_gcrt_final_canonical_solution_modulus + S (gcrt_solution_modulus_final_canonical_solution) = S ((S (gcrt_solution_index_final_canonical_solution)) * c)) /\ exists ff_q_gcrt_final_canonical_solution_modulus. b = ff_q_gcrt_final_canonical_solution_modulus * S ((S (gcrt_solution_index_final_canonical_solution)) * c) + (gcrt_solution_modulus_final_canonical_solution))) -> (exists hgcrt_mod_left_gcrt_final_canonical_solution_congruence hgcrt_mod_right_gcrt_final_canonical_solution_congruence. z + gcrt_solution_modulus_final_canonical_solution * hgcrt_mod_left_gcrt_final_canonical_solution_congruence = gcrt_solution_residue_final_canonical_solution + gcrt_solution_modulus_final_canonical_solution * hgcrt_mod_right_gcrt_final_canonical_solution_congruence)))))
  42. 0042specialize crt_prefix_solution_canonical_remainder r
  43. 0043specialize crt_prefix_solution_canonical_remainder s
  44. 0044specialize crt_prefix_solution_canonical_remainder b
  45. 0045specialize crt_prefix_solution_canonical_remainder c
  46. 0046specialize crt_prefix_solution_canonical_remainder l
  47. 0047specialize crt_prefix_solution_canonical_remainder x
  48. 0048specialize crt_prefix_solution_canonical_remainder x1
  49. 0049apply crt_prefix_solution_canonical_remainder
  50. 0050exact hnonzero
  51. 0051exact hlcm
  52. 0052exact hsolution_witness
  53. 0053cases hcanonical
  54. 0054exists x2
  55. 0055exists x
  56. 0056split
  57. 0057exact hcanonical_witness
  58. 0058intro y
  59. 0059intro hy
  60. 0060specialize crt_canonical_prefix_solution_unique r
  61. 0061specialize crt_canonical_prefix_solution_unique s
  62. 0062specialize crt_canonical_prefix_solution_unique b
  63. 0063specialize crt_canonical_prefix_solution_unique c
  64. 0064specialize crt_canonical_prefix_solution_unique l
  65. 0065specialize crt_canonical_prefix_solution_unique x
  66. 0066specialize crt_canonical_prefix_solution_unique x2
  67. 0067specialize crt_canonical_prefix_solution_unique y
  68. 0068apply crt_canonical_prefix_solution_unique
  69. 0069exact hcanonical_witness
  70. 0070exact hy