FC0013

crt_pairwise_compatible_prefix_normalized_exists_unique

Full zero-inclusive generalized CRT: every arbitrary pairwise-compatible finite list has its exact LCM and a unique normalized simultaneous solution; neither positivity nor an operational merge invariant is assumed.

Alpha v34 checked-use · first admitted v27 · 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.

All finite lists are included, even the empty list and zero moduli. A positive LCM gives x<M; at zero LCM congruence is exact equality and normalization deliberately does not require the impossible x<0.

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. CRTPairwiseCompatiblePrefix(r,s,b,c,l) → ∃ x. ∃ y. CRTNormalizedPrefixSolution(r,s,b,c,l,x,y) ∧ (∀ z. CRTNormalizedPrefixSolution(r,s,b,c,l,z,y) → z = x)

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

Definition DAG

CRTPrefixSolution(r,s,b,c,l,x) · 1CRTPairwiseCompatiblePrefix(r,s,b,c,l) · 1CRTNormalizedPrefixSolution(r,s,b,c,l,x,M) · 3

Actual proof prerequisites

crt_pairwise_compatible_prefix_solution_existscrt_prefix_lcm_exists_unique · checked external prerequisitecrt_prefix_solution_normalized_existscrt_normalized_prefix_solution_unique
Original expanded first-order statement 
forall r s b c l. (forall gcomp_left_index_gfull_normalized_exists_pairs gcomp_right_index_gfull_normalized_exists_pairs gcomp_left_residue_gfull_normalized_exists_pairs gcomp_right_residue_gfull_normalized_exists_pairs gcomp_left_modulus_gfull_normalized_exists_pairs gcomp_right_modulus_gfull_normalized_exists_pairs gcomp_pair_gcd_gfull_normalized_exists_pairs. (exists ff_lt_gcrt_gfull_normalized_exists_pairs_left_bound. ff_lt_gcrt_gfull_normalized_exists_pairs_left_bound + S gcomp_left_index_gfull_normalized_exists_pairs = l) -> (exists ff_lt_gcrt_gfull_normalized_exists_pairs_right_bound. ff_lt_gcrt_gfull_normalized_exists_pairs_right_bound + S gcomp_right_index_gfull_normalized_exists_pairs = l) -> (((exists ff_h_gcrt_gfull_normalized_exists_pairs_left_residue. ff_h_gcrt_gfull_normalized_exists_pairs_left_residue + S (gcomp_left_residue_gfull_normalized_exists_pairs) = S ((S (gcomp_left_index_gfull_normalized_exists_pairs)) * s)) /\ exists ff_q_gcrt_gfull_normalized_exists_pairs_left_residue. r = ff_q_gcrt_gfull_normalized_exists_pairs_left_residue * S ((S (gcomp_left_index_gfull_normalized_exists_pairs)) * s) + (gcomp_left_residue_gfull_normalized_exists_pairs))) -> (((exists ff_h_gcrt_gfull_normalized_exists_pairs_right_residue. ff_h_gcrt_gfull_normalized_exists_pairs_right_residue + S (gcomp_right_residue_gfull_normalized_exists_pairs) = S ((S (gcomp_right_index_gfull_normalized_exists_pairs)) * s)) /\ exists ff_q_gcrt_gfull_normalized_exists_pairs_right_residue. r = ff_q_gcrt_gfull_normalized_exists_pairs_right_residue * S ((S (gcomp_right_index_gfull_normalized_exists_pairs)) * s) + (gcomp_right_residue_gfull_normalized_exists_pairs))) -> (((exists ff_h_gcrt_gfull_normalized_exists_pairs_left_modulus. ff_h_gcrt_gfull_normalized_exists_pairs_left_modulus + S (gcomp_left_modulus_gfull_normalized_exists_pairs) = S ((S (gcomp_left_index_gfull_normalized_exists_pairs)) * c)) /\ exists ff_q_gcrt_gfull_normalized_exists_pairs_left_modulus. b = ff_q_gcrt_gfull_normalized_exists_pairs_left_modulus * S ((S (gcomp_left_index_gfull_normalized_exists_pairs)) * c) + (gcomp_left_modulus_gfull_normalized_exists_pairs))) -> (((exists ff_h_gcrt_gfull_normalized_exists_pairs_right_modulus. ff_h_gcrt_gfull_normalized_exists_pairs_right_modulus + S (gcomp_right_modulus_gfull_normalized_exists_pairs) = S ((S (gcomp_right_index_gfull_normalized_exists_pairs)) * c)) /\ exists ff_q_gcrt_gfull_normalized_exists_pairs_right_modulus. b = ff_q_gcrt_gfull_normalized_exists_pairs_right_modulus * S ((S (gcomp_right_index_gfull_normalized_exists_pairs)) * c) + (gcomp_right_modulus_gfull_normalized_exists_pairs))) -> ((((exists hag_left_factor_gcomp_gfull_normalized_exists_pairs_gcd. gcomp_left_modulus_gfull_normalized_exists_pairs = gcomp_pair_gcd_gfull_normalized_exists_pairs * hag_left_factor_gcomp_gfull_normalized_exists_pairs_gcd) /\ (exists hag_right_factor_gcomp_gfull_normalized_exists_pairs_gcd. gcomp_right_modulus_gfull_normalized_exists_pairs = gcomp_pair_gcd_gfull_normalized_exists_pairs * hag_right_factor_gcomp_gfull_normalized_exists_pairs_gcd)) /\ forall hag_divisor_gcomp_gfull_normalized_exists_pairs_gcd. (exists hag_common_left_gcomp_gfull_normalized_exists_pairs_gcd. gcomp_left_modulus_gfull_normalized_exists_pairs = hag_divisor_gcomp_gfull_normalized_exists_pairs_gcd * hag_common_left_gcomp_gfull_normalized_exists_pairs_gcd) -> (exists hag_common_right_gcomp_gfull_normalized_exists_pairs_gcd. gcomp_right_modulus_gfull_normalized_exists_pairs = hag_divisor_gcomp_gfull_normalized_exists_pairs_gcd * hag_common_right_gcomp_gfull_normalized_exists_pairs_gcd) -> exists hag_greatest_factor_gcomp_gfull_normalized_exists_pairs_gcd. gcomp_pair_gcd_gfull_normalized_exists_pairs = hag_divisor_gcomp_gfull_normalized_exists_pairs_gcd * hag_greatest_factor_gcomp_gfull_normalized_exists_pairs_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_exists_pairs_result hgcrt_mod_right_gcrt_gfull_normalized_exists_pairs_result. gcomp_left_residue_gfull_normalized_exists_pairs + gcomp_pair_gcd_gfull_normalized_exists_pairs * hgcrt_mod_left_gcrt_gfull_normalized_exists_pairs_result = gcomp_right_residue_gfull_normalized_exists_pairs + gcomp_pair_gcd_gfull_normalized_exists_pairs * hgcrt_mod_right_gcrt_gfull_normalized_exists_pairs_result)) -> exists x M. ((((((forall gcrt_common_index_gfull_normalized_exists_chosen_lcm_own gcrt_common_modulus_gfull_normalized_exists_chosen_lcm_own. (exists ff_lt_gcrt_gfull_normalized_exists_chosen_lcm_own_bound. ff_lt_gcrt_gfull_normalized_exists_chosen_lcm_own_bound + S gcrt_common_index_gfull_normalized_exists_chosen_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_exists_chosen_lcm_own_entry. ff_h_gcrt_gfull_normalized_exists_chosen_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_exists_chosen_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_exists_chosen_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_exists_chosen_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_exists_chosen_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_exists_chosen_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_exists_chosen_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_exists_chosen_lcm_own. M = gcrt_common_modulus_gfull_normalized_exists_chosen_lcm_own * gcrt_common_quotient_gfull_normalized_exists_chosen_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_exists_chosen_lcm. (forall gcrt_common_index_gfull_normalized_exists_chosen_lcm_other gcrt_common_modulus_gfull_normalized_exists_chosen_lcm_other. (exists ff_lt_gcrt_gfull_normalized_exists_chosen_lcm_other_bound. ff_lt_gcrt_gfull_normalized_exists_chosen_lcm_other_bound + S gcrt_common_index_gfull_normalized_exists_chosen_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_exists_chosen_lcm_other_entry. ff_h_gcrt_gfull_normalized_exists_chosen_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_exists_chosen_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_exists_chosen_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_exists_chosen_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_exists_chosen_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_exists_chosen_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_exists_chosen_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_exists_chosen_lcm_other. gcrt_lcm_common_gfull_normalized_exists_chosen_lcm = gcrt_common_modulus_gfull_normalized_exists_chosen_lcm_other * gcrt_common_quotient_gfull_normalized_exists_chosen_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_exists_chosen_lcm. gcrt_lcm_common_gfull_normalized_exists_chosen_lcm = M * gcrt_lcm_quotient_gfull_normalized_exists_chosen_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_exists_chosen_bound. ff_lt_gcrt_gfull_normalized_exists_chosen_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_exists_chosen_solution gcrt_solution_residue_gfull_normalized_exists_chosen_solution gcrt_solution_modulus_gfull_normalized_exists_chosen_solution. (exists ff_lt_gcrt_gfull_normalized_exists_chosen_solution_bound. ff_lt_gcrt_gfull_normalized_exists_chosen_solution_bound + S gcrt_solution_index_gfull_normalized_exists_chosen_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_exists_chosen_solution_residue. ff_h_gcrt_gfull_normalized_exists_chosen_solution_residue + S (gcrt_solution_residue_gfull_normalized_exists_chosen_solution) = S ((S (gcrt_solution_index_gfull_normalized_exists_chosen_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_exists_chosen_solution_residue. r = ff_q_gcrt_gfull_normalized_exists_chosen_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_exists_chosen_solution)) * s) + (gcrt_solution_residue_gfull_normalized_exists_chosen_solution))) -> (((exists ff_h_gcrt_gfull_normalized_exists_chosen_solution_modulus. ff_h_gcrt_gfull_normalized_exists_chosen_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_exists_chosen_solution) = S ((S (gcrt_solution_index_gfull_normalized_exists_chosen_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_exists_chosen_solution_modulus. b = ff_q_gcrt_gfull_normalized_exists_chosen_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_exists_chosen_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_exists_chosen_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_exists_chosen_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_exists_chosen_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_exists_chosen_solution * hgcrt_mod_left_gcrt_gfull_normalized_exists_chosen_solution_congruence = gcrt_solution_residue_gfull_normalized_exists_chosen_solution + gcrt_solution_modulus_gfull_normalized_exists_chosen_solution * hgcrt_mod_right_gcrt_gfull_normalized_exists_chosen_solution_congruence))))) /\ forall y. (((((forall gcrt_common_index_gfull_normalized_exists_compared_lcm_own gcrt_common_modulus_gfull_normalized_exists_compared_lcm_own. (exists ff_lt_gcrt_gfull_normalized_exists_compared_lcm_own_bound. ff_lt_gcrt_gfull_normalized_exists_compared_lcm_own_bound + S gcrt_common_index_gfull_normalized_exists_compared_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_exists_compared_lcm_own_entry. ff_h_gcrt_gfull_normalized_exists_compared_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_exists_compared_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_exists_compared_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_exists_compared_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_exists_compared_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_exists_compared_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_exists_compared_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_exists_compared_lcm_own. M = gcrt_common_modulus_gfull_normalized_exists_compared_lcm_own * gcrt_common_quotient_gfull_normalized_exists_compared_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_exists_compared_lcm. (forall gcrt_common_index_gfull_normalized_exists_compared_lcm_other gcrt_common_modulus_gfull_normalized_exists_compared_lcm_other. (exists ff_lt_gcrt_gfull_normalized_exists_compared_lcm_other_bound. ff_lt_gcrt_gfull_normalized_exists_compared_lcm_other_bound + S gcrt_common_index_gfull_normalized_exists_compared_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_exists_compared_lcm_other_entry. ff_h_gcrt_gfull_normalized_exists_compared_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_exists_compared_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_exists_compared_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_exists_compared_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_exists_compared_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_exists_compared_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_exists_compared_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_exists_compared_lcm_other. gcrt_lcm_common_gfull_normalized_exists_compared_lcm = gcrt_common_modulus_gfull_normalized_exists_compared_lcm_other * gcrt_common_quotient_gfull_normalized_exists_compared_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_exists_compared_lcm. gcrt_lcm_common_gfull_normalized_exists_compared_lcm = M * gcrt_lcm_quotient_gfull_normalized_exists_compared_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_exists_compared_bound. ff_lt_gcrt_gfull_normalized_exists_compared_bound + S y = M)) /\ (forall gcrt_solution_index_gfull_normalized_exists_compared_solution gcrt_solution_residue_gfull_normalized_exists_compared_solution gcrt_solution_modulus_gfull_normalized_exists_compared_solution. (exists ff_lt_gcrt_gfull_normalized_exists_compared_solution_bound. ff_lt_gcrt_gfull_normalized_exists_compared_solution_bound + S gcrt_solution_index_gfull_normalized_exists_compared_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_exists_compared_solution_residue. ff_h_gcrt_gfull_normalized_exists_compared_solution_residue + S (gcrt_solution_residue_gfull_normalized_exists_compared_solution) = S ((S (gcrt_solution_index_gfull_normalized_exists_compared_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_exists_compared_solution_residue. r = ff_q_gcrt_gfull_normalized_exists_compared_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_exists_compared_solution)) * s) + (gcrt_solution_residue_gfull_normalized_exists_compared_solution))) -> (((exists ff_h_gcrt_gfull_normalized_exists_compared_solution_modulus. ff_h_gcrt_gfull_normalized_exists_compared_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_exists_compared_solution) = S ((S (gcrt_solution_index_gfull_normalized_exists_compared_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_exists_compared_solution_modulus. b = ff_q_gcrt_gfull_normalized_exists_compared_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_exists_compared_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_exists_compared_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_exists_compared_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_exists_compared_solution_congruence. y + gcrt_solution_modulus_gfull_normalized_exists_compared_solution * hgcrt_mod_left_gcrt_gfull_normalized_exists_compared_solution_congruence = gcrt_solution_residue_gfull_normalized_exists_compared_solution + gcrt_solution_modulus_gfull_normalized_exists_compared_solution * hgcrt_mod_right_gcrt_gfull_normalized_exists_compared_solution_congruence))))) -> y = x)

Complete tactic proof in conservative notation

All 49 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

49 script commands · 14 reading checkpoints · 2 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 (3)
crt pairwise compatible prefix solution existscrt prefix solution normalized existscrt normalized prefix solution unique
01Fix variables and assumptionsL1–6

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 hp
02Establish hsL7–14

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

  1. L7
    have hs : ∃ x. CRTPrefixSolution(r,s,b,c,l,x)Definitions: CRTPrefixSolution(r,s,b,c,l,x)Original native command in the exact edition
  2. L8
    specialize crt_pairwise_compatible_prefix_solution_exists r
  3. L9
    specialize crt_pairwise_compatible_prefix_solution_exists s
  4. L10
    specialize crt_pairwise_compatible_prefix_solution_exists b
  5. L11
    specialize crt_pairwise_compatible_prefix_solution_exists c
  6. L12
    specialize crt_pairwise_compatible_prefix_solution_exists l
  7. L13
    apply crt_pairwise_compatible_prefix_solution_exists
  8. L14
    exact hp
03Separate the logical casesL15–15

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

  1. L15
    cases hs
04Use earlier factsL16–18

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

  1. L16
    specialize crt_prefix_lcm_exists_unique b
  2. L17
    specialize crt_prefix_lcm_exists_unique c
  3. L18
    specialize crt_prefix_lcm_exists_unique l
05Separate the logical casesL19–20

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

  1. L19
    cases crt_prefix_lcm_exists_unique
  2. L20
    cases crt_prefix_lcm_exists_unique_witness
06Establish hnL21–30

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

  1. L21
    have hn : ∃ z. CRTNormalizedPrefixSolution(r,s,b,c,l,z,x1)Definitions: CRTNormalizedPrefixSolution(r,s,b,c,l,z,x1)Original native command in the exact edition
  2. L22
    specialize crt_prefix_solution_normalized_exists r
  3. L23
    specialize crt_prefix_solution_normalized_exists s
  4. L24
    specialize crt_prefix_solution_normalized_exists b
  5. L25
    specialize crt_prefix_solution_normalized_exists c
  6. L26
    specialize crt_prefix_solution_normalized_exists l
  7. L27
    specialize crt_prefix_solution_normalized_exists x1
  8. L28
    specialize crt_prefix_solution_normalized_exists x
  9. L29
    apply crt_prefix_solution_normalized_exists
  10. L30
    exact crt_prefix_lcm_exists_unique_witness_left
07Use earlier factsL31–31

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

  1. L31
    exact hs_witness
08Separate the logical casesL32–32

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

  1. L32
    cases hn
09Construct an explicit witnessL33–34

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

  1. L33
    exists x2
  2. L34
    exists x1
10Separate the logical casesL35–35

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

  1. L35
    split
11Use earlier factsL36–36

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

  1. L36
    exact hn_witness
12Fix variables and assumptionsL37–38

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

  1. L37
    intro y
  2. L38
    intro hy
13Use earlier factsL39–48

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

  1. L39
    specialize crt_normalized_prefix_solution_unique r
  2. L40
    specialize crt_normalized_prefix_solution_unique s
  3. L41
    specialize crt_normalized_prefix_solution_unique b
  4. L42
    specialize crt_normalized_prefix_solution_unique c
  5. L43
    specialize crt_normalized_prefix_solution_unique l
  6. L44
    specialize crt_normalized_prefix_solution_unique x1
  7. L45
    specialize crt_normalized_prefix_solution_unique x2
  8. L46
    specialize crt_normalized_prefix_solution_unique y
  9. L47
    apply crt_normalized_prefix_solution_unique
  10. L48
    exact hn_witness
14Use earlier factsL49–49

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

  1. L49
    exact hy

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro hp
  7. 0007have hs : ∃ x. CRTPrefixSolution(r,s,b,c,l,x)
  8. 0008specialize crt_pairwise_compatible_prefix_solution_exists r
  9. 0009specialize crt_pairwise_compatible_prefix_solution_exists s
  10. 0010specialize crt_pairwise_compatible_prefix_solution_exists b
  11. 0011specialize crt_pairwise_compatible_prefix_solution_exists c
  12. 0012specialize crt_pairwise_compatible_prefix_solution_exists l
  13. 0013apply crt_pairwise_compatible_prefix_solution_exists
  14. 0014exact hp
  15. 0015cases hs
  16. 0016specialize crt_prefix_lcm_exists_unique b
  17. 0017specialize crt_prefix_lcm_exists_unique c
  18. 0018specialize crt_prefix_lcm_exists_unique l
  19. 0019cases crt_prefix_lcm_exists_unique
  20. 0020cases crt_prefix_lcm_exists_unique_witness
  21. 0021have hn : ∃ z. CRTNormalizedPrefixSolution(r,s,b,c,l,z,x1)
  22. 0022specialize crt_prefix_solution_normalized_exists r
  23. 0023specialize crt_prefix_solution_normalized_exists s
  24. 0024specialize crt_prefix_solution_normalized_exists b
  25. 0025specialize crt_prefix_solution_normalized_exists c
  26. 0026specialize crt_prefix_solution_normalized_exists l
  27. 0027specialize crt_prefix_solution_normalized_exists x1
  28. 0028specialize crt_prefix_solution_normalized_exists x
  29. 0029apply crt_prefix_solution_normalized_exists
  30. 0030exact crt_prefix_lcm_exists_unique_witness_left
  31. 0031exact hs_witness
  32. 0032cases hn
  33. 0033exists x2
  34. 0034exists x1
  35. 0035split
  36. 0036exact hn_witness
  37. 0037intro y
  38. 0038intro hy
  39. 0039specialize crt_normalized_prefix_solution_unique r
  40. 0040specialize crt_normalized_prefix_solution_unique s
  41. 0041specialize crt_normalized_prefix_solution_unique b
  42. 0042specialize crt_normalized_prefix_solution_unique c
  43. 0043specialize crt_normalized_prefix_solution_unique l
  44. 0044specialize crt_normalized_prefix_solution_unique x1
  45. 0045specialize crt_normalized_prefix_solution_unique x2
  46. 0046specialize crt_normalized_prefix_solution_unique y
  47. 0047apply crt_normalized_prefix_solution_unique
  48. 0048exact hn_witness
  49. 0049exact hy