PA008I · theorem

prime_mul_residue_reindex_exists

Alpha v34 checked-use theorem · independently closed; not Stable

A nonzero multiplier modulo a prime induces a beta-coded residue reindexing.

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.

Statement with defined notation

∀ p. ∀ n. ∀ a. ∀ b. ∀ c. p = S n → Prime(p) → ¬Dvd(p,a) → Range(b,c,1,n) → ∃ x. ∃ y. ∃ z. ∃ m. BoundedPrefix(x,y,n) ∧ (InjectivePrefix(x,y,n) ∧ ((∀ k. ∀ i. ∀ j. Lt(k,n) → BetaAt(x,y,k,i) → BetaAt(b,c,i,j) → BetaAt(z,m,k,j)) ∧ (∀ k. ∀ i. ∀ j. Lt(k,n) → BetaAt(b,c,k,i) → BetaAt(z,m,k,j) → ModEq(p,a · i,j))))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0003 Dvd PD0004 Prime PD0008 ModEq PD0013 BetaAt PD0018 Range PD0024 BoundedPrefix PD0025 InjectivePrefix

13 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0024 BoundedPrefix PD0025 InjectivePrefix

17 occurrences

Exact expanded native-PA statement
forall p n a b c. p = S n -> ((~(p = 1) /\ forall frm_prime_left_package_prime frm_prime_right_package_prime. p = frm_prime_left_package_prime * frm_prime_right_package_prime -> frm_prime_left_package_prime = 1 \/ frm_prime_right_package_prime = 1)) -> (~(exists frm_factor_package_multiplier. a = p * frm_factor_package_multiplier)) -> (forall ff_i_frp_range_package_range. (exists ff_lt_frp_range_package_range_bound. ff_lt_frp_range_package_range_bound + S ff_i_frp_range_package_range = n) -> (((exists ff_h_frp_range_package_range_decoded. ff_h_frp_range_package_range_decoded + S (1 + ff_i_frp_range_package_range) = S ((S (ff_i_frp_range_package_range)) * c)) /\ exists ff_q_frp_range_package_range_decoded. b = ff_q_frp_range_package_range_decoded * S ((S (ff_i_frp_range_package_range)) * c) + (1 + ff_i_frp_range_package_range)))) -> exists r s z d. (forall fp_i_package_result_bounded. (exists fp_gap_package_result_bounded_index. fp_gap_package_result_bounded_index + S fp_i_package_result_bounded = n) -> exists fp_value_package_result_bounded. ((((exists ff_h_package_result_bounded_entry. ff_h_package_result_bounded_entry + S (fp_value_package_result_bounded) = S ((S (fp_i_package_result_bounded)) * s)) /\ exists ff_q_package_result_bounded_entry. r = ff_q_package_result_bounded_entry * S ((S (fp_i_package_result_bounded)) * s) + (fp_value_package_result_bounded))) /\ (exists fp_gap_package_result_bounded_value. fp_gap_package_result_bounded_value + S fp_value_package_result_bounded = n))) /\ ((forall fp_i_package_result_injective fp_j_package_result_injective fp_value_package_result_injective. (exists fp_gap_package_result_injective_i. fp_gap_package_result_injective_i + S fp_i_package_result_injective = n) -> (exists fp_gap_package_result_injective_j. fp_gap_package_result_injective_j + S fp_j_package_result_injective = n) -> (((exists ff_h_package_result_injective_left. ff_h_package_result_injective_left + S (fp_value_package_result_injective) = S ((S (fp_i_package_result_injective)) * s)) /\ exists ff_q_package_result_injective_left. r = ff_q_package_result_injective_left * S ((S (fp_i_package_result_injective)) * s) + (fp_value_package_result_injective))) -> (((exists ff_h_package_result_injective_right. ff_h_package_result_injective_right + S (fp_value_package_result_injective) = S ((S (fp_j_package_result_injective)) * s)) /\ exists ff_q_package_result_injective_right. r = ff_q_package_result_injective_right * S ((S (fp_j_package_result_injective)) * s) + (fp_value_package_result_injective))) -> fp_i_package_result_injective = fp_j_package_result_injective) /\ ((forall fpr_i_package_result_aligned fpr_j_package_result_aligned fpr_x_package_result_aligned. (exists fpr_h_package_result_aligned. fpr_h_package_result_aligned + S fpr_i_package_result_aligned = n) -> (((exists ff_h_package_result_aligned_map. ff_h_package_result_aligned_map + S (fpr_j_package_result_aligned) = S ((S (fpr_i_package_result_aligned)) * s)) /\ exists ff_q_package_result_aligned_map. r = ff_q_package_result_aligned_map * S ((S (fpr_i_package_result_aligned)) * s) + (fpr_j_package_result_aligned))) -> (((exists ff_h_package_result_aligned_source. ff_h_package_result_aligned_source + S (fpr_x_package_result_aligned) = S ((S (fpr_j_package_result_aligned)) * c)) /\ exists ff_q_package_result_aligned_source. b = ff_q_package_result_aligned_source * S ((S (fpr_j_package_result_aligned)) * c) + (fpr_x_package_result_aligned))) -> (((exists ff_h_package_result_aligned_target. ff_h_package_result_aligned_target + S (fpr_x_package_result_aligned) = S ((S (fpr_i_package_result_aligned)) * d)) /\ exists ff_q_package_result_aligned_target. z = ff_q_package_result_aligned_target * S ((S (fpr_i_package_result_aligned)) * d) + (fpr_x_package_result_aligned)))) /\ (forall fsp_index_package_result_scale fsp_source_package_result_scale fsp_target_package_result_scale. (exists fsp_gap_package_result_scale. fsp_gap_package_result_scale + S fsp_index_package_result_scale = n) -> (((exists fsp_source_height_package_result_scale. fsp_source_height_package_result_scale + S (fsp_source_package_result_scale) = S ((S (fsp_index_package_result_scale)) * c)) /\ exists fsp_source_quotient_package_result_scale. b = fsp_source_quotient_package_result_scale * S ((S (fsp_index_package_result_scale)) * c) + (fsp_source_package_result_scale))) -> (((exists fsp_target_height_package_result_scale. fsp_target_height_package_result_scale + S (fsp_target_package_result_scale) = S ((S (fsp_index_package_result_scale)) * d)) /\ exists fsp_target_quotient_package_result_scale. z = fsp_target_quotient_package_result_scale * S ((S (fsp_index_package_result_scale)) * d) + (fsp_target_package_result_scale))) -> (exists fsp_mod_left_package_result_scale fsp_mod_right_package_result_scale. a * fsp_source_package_result_scale + p * fsp_mod_left_package_result_scale = fsp_target_package_result_scale + p * fsp_mod_right_package_result_scale))))

Proof neighborhood

Direct theorem prerequisites

PA001A le_refl PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008D fermat_index_map_bounded PA008E prime_mul_index_map_injective PA008G beta_successor_range_reindex_aligned PA008H beta_successor_range_scale_mod

Direct theorem dependents

PA008J prime_mul_residue_product_balance

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

85 script commands · 20 reading checkpoints · 6 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 (7)
le reflprime mul index map exists up tobeta successor lift existsfermat index map boundedprime mul index map injectivebeta successor range reindex alignedbeta successor range scale mod
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hnotdiv
  9. L9
    intro hrange
02Establish hmapsL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mul index map exists up to.

  1. L10
    have hmaps : ∃ r. ∃ s. ∀ x. Lt(x,n) → ∃ y. Lt(y,n) ∧ (BetaAt(r,s,x,y) ∧ ModEq(p,a · S x,S y))Definitions: Lt(x,n)Lt(y,n)BetaAt(r,s,x,y)ModEq(p,a · S x,S y)Original native command in the exact edition
  2. L11
    specialize prime_mul_index_map_exists_up_to n
  3. L12
    specialize prime_mul_index_map_exists_up_to n
  4. L13
    specialize prime_mul_index_map_exists_up_to p
  5. L14
    specialize prime_mul_index_map_exists_up_to a
  6. L15
    apply prime_mul_index_map_exists_up_to
  7. L16
    specialize le_refl n
  8. L17
    exact le_refl
  9. L18
    exact hpn
  10. L19
    exact hp
03Use earlier factsL20–20

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

  1. L20
    exact hnotdiv
04Separate the logical casesL21–22

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

  1. L21
    cases hmaps
  2. L22
    cases hmaps_witness
05Establish hliftsL23–27

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

  1. L23
    have hlifts : ∃ z. ∃ d. ∀ y. ∀ m. Lt(y,n) → BetaAt(x,x1,y,m) → BetaAt(z,d,y,S m)Definitions: Lt(y,n)BetaAt(x,x1,y,m)BetaAt(z,d,y,S m)Original native command in the exact edition
  2. L24
    specialize beta_successor_lift_exists x
  3. L25
    specialize beta_successor_lift_exists x1
  4. L26
    specialize beta_successor_lift_exists n
  5. L27
    exact beta_successor_lift_exists
06Separate the logical casesL28–29

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

  1. L28
    cases hlifts
  2. L29
    cases hlifts_witness
07Establish hboundedL30–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat index map bounded.

  1. L30
    have hbounded : BoundedPrefix(x,x1,n)Definitions: BoundedPrefix(x,x1,n)Original native command in the exact edition
  2. L31
    specialize fermat_index_map_bounded x
  3. L32
    specialize fermat_index_map_bounded x1
  4. L33
    specialize fermat_index_map_bounded n
  5. L34
    specialize fermat_index_map_bounded p
  6. L35
    specialize fermat_index_map_bounded a
  7. L36
    apply fermat_index_map_bounded
  8. L37
    exact hmaps_witness_witness
08Establish hinjectiveL38–47

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mul index map injective.

  1. L38
    have hinjective : InjectivePrefix(x,x1,n)Definitions: InjectivePrefix(x,x1,n)Original native command in the exact edition
  2. L39
    specialize prime_mul_index_map_injective p
  3. L40
    specialize prime_mul_index_map_injective n
  4. L41
    specialize prime_mul_index_map_injective a
  5. L42
    specialize prime_mul_index_map_injective x
  6. L43
    specialize prime_mul_index_map_injective x1
  7. L44
    apply prime_mul_index_map_injective
  8. L45
    exact hpn
  9. L46
    exact hp
  10. L47
    exact hnotdiv
09Use earlier factsL48–48

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

  1. L48
    exact hmaps_witness_witness
10Establish halignedL49–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta successor range reindex aligned.

  1. L49
    have haligned : ∀ fpr_i_package_aligned. ∀ fpr_j_package_aligned. ∀ fpr_x_package_aligned. Lt(fpr_i_package_aligned,n) → BetaAt(x,x1,fpr_i_package_aligned,fpr_j_package_aligned) → BetaAt(b,c,fpr_j_package_aligned,fpr_x_package_aligned) → BetaAt(x2,x3,fpr_i_package_aligned,fpr_x_package_aligned)Definitions: Lt(fpr_i_package_aligned,n)BetaAt(x,x1,fpr_i_package_aligned,fpr_j_package_aligned)BetaAt(b,c,fpr_j_package_aligned,fpr_x_package_aligned)BetaAt(x2,x3,fpr_i_package_aligned,fpr_x_package_aligned)Original native command in the exact edition
  2. L50
    specialize beta_successor_range_reindex_aligned x
  3. L51
    specialize beta_successor_range_reindex_aligned x1
  4. L52
    specialize beta_successor_range_reindex_aligned b
  5. L53
    specialize beta_successor_range_reindex_aligned c
  6. L54
    specialize beta_successor_range_reindex_aligned x2
  7. L55
    specialize beta_successor_range_reindex_aligned x3
  8. L56
    specialize beta_successor_range_reindex_aligned n
  9. L57
    apply beta_successor_range_reindex_aligned
  10. L58
    exact hbounded
11Use earlier factsL59–60

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

  1. L59
    exact hrange
  2. L60
    exact hlifts_witness_witness
12Establish hscaleL61–70

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

  1. L61
    have hscale : ∀ fsp_index_package_scale. ∀ fsp_source_package_scale. ∀ fsp_target_package_scale. Lt(fsp_index_package_scale,n) → BetaAt(b,c,fsp_index_package_scale,fsp_source_package_scale) → BetaAt(x2,x3,fsp_index_package_scale,fsp_target_package_scale) → ModEq(p,a · fsp_source_package_scale,fsp_target_package_scale)Definitions: Lt(fsp_index_package_scale,n)BetaAt(b,c,fsp_index_package_scale,fsp_source_package_scale)BetaAt(x2,x3,fsp_index_package_scale,fsp_target_package_scale)ModEq(p,a · fsp_source_package_scale,fsp_target_package_scale)Original native command in the exact edition
  2. L62
    specialize beta_successor_range_scale_mod p
  3. L63
    specialize beta_successor_range_scale_mod n
  4. L64
    specialize beta_successor_range_scale_mod a
  5. L65
    specialize beta_successor_range_scale_mod x
  6. L66
    specialize beta_successor_range_scale_mod x1
  7. L67
    specialize beta_successor_range_scale_mod b
  8. L68
    specialize beta_successor_range_scale_mod c
  9. L69
    specialize beta_successor_range_scale_mod x2
  10. L70
    specialize beta_successor_range_scale_mod x3
13Use earlier factsL71–74

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

  1. L71
    apply beta_successor_range_scale_mod
  2. L72
    exact hmaps_witness_witness
  3. L73
    exact hrange
  4. L74
    exact hlifts_witness_witness
14Construct an explicit witnessL75–78

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

  1. L75
    exists x
  2. L76
    exists x1
  3. L77
    exists x2
  4. L78
    exists x3
15Separate the logical casesL79–79

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

  1. L79
    split
16Use earlier factsL80–80

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

  1. L80
    exact hbounded
17Separate the logical casesL81–81

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

  1. L81
    split
18Use earlier factsL82–82

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

  1. L82
    exact hinjective
19Separate the logical casesL83–83

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

  1. L83
    split
20Use earlier factsL84–85

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

  1. L84
    exact haligned
  2. L85
    exact hscale

Library-wide reading audit

Original defined command ledger · 85 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hnotdiv
  9. 0009intro hrange
  10. 0010have hmaps : ∃ r. ∃ s. ∀ x. Lt(x,n) → ∃ y. Lt(y,n) ∧ (BetaAt(r,s,x,y) ∧ ModEq(p,a · S x,S y))
    Exact native replay linehave hmaps : exists r s. (forall frm_index_package_map. (exists frm_gap_package_map_index_bound. frm_gap_package_map_index_bound + S frm_index_package_map = n) -> (exists frm_residue_package_map_result. (exists frm_gap_package_map_result_residue_bound. frm_gap_package_map_result_residue_bound + S frm_residue_package_map_result = n) /\ ((((exists ff_h_frm_package_map_result_decoded. ff_h_frm_package_map_result_decoded + S (frm_residue_package_map_result) = S ((S (frm_index_package_map)) * s)) /\ exists ff_q_frm_package_map_result_decoded. r = ff_q_frm_package_map_result_decoded * S ((S (frm_index_package_map)) * s) + (frm_residue_package_map_result))) /\ (exists frm_mod_left_package_map_result_congruence frm_mod_right_package_map_result_congruence. a * S frm_index_package_map + p * frm_mod_left_package_map_result_congruence = S frm_residue_package_map_result + p * frm_mod_right_package_map_result_congruence))))
  11. 0011specialize prime_mul_index_map_exists_up_to n
  12. 0012specialize prime_mul_index_map_exists_up_to n
  13. 0013specialize prime_mul_index_map_exists_up_to p
  14. 0014specialize prime_mul_index_map_exists_up_to a
  15. 0015apply prime_mul_index_map_exists_up_to
  16. 0016specialize le_refl n
  17. 0017exact le_refl
  18. 0018exact hpn
  19. 0019exact hp
  20. 0020exact hnotdiv
  21. 0021cases hmaps
  22. 0022cases hmaps_witness
  23. 0023have hlifts : ∃ z. ∃ d. ∀ y. ∀ m. Lt(y,n) → BetaAt(x,x1,y,m) → BetaAt(z,d,y,S m)
    Exact native replay linehave hlifts : exists z d. (forall frr_index_package_lift frr_value_package_lift. (exists frr_gap_package_lift. frr_gap_package_lift + S frr_index_package_lift = n) -> (((exists ff_h_frr_package_lift_source. ff_h_frr_package_lift_source + S (frr_value_package_lift) = S ((S (frr_index_package_lift)) * x1)) /\ exists ff_q_frr_package_lift_source. x = ff_q_frr_package_lift_source * S ((S (frr_index_package_lift)) * x1) + (frr_value_package_lift))) -> (((exists frm_height_frr_package_lift_target. frm_height_frr_package_lift_target + S (S frr_value_package_lift) = S ((S (frr_index_package_lift)) * d)) /\ exists frm_quotient_frr_package_lift_target. z = frm_quotient_frr_package_lift_target * S ((S (frr_index_package_lift)) * d) + (S frr_value_package_lift))))
  24. 0024specialize beta_successor_lift_exists x
  25. 0025specialize beta_successor_lift_exists x1
  26. 0026specialize beta_successor_lift_exists n
  27. 0027exact beta_successor_lift_exists
  28. 0028cases hlifts
  29. 0029cases hlifts_witness
  30. 0030have hbounded : BoundedPrefix(x,x1,n)
    Exact native replay linehave hbounded : forall fp_i_package_bounded. (exists fp_gap_package_bounded_index. fp_gap_package_bounded_index + S fp_i_package_bounded = n) -> exists fp_value_package_bounded. ((((exists ff_h_package_bounded_entry. ff_h_package_bounded_entry + S (fp_value_package_bounded) = S ((S (fp_i_package_bounded)) * x1)) /\ exists ff_q_package_bounded_entry. x = ff_q_package_bounded_entry * S ((S (fp_i_package_bounded)) * x1) + (fp_value_package_bounded))) /\ (exists fp_gap_package_bounded_value. fp_gap_package_bounded_value + S fp_value_package_bounded = n))
  31. 0031specialize fermat_index_map_bounded x
  32. 0032specialize fermat_index_map_bounded x1
  33. 0033specialize fermat_index_map_bounded n
  34. 0034specialize fermat_index_map_bounded p
  35. 0035specialize fermat_index_map_bounded a
  36. 0036apply fermat_index_map_bounded
  37. 0037exact hmaps_witness_witness
  38. 0038have hinjective : InjectivePrefix(x,x1,n)
    Exact native replay linehave hinjective : forall fp_i_package_injective fp_j_package_injective fp_value_package_injective. (exists fp_gap_package_injective_i. fp_gap_package_injective_i + S fp_i_package_injective = n) -> (exists fp_gap_package_injective_j. fp_gap_package_injective_j + S fp_j_package_injective = n) -> (((exists ff_h_package_injective_left. ff_h_package_injective_left + S (fp_value_package_injective) = S ((S (fp_i_package_injective)) * x1)) /\ exists ff_q_package_injective_left. x = ff_q_package_injective_left * S ((S (fp_i_package_injective)) * x1) + (fp_value_package_injective))) -> (((exists ff_h_package_injective_right. ff_h_package_injective_right + S (fp_value_package_injective) = S ((S (fp_j_package_injective)) * x1)) /\ exists ff_q_package_injective_right. x = ff_q_package_injective_right * S ((S (fp_j_package_injective)) * x1) + (fp_value_package_injective))) -> fp_i_package_injective = fp_j_package_injective
  39. 0039specialize prime_mul_index_map_injective p
  40. 0040specialize prime_mul_index_map_injective n
  41. 0041specialize prime_mul_index_map_injective a
  42. 0042specialize prime_mul_index_map_injective x
  43. 0043specialize prime_mul_index_map_injective x1
  44. 0044apply prime_mul_index_map_injective
  45. 0045exact hpn
  46. 0046exact hp
  47. 0047exact hnotdiv
  48. 0048exact hmaps_witness_witness
  49. 0049have haligned : ∀ fpr_i_package_aligned. ∀ fpr_j_package_aligned. ∀ fpr_x_package_aligned. Lt(fpr_i_package_aligned,n) → BetaAt(x,x1,fpr_i_package_aligned,fpr_j_package_aligned) → BetaAt(b,c,fpr_j_package_aligned,fpr_x_package_aligned) → BetaAt(x2,x3,fpr_i_package_aligned,fpr_x_package_aligned)
    Exact native replay linehave haligned : forall fpr_i_package_aligned fpr_j_package_aligned fpr_x_package_aligned. (exists fpr_h_package_aligned. fpr_h_package_aligned + S fpr_i_package_aligned = n) -> (((exists ff_h_package_aligned_map. ff_h_package_aligned_map + S (fpr_j_package_aligned) = S ((S (fpr_i_package_aligned)) * x1)) /\ exists ff_q_package_aligned_map. x = ff_q_package_aligned_map * S ((S (fpr_i_package_aligned)) * x1) + (fpr_j_package_aligned))) -> (((exists ff_h_package_aligned_source. ff_h_package_aligned_source + S (fpr_x_package_aligned) = S ((S (fpr_j_package_aligned)) * c)) /\ exists ff_q_package_aligned_source. b = ff_q_package_aligned_source * S ((S (fpr_j_package_aligned)) * c) + (fpr_x_package_aligned))) -> (((exists ff_h_package_aligned_target. ff_h_package_aligned_target + S (fpr_x_package_aligned) = S ((S (fpr_i_package_aligned)) * x3)) /\ exists ff_q_package_aligned_target. x2 = ff_q_package_aligned_target * S ((S (fpr_i_package_aligned)) * x3) + (fpr_x_package_aligned)))
  50. 0050specialize beta_successor_range_reindex_aligned x
  51. 0051specialize beta_successor_range_reindex_aligned x1
  52. 0052specialize beta_successor_range_reindex_aligned b
  53. 0053specialize beta_successor_range_reindex_aligned c
  54. 0054specialize beta_successor_range_reindex_aligned x2
  55. 0055specialize beta_successor_range_reindex_aligned x3
  56. 0056specialize beta_successor_range_reindex_aligned n
  57. 0057apply beta_successor_range_reindex_aligned
  58. 0058exact hbounded
  59. 0059exact hrange
  60. 0060exact hlifts_witness_witness
  61. 0061have hscale : ∀ fsp_index_package_scale. ∀ fsp_source_package_scale. ∀ fsp_target_package_scale. Lt(fsp_index_package_scale,n) → BetaAt(b,c,fsp_index_package_scale,fsp_source_package_scale) → BetaAt(x2,x3,fsp_index_package_scale,fsp_target_package_scale) → ModEq(p,a · fsp_source_package_scale,fsp_target_package_scale)
    Exact native replay linehave hscale : forall fsp_index_package_scale fsp_source_package_scale fsp_target_package_scale. (exists fsp_gap_package_scale. fsp_gap_package_scale + S fsp_index_package_scale = n) -> (((exists fsp_source_height_package_scale. fsp_source_height_package_scale + S (fsp_source_package_scale) = S ((S (fsp_index_package_scale)) * c)) /\ exists fsp_source_quotient_package_scale. b = fsp_source_quotient_package_scale * S ((S (fsp_index_package_scale)) * c) + (fsp_source_package_scale))) -> (((exists fsp_target_height_package_scale. fsp_target_height_package_scale + S (fsp_target_package_scale) = S ((S (fsp_index_package_scale)) * x3)) /\ exists fsp_target_quotient_package_scale. x2 = fsp_target_quotient_package_scale * S ((S (fsp_index_package_scale)) * x3) + (fsp_target_package_scale))) -> (exists fsp_mod_left_package_scale fsp_mod_right_package_scale. a * fsp_source_package_scale + p * fsp_mod_left_package_scale = fsp_target_package_scale + p * fsp_mod_right_package_scale)
  62. 0062specialize beta_successor_range_scale_mod p
  63. 0063specialize beta_successor_range_scale_mod n
  64. 0064specialize beta_successor_range_scale_mod a
  65. 0065specialize beta_successor_range_scale_mod x
  66. 0066specialize beta_successor_range_scale_mod x1
  67. 0067specialize beta_successor_range_scale_mod b
  68. 0068specialize beta_successor_range_scale_mod c
  69. 0069specialize beta_successor_range_scale_mod x2
  70. 0070specialize beta_successor_range_scale_mod x3
  71. 0071apply beta_successor_range_scale_mod
  72. 0072exact hmaps_witness_witness
  73. 0073exact hrange
  74. 0074exact hlifts_witness_witness
  75. 0075exists x
  76. 0076exists x1
  77. 0077exists x2
  78. 0078exists x3
  79. 0079split
  80. 0080exact hbounded
  81. 0081split
  82. 0082exact hinjective
  83. 0083split
  84. 0084exact haligned
  85. 0085exact hscale