PA007C · theorem

gauss_signed_half_magnitude_injective

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

The positive signed-half magnitude prefix is injective over the full beta-coded half range.

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. ∀ h. ∀ a. ∀ b. ∀ c. ∀ mb. ∀ mc. ∀ sb. ∀ sc. p = 2 · h + 1 → Prime(p) → ¬Dvd(p,a) → Range(b,c,1,h) → (∀ x. Lt(x,h) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(mb,mc,x,z) ∧ (BetaAt(sb,sc,x,n) ∧ (Lt(0,z) ∧ (Le(z,h) ∧ ((n = 0 ∨ n = 1) ∧ (n = 0 ∧ ModEq(p,a · y,z) ∨ n = 1 ∧ ModEq(p,a · y,2 · h · z)))))))) → InjectivePrefix(mb,mc,h)

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

PD0001 Le PD0002 Lt PD0003 Dvd PD0004 Prime PD0008 ModEq PD0013 BetaAt PD0018 Range PD0025 InjectivePrefix

12 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0030 UnitResidue

28 occurrences

Exact expanded native-PA statement
forall p h a b c mb mc sb sc. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_collision_prime gsp_prime_right_collision_prime. p = gsp_prime_left_collision_prime * gsp_prime_right_collision_prime -> gsp_prime_left_collision_prime = 1 \/ gsp_prime_right_collision_prime = 1)) -> (~(exists gsp_divisor_factor_collision_multiplier. a = p * gsp_divisor_factor_collision_multiplier)) -> (forall gsp_range_index_injective_source. (exists gsp_lt_gap_injective_source_range_bound. gsp_lt_gap_injective_source_range_bound + S gsp_range_index_injective_source = h) -> (((exists gsp_beta_height_injective_source_range_entry. gsp_beta_height_injective_source_range_entry + S (1 + gsp_range_index_injective_source) = S ((S (gsp_range_index_injective_source)) * c)) /\ exists gsp_beta_quotient_injective_source_range_entry. b = gsp_beta_quotient_injective_source_range_entry * S ((S (gsp_range_index_injective_source)) * c) + (1 + gsp_range_index_injective_source)))) -> (forall gsp_index_injective_signed_source. (exists gsp_lt_gap_injective_signed_source_index_bound. gsp_lt_gap_injective_signed_source_index_bound + S gsp_index_injective_signed_source = h) -> (exists gsp_value_injective_signed_source_entry gsp_magnitude_injective_signed_source_entry gsp_sign_injective_signed_source_entry. (((exists ff_h_gsp_injective_signed_source_entry_source. ff_h_gsp_injective_signed_source_entry_source + S (gsp_value_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * c)) /\ exists ff_q_gsp_injective_signed_source_entry_source. b = ff_q_gsp_injective_signed_source_entry_source * S ((S (gsp_index_injective_signed_source)) * c) + (gsp_value_injective_signed_source_entry))) /\ ((((exists ff_h_gsp_injective_signed_source_entry_magnitude. ff_h_gsp_injective_signed_source_entry_magnitude + S (gsp_magnitude_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * mc)) /\ exists ff_q_gsp_injective_signed_source_entry_magnitude. mb = ff_q_gsp_injective_signed_source_entry_magnitude * S ((S (gsp_index_injective_signed_source)) * mc) + (gsp_magnitude_injective_signed_source_entry))) /\ ((((exists ff_h_gsp_injective_signed_source_entry_sign. ff_h_gsp_injective_signed_source_entry_sign + S (gsp_sign_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * sc)) /\ exists ff_q_gsp_injective_signed_source_entry_sign. sb = ff_q_gsp_injective_signed_source_entry_sign * S ((S (gsp_index_injective_signed_source)) * sc) + (gsp_sign_injective_signed_source_entry))) /\ ((exists gsp_lt_gap_injective_signed_source_entry_positive. gsp_lt_gap_injective_signed_source_entry_positive + S 0 = gsp_magnitude_injective_signed_source_entry) /\ ((exists gsp_le_gap_injective_signed_source_entry_bounded. gsp_le_gap_injective_signed_source_entry_bounded + gsp_magnitude_injective_signed_source_entry = h) /\ ((gsp_sign_injective_signed_source_entry = 0 \/ gsp_sign_injective_signed_source_entry = 1) /\ (((gsp_sign_injective_signed_source_entry = 0 /\ (exists gsp_mod_left_injective_signed_source_entry_lower gsp_mod_right_injective_signed_source_entry_lower. (a * gsp_value_injective_signed_source_entry) + p * gsp_mod_left_injective_signed_source_entry_lower = (gsp_magnitude_injective_signed_source_entry) + p * gsp_mod_right_injective_signed_source_entry_lower)) \/ (gsp_sign_injective_signed_source_entry = 1 /\ (exists gsp_mod_left_injective_signed_source_entry_reflected gsp_mod_right_injective_signed_source_entry_reflected. (a * gsp_value_injective_signed_source_entry) + p * gsp_mod_left_injective_signed_source_entry_reflected = ((2 * h) * gsp_magnitude_injective_signed_source_entry) + p * gsp_mod_right_injective_signed_source_entry_reflected))))))))))) -> (forall fp_i_signed_magnitude_injective fp_j_signed_magnitude_injective fp_value_signed_magnitude_injective. (exists fp_gap_signed_magnitude_injective_i. fp_gap_signed_magnitude_injective_i + S fp_i_signed_magnitude_injective = h) -> (exists fp_gap_signed_magnitude_injective_j. fp_gap_signed_magnitude_injective_j + S fp_j_signed_magnitude_injective = h) -> (((exists ff_h_signed_magnitude_injective_left. ff_h_signed_magnitude_injective_left + S (fp_value_signed_magnitude_injective) = S ((S (fp_i_signed_magnitude_injective)) * mc)) /\ exists ff_q_signed_magnitude_injective_left. mb = ff_q_signed_magnitude_injective_left * S ((S (fp_i_signed_magnitude_injective)) * mc) + (fp_value_signed_magnitude_injective))) -> (((exists ff_h_signed_magnitude_injective_right. ff_h_signed_magnitude_injective_right + S (fp_value_signed_magnitude_injective) = S ((S (fp_j_signed_magnitude_injective)) * mc)) /\ exists ff_q_signed_magnitude_injective_right. mb = ff_q_signed_magnitude_injective_right * S ((S (fp_j_signed_magnitude_injective)) * mc) + (fp_value_signed_magnitude_injective))) -> fp_i_signed_magnitude_injective = fp_j_signed_magnitude_injective)

Proof neighborhood

Direct theorem prerequisites

PA002F beta_at_unique PA0034 beta_half_range_entry_bounds PA0032 beta_range_entry_eq PA000E add_succ_left PA0001 zero_add PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000G mul_succ_left PA000D mul_zero_left PA0033 lt_of_le_of_lt PA000J add_eq_zero_left PA000F add_comm PA007A gauss_same_sign_scaled_source_unique PA007B gauss_mixed_sign_scaled_source_impossible PA003T beta_range_injective

Direct theorem dependents

PA0085 gauss_lemma_power_congruence_exists PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum

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

281 script commands · 54 reading checkpoints · 24 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 (14)
beta at uniquebeta half range entry boundsbeta range entry eqadd succ leftzero addadd le add rightadd le add leftle translt of le of ltadd eq zero leftadd commgauss same sign scaled source uniquegauss mixed sign scaled source impossiblebeta range injective
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro mb
  7. L7
    intro mc
  8. L8
    intro sb
  9. L9
    intro sc
  10. L10
    intro hpodd
02Fix variables and assumptionsL11–20

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

  1. L11
    intro hp
  2. L12
    intro hnotdiv
  3. L13
    intro hrange
  4. L14
    intro hprefix
  5. L15
    intro i
  6. L16
    intro j
  7. L17
    intro m
  8. L18
    intro hi
  9. L19
    intro hj
  10. L20
    intro hmi
03Fix variables and assumptionsL21–21

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

  1. L21
    intro hmj
04Establish hentryiL22–25

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

  1. L22
    have hentryi · expand full local formula (631 characters)have hentryi : ∃ gsp_value_injective_entry_i. ∃ gsp_magnitude_injective_entry_i. ∃ gsp_sign_injective_entry_i. BetaAt(b,c,i,gsp_value_injective_entry_i) ∧ (BetaAt(mb,mc,i,gsp_magnitude_injective_entry_i) ∧ (BetaAt(sb,sc,i,gsp_sign_injective_entry_i) ∧ (Lt(0,gsp_magnitude_injective_entry_i) ∧ (Le(gsp_magnitude_injective_entry_i,h) ∧ ((gsp_sign_injective_entry_i = 0 ∨ gsp_sign_injective_entry_i = 1) ∧ (gsp_sign_injective_entry_i = 0 ∧ ModEq(p,a · gsp_value_injective_entry_i,gsp_magnitude_injective_entry_i) ∨ gsp_sign_injective_entry_i = 1 ∧ ModEq(p,a · gsp_value_injective_entry_i,2 · h · gsp_magnitude_injective_entry_i)))))))
    Definitions: BetaAt(b,c,i,gsp_value_injective_entry_i)BetaAt(mb,mc,i,gsp_magnitude_injective_entry_i)BetaAt(sb,sc,i,gsp_sign_injective_entry_i)Lt(0,gsp_magnitude_injective_entry_i)Le(gsp_magnitude_injective_entry_i,h)ModEq(p,a · gsp_value_injective_entry_i,gsp_magnitude_injective_entry_i)ModEq(p,a · gsp_value_injective_entry_i,2 · h · gsp_magnitude_injective_entry_i)Original native command in the exact edition
  2. L23
    specialize hprefix i
  3. L24
    apply hprefix
  4. L25
    exact hi
05Separate the logical casesL26–34

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

  1. L26
    cases hentryi
  2. L27
    cases hentryi_witness
  3. L28
    cases hentryi_witness_witness
  4. L29
    cases hentryi_witness_witness_witness
  5. L30
    cases hentryi_witness_witness_witness_right
  6. L31
    cases hentryi_witness_witness_witness_right_right
  7. L32
    cases hentryi_witness_witness_witness_right_right_right
  8. L33
    cases hentryi_witness_witness_witness_right_right_right_right
  9. L34
    cases hentryi_witness_witness_witness_right_right_right_right_right
06Establish hentryjL35–38

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

  1. L35
    have hentryj · expand full local formula (631 characters)have hentryj : ∃ gsp_value_injective_entry_j. ∃ gsp_magnitude_injective_entry_j. ∃ gsp_sign_injective_entry_j. BetaAt(b,c,j,gsp_value_injective_entry_j) ∧ (BetaAt(mb,mc,j,gsp_magnitude_injective_entry_j) ∧ (BetaAt(sb,sc,j,gsp_sign_injective_entry_j) ∧ (Lt(0,gsp_magnitude_injective_entry_j) ∧ (Le(gsp_magnitude_injective_entry_j,h) ∧ ((gsp_sign_injective_entry_j = 0 ∨ gsp_sign_injective_entry_j = 1) ∧ (gsp_sign_injective_entry_j = 0 ∧ ModEq(p,a · gsp_value_injective_entry_j,gsp_magnitude_injective_entry_j) ∨ gsp_sign_injective_entry_j = 1 ∧ ModEq(p,a · gsp_value_injective_entry_j,2 · h · gsp_magnitude_injective_entry_j)))))))
    Definitions: BetaAt(b,c,j,gsp_value_injective_entry_j)BetaAt(mb,mc,j,gsp_magnitude_injective_entry_j)BetaAt(sb,sc,j,gsp_sign_injective_entry_j)Lt(0,gsp_magnitude_injective_entry_j)Le(gsp_magnitude_injective_entry_j,h)ModEq(p,a · gsp_value_injective_entry_j,gsp_magnitude_injective_entry_j)ModEq(p,a · gsp_value_injective_entry_j,2 · h · gsp_magnitude_injective_entry_j)Original native command in the exact edition
  2. L36
    specialize hprefix j
  3. L37
    apply hprefix
  4. L38
    exact hj
07Separate the logical casesL39–47

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

  1. L39
    cases hentryj
  2. L40
    cases hentryj_witness
  3. L41
    cases hentryj_witness_witness
  4. L42
    cases hentryj_witness_witness_witness
  5. L43
    cases hentryj_witness_witness_witness_right
  6. L44
    cases hentryj_witness_witness_witness_right_right
  7. L45
    cases hentryj_witness_witness_witness_right_right_right
  8. L46
    cases hentryj_witness_witness_witness_right_right_right_right
  9. L47
    cases hentryj_witness_witness_witness_right_right_right_right_right
08Establish hmagiL48–56

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

  1. L48
    have hmagi : m = x1
  2. L49
    specialize beta_at_unique mb
  3. L50
    specialize beta_at_unique mc
  4. L51
    specialize beta_at_unique i
  5. L52
    specialize beta_at_unique m
  6. L53
    specialize beta_at_unique x1
  7. L54
    apply beta_at_unique
  8. L55
    exact hmi
  9. L56
    exact hentryi_witness_witness_witness_right_left
09Establish hmagjL57–66

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

  1. L57
    have hmagj : m = x4
  2. L58
    specialize beta_at_unique mb
  3. L59
    specialize beta_at_unique mc
  4. L60
    specialize beta_at_unique j
  5. L61
    specialize beta_at_unique m
  6. L62
    specialize beta_at_unique x4
  7. L63
    apply beta_at_unique
  8. L64
    exact hmj
  9. L65
    exact hentryj_witness_witness_witness_right_left
  10. L66
    rewrite <- hmagi at hentryi_witness_witness_witness_right_right_right_right_right_right
10Calculate and transport equalitiesL67–69

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

  1. L67
    rewrite <- hmagi at hentryi_witness_witness_witness_right_right_right_right_right_right
  2. L68
    rewrite <- hmagj at hentryj_witness_witness_witness_right_right_right_right_right_right
  3. L69
    rewrite <- hmagj at hentryj_witness_witness_witness_right_right_right_right_right_right
11Establish hisignedL70–71

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

  1. L70
    have hisigned : x2 = 0 ∧ ModEq(p,a · x,m) ∨ x2 = 1 ∧ ModEq(p,a · x,2 · h · m)Definitions: ModEq(p,a · x,m)ModEq(p,a · x,2 · h · m)Original native command in the exact edition
  2. L71
    exact hentryi_witness_witness_witness_right_right_right_right_right_right
12Establish hjsignedL72–73

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

  1. L72
    have hjsigned : x5 = 0 ∧ ModEq(p,a · x3,m) ∨ x5 = 1 ∧ ModEq(p,a · x3,2 · h · m)Definitions: ModEq(p,a · x3,m)ModEq(p,a · x3,2 · h · m)Original native command in the exact edition
  2. L73
    exact hentryj_witness_witness_witness_right_right_right_right_right_right
13Establish hxboundsL74–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta half range entry bounds.

  1. L74
    have hxbounds : UnitResidue(p,x)Definitions: UnitResidue(p,x)Original native command in the exact edition
  2. L75
    specialize beta_half_range_entry_bounds p
  3. L76
    specialize beta_half_range_entry_bounds h
  4. L77
    specialize beta_half_range_entry_bounds b
  5. L78
    specialize beta_half_range_entry_bounds c
  6. L79
    specialize beta_half_range_entry_bounds i
  7. L80
    specialize beta_half_range_entry_bounds x
  8. L81
    apply beta_half_range_entry_bounds
  9. L82
    exact hpodd
  10. L83
    exact hrange
14Use earlier factsL84–85

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

  1. L84
    exact hi
  2. L85
    exact hentryi_witness_witness_witness_left
15Establish hyboundsL86–95

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta half range entry bounds.

  1. L86
    have hybounds : UnitResidue(p,x3)Definitions: UnitResidue(p,x3)Original native command in the exact edition
  2. L87
    specialize beta_half_range_entry_bounds p
  3. L88
    specialize beta_half_range_entry_bounds h
  4. L89
    specialize beta_half_range_entry_bounds b
  5. L90
    specialize beta_half_range_entry_bounds c
  6. L91
    specialize beta_half_range_entry_bounds j
  7. L92
    specialize beta_half_range_entry_bounds x3
  8. L93
    apply beta_half_range_entry_bounds
  9. L94
    exact hpodd
  10. L95
    exact hrange
16Use earlier factsL96–97

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

  1. L96
    exact hj
  2. L97
    exact hentryj_witness_witness_witness_left
17Separate the logical casesL98–99

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

  1. L98
    cases hxbounds
  2. L99
    cases hybounds
18Establish hxvalueL100–109

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

  1. L100
    have hxvalue : x = 1 + i
  2. L101
    specialize beta_range_entry_eq b
  3. L102
    specialize beta_range_entry_eq c
  4. L103
    specialize beta_range_entry_eq 1
  5. L104
    specialize beta_range_entry_eq h
  6. L105
    specialize beta_range_entry_eq i
  7. L106
    specialize beta_range_entry_eq x
  8. L107
    apply beta_range_entry_eq
  9. L108
    exact hrange
  10. L109
    exact hi
19Use earlier factsL110–110

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

  1. L110
    exact hentryi_witness_witness_witness_left
20Establish hyvalueL111–120

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

  1. L111
    have hyvalue : x3 = 1 + j
  2. L112
    specialize beta_range_entry_eq b
  3. L113
    specialize beta_range_entry_eq c
  4. L114
    specialize beta_range_entry_eq 1
  5. L115
    specialize beta_range_entry_eq h
  6. L116
    specialize beta_range_entry_eq j
  7. L117
    specialize beta_range_entry_eq x3
  8. L118
    apply beta_range_entry_eq
  9. L119
    exact hrange
  10. L120
    exact hj
21Use earlier factsL121–121

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

  1. L121
    exact hentryj_witness_witness_witness_left
22Establish honeiL122–129

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

  1. L122
    have honei : 1 + i = S i
  2. L123
    trans S (0 + i)
  3. L124
    specialize add_succ_left 0
  4. L125
    specialize add_succ_left i
  5. L126
    exact add_succ_left
  6. L127
    congr
  7. L128
    specialize zero_add i
  8. L129
    exact zero_add
23Establish honejL130–137

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

  1. L130
    have honej : 1 + j = S j
  2. L131
    trans S (0 + j)
  3. L132
    specialize add_succ_left 0
  4. L133
    specialize add_succ_left j
  5. L134
    exact add_succ_left
  6. L135
    congr
  7. L136
    specialize zero_add j
  8. L137
    exact zero_add
24Establish hxleL138–141

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

  1. L138
  2. L139
    rewrite hxvalue
  3. L140
    rewrite honei
  4. L141
    exact hi
25Establish hyleL142–145

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

  1. L142
  2. L143
    rewrite hyvalue
  3. L144
    rewrite honej
  4. L145
    exact hj
26Establish hsum_firstL146–151

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

  1. L146
    have hsum_first : Le(x + x3,h + x3)Definitions: Le(x + x3,h + x3)Original native command in the exact edition
  2. L147
    specialize add_le_add_right x
  3. L148
    specialize add_le_add_right h
  4. L149
    specialize add_le_add_right x3
  5. L150
    apply add_le_add_right
  6. L151
    exact hxle
27Establish hsum_secondL152–157

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

  1. L152
    have hsum_second : Le(h + x3,h + h)Definitions: Le(h + x3,h + h)Original native command in the exact edition
  2. L153
    specialize add_le_add_left x3
  3. L154
    specialize add_le_add_left h
  4. L155
    specialize add_le_add_left h
  5. L156
    apply add_le_add_left
  6. L157
    exact hyle
28Establish hsum_le_doubleL158–164

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

  1. L158
    have hsum_le_double : Le(x + x3,h + h)Definitions: Le(x + x3,h + h)Original native command in the exact edition
  2. L159
    specialize le_trans (x + x3)
  3. L160
    specialize le_trans (h + x3)
  4. L161
    specialize le_trans (h + h)
  5. L162
    apply le_trans
  6. L163
    exact hsum_first
  7. L164
    exact hsum_second
29Establish hdouble_belowL165–165

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

  1. L165
    have hdouble_below : Lt(h + h,p)Definitions: Lt(h + h,p)Original native command in the exact edition
30Construct an explicit witnessL166–166

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

  1. L166
    exists 0
31Calculate and transport equalitiesL167–168

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

  1. L167
    rewrite hpodd
  2. L168
    simp [mul_succ_left, mul_zero_left, zero_add, add_succ_left]
32Establish hsum_boundL169–175

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

  1. L169
    have hsum_bound : Lt(x + x3,p)Definitions: Lt(x + x3,p)Original native command in the exact edition
  2. L170
    specialize lt_of_le_of_lt (x + x3)
  3. L171
    specialize lt_of_le_of_lt (h + h)
  4. L172
    specialize lt_of_le_of_lt p
  5. L173
    apply lt_of_le_of_lt
  6. L174
    exact hsum_le_double
  7. L175
    exact hdouble_below
33Establish hsum_nonzeroL176–182

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

  1. L176
    have hsum_nonzero : ~(x + x3 = 0)
  2. L177
    intro hsumzero
  3. L178
    apply hxbounds_left
  4. L179
    specialize add_eq_zero_left x
  5. L180
    specialize add_eq_zero_left x3
  6. L181
    apply add_eq_zero_left
  7. L182
    exact hsumzero
34Establish hsumcommL183–186

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

  1. L183
    have hsumcomm : x3 + x = x + x3
  2. L184
    specialize add_comm x3
  3. L185
    specialize add_comm x
  4. L186
    exact add_comm
35Establish hreverse_sum_boundL187–189

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

  1. L187
    have hreverse_sum_bound : Lt(x3 + x,p)Definitions: Lt(x3 + x,p)Original native command in the exact edition
  2. L188
    rewrite hsumcomm
  3. L189
    exact hsum_bound
36Establish hreverse_sum_nonzeroL190–196

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

  1. L190
    have hreverse_sum_nonzero : ~(x3 + x = 0)
  2. L191
    intro hreversezero
  3. L192
    apply hsum_nonzero
  4. L193
    trans x3 + x
  5. L194
    symm
  6. L195
    exact hsumcomm
  7. L196
    exact hreversezero
37Establish hsourceeqL197–197

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

  1. L197
    have hsourceeq : x = x3
38Separate the logical casesL198–201

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

  1. L198
    cases hisigned
  2. L199
    cases hisigned_left
  3. L200
    cases hjsigned
  4. L201
    cases hjsigned_left
39Use earlier factsL202–211

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

  1. L202
    specialize gauss_same_sign_scaled_source_unique p
  2. L203
    specialize gauss_same_sign_scaled_source_unique h
  3. L204
    specialize gauss_same_sign_scaled_source_unique a
  4. L205
    specialize gauss_same_sign_scaled_source_unique x
  5. L206
    specialize gauss_same_sign_scaled_source_unique x3
  6. L207
    specialize gauss_same_sign_scaled_source_unique m
  7. L208
    apply gauss_same_sign_scaled_source_unique
  8. L209
    exact hp
  9. L210
    exact hnotdiv
  10. L211
    exact hxbounds_right
40Use earlier factsL212–212

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

  1. L212
    exact hybounds_right
41Separate the logical casesL213–214

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

  1. L213
    left
  2. L214
    split
42Use earlier factsL215–216

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

  1. L215
    exact hisigned_left_right
  2. L216
    exact hjsigned_left_right
43Separate the logical casesL217–218

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

  1. L217
    cases hjsigned_right
  2. L218
    exfalso
44Use earlier factsL219–228

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

  1. L219
    specialize gauss_mixed_sign_scaled_source_impossible p
  2. L220
    specialize gauss_mixed_sign_scaled_source_impossible h
  3. L221
    specialize gauss_mixed_sign_scaled_source_impossible a
  4. L222
    specialize gauss_mixed_sign_scaled_source_impossible x
  5. L223
    specialize gauss_mixed_sign_scaled_source_impossible x3
  6. L224
    specialize gauss_mixed_sign_scaled_source_impossible m
  7. L225
    apply gauss_mixed_sign_scaled_source_impossible
  8. L226
    exact hpodd
  9. L227
    exact hp
  10. L228
    exact hnotdiv
45Use earlier factsL229–232

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

  1. L229
    exact hsum_bound
  2. L230
    exact hsum_nonzero
  3. L231
    exact hisigned_left_right
  4. L232
    exact hjsigned_right_right
46Separate the logical casesL233–236

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

  1. L233
    cases hisigned_right
  2. L234
    cases hjsigned
  3. L235
    cases hjsigned_left
  4. L236
    exfalso
47Use earlier factsL237–246

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

  1. L237
    specialize gauss_mixed_sign_scaled_source_impossible p
  2. L238
    specialize gauss_mixed_sign_scaled_source_impossible h
  3. L239
    specialize gauss_mixed_sign_scaled_source_impossible a
  4. L240
    specialize gauss_mixed_sign_scaled_source_impossible x3
  5. L241
    specialize gauss_mixed_sign_scaled_source_impossible x
  6. L242
    specialize gauss_mixed_sign_scaled_source_impossible m
  7. L243
    apply gauss_mixed_sign_scaled_source_impossible
  8. L244
    exact hpodd
  9. L245
    exact hp
  10. L246
    exact hnotdiv
48Use earlier factsL247–250

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

  1. L247
    exact hreverse_sum_bound
  2. L248
    exact hreverse_sum_nonzero
  3. L249
    exact hjsigned_left_right
  4. L250
    exact hisigned_right_right
49Separate the logical casesL251–251

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

  1. L251
    cases hjsigned_right
50Use earlier factsL252–261

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

  1. L252
    specialize gauss_same_sign_scaled_source_unique p
  2. L253
    specialize gauss_same_sign_scaled_source_unique h
  3. L254
    specialize gauss_same_sign_scaled_source_unique a
  4. L255
    specialize gauss_same_sign_scaled_source_unique x
  5. L256
    specialize gauss_same_sign_scaled_source_unique x3
  6. L257
    specialize gauss_same_sign_scaled_source_unique m
  7. L258
    apply gauss_same_sign_scaled_source_unique
  8. L259
    exact hp
  9. L260
    exact hnotdiv
  10. L261
    exact hxbounds_right
51Use earlier factsL262–262

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

  1. L262
    exact hybounds_right
52Separate the logical casesL263–264

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

  1. L263
    right
  2. L264
    split
53Use earlier factsL265–274

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

  1. L265
    exact hisigned_right_right
  2. L266
    exact hjsigned_right_right
  3. L267
    specialize beta_range_injective b
  4. L268
    specialize beta_range_injective c
  5. L269
    specialize beta_range_injective 1
  6. L270
    specialize beta_range_injective h
  7. L271
    specialize beta_range_injective i
  8. L272
    specialize beta_range_injective j
  9. L273
    specialize beta_range_injective x
  10. L274
    specialize beta_range_injective x3
54Use earlier factsL275–281

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

  1. L275
    apply beta_range_injective
  2. L276
    exact hrange
  3. L277
    exact hi
  4. L278
    exact hj
  5. L279
    exact hentryi_witness_witness_witness_left
  6. L280
    exact hentryj_witness_witness_witness_left
  7. L281
    exact hsourceeq

Library-wide reading audit

Original defined command ledger · 281 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro hpodd
  11. 0011intro hp
  12. 0012intro hnotdiv
  13. 0013intro hrange
  14. 0014intro hprefix
  15. 0015intro i
  16. 0016intro j
  17. 0017intro m
  18. 0018intro hi
  19. 0019intro hj
  20. 0020intro hmi
  21. 0021intro hmj
  22. 0022have hentryi : ∃ gsp_value_injective_entry_i. ∃ gsp_magnitude_injective_entry_i. ∃ gsp_sign_injective_entry_i. BetaAt(b,c,i,gsp_value_injective_entry_i) ∧ (BetaAt(mb,mc,i,gsp_magnitude_injective_entry_i) ∧ (BetaAt(sb,sc,i,gsp_sign_injective_entry_i) ∧ (Lt(0,gsp_magnitude_injective_entry_i) ∧ (Le(gsp_magnitude_injective_entry_i,h) ∧ ((gsp_sign_injective_entry_i = 0 ∨ gsp_sign_injective_entry_i = 1) ∧ (gsp_sign_injective_entry_i = 0 ∧ ModEq(p,a · gsp_value_injective_entry_i,gsp_magnitude_injective_entry_i) ∨ gsp_sign_injective_entry_i = 1 ∧ ModEq(p,a · gsp_value_injective_entry_i,2 · h · gsp_magnitude_injective_entry_i)))))))
    Exact native replay linehave hentryi : exists gsp_value_injective_entry_i gsp_magnitude_injective_entry_i gsp_sign_injective_entry_i. (((exists ff_h_gsp_injective_entry_i_source. ff_h_gsp_injective_entry_i_source + S (gsp_value_injective_entry_i) = S ((S (i)) * c)) /\ exists ff_q_gsp_injective_entry_i_source. b = ff_q_gsp_injective_entry_i_source * S ((S (i)) * c) + (gsp_value_injective_entry_i))) /\ ((((exists ff_h_gsp_injective_entry_i_magnitude. ff_h_gsp_injective_entry_i_magnitude + S (gsp_magnitude_injective_entry_i) = S ((S (i)) * mc)) /\ exists ff_q_gsp_injective_entry_i_magnitude. mb = ff_q_gsp_injective_entry_i_magnitude * S ((S (i)) * mc) + (gsp_magnitude_injective_entry_i))) /\ ((((exists ff_h_gsp_injective_entry_i_sign. ff_h_gsp_injective_entry_i_sign + S (gsp_sign_injective_entry_i) = S ((S (i)) * sc)) /\ exists ff_q_gsp_injective_entry_i_sign. sb = ff_q_gsp_injective_entry_i_sign * S ((S (i)) * sc) + (gsp_sign_injective_entry_i))) /\ ((exists gsp_lt_gap_injective_entry_i_positive. gsp_lt_gap_injective_entry_i_positive + S 0 = gsp_magnitude_injective_entry_i) /\ ((exists gsp_le_gap_injective_entry_i_bounded. gsp_le_gap_injective_entry_i_bounded + gsp_magnitude_injective_entry_i = h) /\ ((gsp_sign_injective_entry_i = 0 \/ gsp_sign_injective_entry_i = 1) /\ (((gsp_sign_injective_entry_i = 0 /\ (exists gsp_mod_left_injective_entry_i_lower gsp_mod_right_injective_entry_i_lower. (a * gsp_value_injective_entry_i) + p * gsp_mod_left_injective_entry_i_lower = (gsp_magnitude_injective_entry_i) + p * gsp_mod_right_injective_entry_i_lower)) \/ (gsp_sign_injective_entry_i = 1 /\ (exists gsp_mod_left_injective_entry_i_reflected gsp_mod_right_injective_entry_i_reflected. (a * gsp_value_injective_entry_i) + p * gsp_mod_left_injective_entry_i_reflected = ((2 * h) * gsp_magnitude_injective_entry_i) + p * gsp_mod_right_injective_entry_i_reflected)))))))))
  23. 0023specialize hprefix i
  24. 0024apply hprefix
  25. 0025exact hi
  26. 0026cases hentryi
  27. 0027cases hentryi_witness
  28. 0028cases hentryi_witness_witness
  29. 0029cases hentryi_witness_witness_witness
  30. 0030cases hentryi_witness_witness_witness_right
  31. 0031cases hentryi_witness_witness_witness_right_right
  32. 0032cases hentryi_witness_witness_witness_right_right_right
  33. 0033cases hentryi_witness_witness_witness_right_right_right_right
  34. 0034cases hentryi_witness_witness_witness_right_right_right_right_right
  35. 0035have hentryj : ∃ gsp_value_injective_entry_j. ∃ gsp_magnitude_injective_entry_j. ∃ gsp_sign_injective_entry_j. BetaAt(b,c,j,gsp_value_injective_entry_j) ∧ (BetaAt(mb,mc,j,gsp_magnitude_injective_entry_j) ∧ (BetaAt(sb,sc,j,gsp_sign_injective_entry_j) ∧ (Lt(0,gsp_magnitude_injective_entry_j) ∧ (Le(gsp_magnitude_injective_entry_j,h) ∧ ((gsp_sign_injective_entry_j = 0 ∨ gsp_sign_injective_entry_j = 1) ∧ (gsp_sign_injective_entry_j = 0 ∧ ModEq(p,a · gsp_value_injective_entry_j,gsp_magnitude_injective_entry_j) ∨ gsp_sign_injective_entry_j = 1 ∧ ModEq(p,a · gsp_value_injective_entry_j,2 · h · gsp_magnitude_injective_entry_j)))))))
    Exact native replay linehave hentryj : exists gsp_value_injective_entry_j gsp_magnitude_injective_entry_j gsp_sign_injective_entry_j. (((exists ff_h_gsp_injective_entry_j_source. ff_h_gsp_injective_entry_j_source + S (gsp_value_injective_entry_j) = S ((S (j)) * c)) /\ exists ff_q_gsp_injective_entry_j_source. b = ff_q_gsp_injective_entry_j_source * S ((S (j)) * c) + (gsp_value_injective_entry_j))) /\ ((((exists ff_h_gsp_injective_entry_j_magnitude. ff_h_gsp_injective_entry_j_magnitude + S (gsp_magnitude_injective_entry_j) = S ((S (j)) * mc)) /\ exists ff_q_gsp_injective_entry_j_magnitude. mb = ff_q_gsp_injective_entry_j_magnitude * S ((S (j)) * mc) + (gsp_magnitude_injective_entry_j))) /\ ((((exists ff_h_gsp_injective_entry_j_sign. ff_h_gsp_injective_entry_j_sign + S (gsp_sign_injective_entry_j) = S ((S (j)) * sc)) /\ exists ff_q_gsp_injective_entry_j_sign. sb = ff_q_gsp_injective_entry_j_sign * S ((S (j)) * sc) + (gsp_sign_injective_entry_j))) /\ ((exists gsp_lt_gap_injective_entry_j_positive. gsp_lt_gap_injective_entry_j_positive + S 0 = gsp_magnitude_injective_entry_j) /\ ((exists gsp_le_gap_injective_entry_j_bounded. gsp_le_gap_injective_entry_j_bounded + gsp_magnitude_injective_entry_j = h) /\ ((gsp_sign_injective_entry_j = 0 \/ gsp_sign_injective_entry_j = 1) /\ (((gsp_sign_injective_entry_j = 0 /\ (exists gsp_mod_left_injective_entry_j_lower gsp_mod_right_injective_entry_j_lower. (a * gsp_value_injective_entry_j) + p * gsp_mod_left_injective_entry_j_lower = (gsp_magnitude_injective_entry_j) + p * gsp_mod_right_injective_entry_j_lower)) \/ (gsp_sign_injective_entry_j = 1 /\ (exists gsp_mod_left_injective_entry_j_reflected gsp_mod_right_injective_entry_j_reflected. (a * gsp_value_injective_entry_j) + p * gsp_mod_left_injective_entry_j_reflected = ((2 * h) * gsp_magnitude_injective_entry_j) + p * gsp_mod_right_injective_entry_j_reflected)))))))))
  36. 0036specialize hprefix j
  37. 0037apply hprefix
  38. 0038exact hj
  39. 0039cases hentryj
  40. 0040cases hentryj_witness
  41. 0041cases hentryj_witness_witness
  42. 0042cases hentryj_witness_witness_witness
  43. 0043cases hentryj_witness_witness_witness_right
  44. 0044cases hentryj_witness_witness_witness_right_right
  45. 0045cases hentryj_witness_witness_witness_right_right_right
  46. 0046cases hentryj_witness_witness_witness_right_right_right_right
  47. 0047cases hentryj_witness_witness_witness_right_right_right_right_right
  48. 0048have hmagi : m = x1
  49. 0049specialize beta_at_unique mb
  50. 0050specialize beta_at_unique mc
  51. 0051specialize beta_at_unique i
  52. 0052specialize beta_at_unique m
  53. 0053specialize beta_at_unique x1
  54. 0054apply beta_at_unique
  55. 0055exact hmi
  56. 0056exact hentryi_witness_witness_witness_right_left
  57. 0057have hmagj : m = x4
  58. 0058specialize beta_at_unique mb
  59. 0059specialize beta_at_unique mc
  60. 0060specialize beta_at_unique j
  61. 0061specialize beta_at_unique m
  62. 0062specialize beta_at_unique x4
  63. 0063apply beta_at_unique
  64. 0064exact hmj
  65. 0065exact hentryj_witness_witness_witness_right_left
  66. 0066rewrite <- hmagi at hentryi_witness_witness_witness_right_right_right_right_right_right
  67. 0067rewrite <- hmagi at hentryi_witness_witness_witness_right_right_right_right_right_right
  68. 0068rewrite <- hmagj at hentryj_witness_witness_witness_right_right_right_right_right_right
  69. 0069rewrite <- hmagj at hentryj_witness_witness_witness_right_right_right_right_right_right
  70. 0070have hisigned : x2 = 0 ∧ ModEq(p,a · x,m) ∨ x2 = 1 ∧ ModEq(p,a · x,2 · h · m)
    Exact native replay linehave hisigned : ((x2 = 0 /\ (exists gmp_mod_left_injective_i_lower gmp_mod_right_injective_i_lower. (a * x) + p * gmp_mod_left_injective_i_lower = (m) + p * gmp_mod_right_injective_i_lower)) \/ (x2 = 1 /\ (exists gmp_mod_left_injective_i_reflected gmp_mod_right_injective_i_reflected. (a * x) + p * gmp_mod_left_injective_i_reflected = ((2 * h) * m) + p * gmp_mod_right_injective_i_reflected)))
  71. 0071exact hentryi_witness_witness_witness_right_right_right_right_right_right
  72. 0072have hjsigned : x5 = 0 ∧ ModEq(p,a · x3,m) ∨ x5 = 1 ∧ ModEq(p,a · x3,2 · h · m)
    Exact native replay linehave hjsigned : ((x5 = 0 /\ (exists gmp_mod_left_injective_j_lower gmp_mod_right_injective_j_lower. (a * x3) + p * gmp_mod_left_injective_j_lower = (m) + p * gmp_mod_right_injective_j_lower)) \/ (x5 = 1 /\ (exists gmp_mod_left_injective_j_reflected gmp_mod_right_injective_j_reflected. (a * x3) + p * gmp_mod_left_injective_j_reflected = ((2 * h) * m) + p * gmp_mod_right_injective_j_reflected)))
  73. 0073exact hentryj_witness_witness_witness_right_right_right_right_right_right
  74. 0074have hxbounds : UnitResidue(p,x)
    Exact native replay linehave hxbounds : (~(x = 0) /\ (exists gsp_lt_gap_injective_x_bound. gsp_lt_gap_injective_x_bound + S x = p))
  75. 0075specialize beta_half_range_entry_bounds p
  76. 0076specialize beta_half_range_entry_bounds h
  77. 0077specialize beta_half_range_entry_bounds b
  78. 0078specialize beta_half_range_entry_bounds c
  79. 0079specialize beta_half_range_entry_bounds i
  80. 0080specialize beta_half_range_entry_bounds x
  81. 0081apply beta_half_range_entry_bounds
  82. 0082exact hpodd
  83. 0083exact hrange
  84. 0084exact hi
  85. 0085exact hentryi_witness_witness_witness_left
  86. 0086have hybounds : UnitResidue(p,x3)
    Exact native replay linehave hybounds : (~(x3 = 0) /\ (exists gsp_lt_gap_injective_y_bound. gsp_lt_gap_injective_y_bound + S x3 = p))
  87. 0087specialize beta_half_range_entry_bounds p
  88. 0088specialize beta_half_range_entry_bounds h
  89. 0089specialize beta_half_range_entry_bounds b
  90. 0090specialize beta_half_range_entry_bounds c
  91. 0091specialize beta_half_range_entry_bounds j
  92. 0092specialize beta_half_range_entry_bounds x3
  93. 0093apply beta_half_range_entry_bounds
  94. 0094exact hpodd
  95. 0095exact hrange
  96. 0096exact hj
  97. 0097exact hentryj_witness_witness_witness_left
  98. 0098cases hxbounds
  99. 0099cases hybounds
  100. 0100have hxvalue : x = 1 + i
  101. 0101specialize beta_range_entry_eq b
  102. 0102specialize beta_range_entry_eq c
  103. 0103specialize beta_range_entry_eq 1
  104. 0104specialize beta_range_entry_eq h
  105. 0105specialize beta_range_entry_eq i
  106. 0106specialize beta_range_entry_eq x
  107. 0107apply beta_range_entry_eq
  108. 0108exact hrange
  109. 0109exact hi
  110. 0110exact hentryi_witness_witness_witness_left
  111. 0111have hyvalue : x3 = 1 + j
  112. 0112specialize beta_range_entry_eq b
  113. 0113specialize beta_range_entry_eq c
  114. 0114specialize beta_range_entry_eq 1
  115. 0115specialize beta_range_entry_eq h
  116. 0116specialize beta_range_entry_eq j
  117. 0117specialize beta_range_entry_eq x3
  118. 0118apply beta_range_entry_eq
  119. 0119exact hrange
  120. 0120exact hj
  121. 0121exact hentryj_witness_witness_witness_left
  122. 0122have honei : 1 + i = S i
  123. 0123trans S (0 + i)
  124. 0124specialize add_succ_left 0
  125. 0125specialize add_succ_left i
  126. 0126exact add_succ_left
  127. 0127congr
  128. 0128specialize zero_add i
  129. 0129exact zero_add
  130. 0130have honej : 1 + j = S j
  131. 0131trans S (0 + j)
  132. 0132specialize add_succ_left 0
  133. 0133specialize add_succ_left j
  134. 0134exact add_succ_left
  135. 0135congr
  136. 0136specialize zero_add j
  137. 0137exact zero_add
  138. 0138have hxle : Le(x,h)
    Exact native replay linehave hxle : exists gsp_le_gap_injective_x_le_half. gsp_le_gap_injective_x_le_half + x = h
  139. 0139rewrite hxvalue
  140. 0140rewrite honei
  141. 0141exact hi
  142. 0142have hyle : Le(x3,h)
    Exact native replay linehave hyle : exists gsp_le_gap_injective_y_le_half. gsp_le_gap_injective_y_le_half + x3 = h
  143. 0143rewrite hyvalue
  144. 0144rewrite honej
  145. 0145exact hj
  146. 0146have hsum_first : Le(x + x3,h + x3)
    Exact native replay linehave hsum_first : exists gmp_sum_first_gap. gmp_sum_first_gap + (x + x3) = h + x3
  147. 0147specialize add_le_add_right x
  148. 0148specialize add_le_add_right h
  149. 0149specialize add_le_add_right x3
  150. 0150apply add_le_add_right
  151. 0151exact hxle
  152. 0152have hsum_second : Le(h + x3,h + h)
    Exact native replay linehave hsum_second : exists gmp_sum_second_gap. gmp_sum_second_gap + (h + x3) = h + h
  153. 0153specialize add_le_add_left x3
  154. 0154specialize add_le_add_left h
  155. 0155specialize add_le_add_left h
  156. 0156apply add_le_add_left
  157. 0157exact hyle
  158. 0158have hsum_le_double : Le(x + x3,h + h)
    Exact native replay linehave hsum_le_double : exists gmp_sum_double_gap. gmp_sum_double_gap + (x + x3) = h + h
  159. 0159specialize le_trans (x + x3)
  160. 0160specialize le_trans (h + x3)
  161. 0161specialize le_trans (h + h)
  162. 0162apply le_trans
  163. 0163exact hsum_first
  164. 0164exact hsum_second
  165. 0165have hdouble_below : Lt(h + h,p)
    Exact native replay linehave hdouble_below : exists gmp_double_below_gap. gmp_double_below_gap + S (h + h) = p
  166. 0166exists 0
  167. 0167rewrite hpodd
  168. 0168simp [mul_succ_left, mul_zero_left, zero_add, add_succ_left]
  169. 0169have hsum_bound : Lt(x + x3,p)
    Exact native replay linehave hsum_bound : exists gsp_lt_gap_injective_sum_bound. gsp_lt_gap_injective_sum_bound + S (x + x3) = p
  170. 0170specialize lt_of_le_of_lt (x + x3)
  171. 0171specialize lt_of_le_of_lt (h + h)
  172. 0172specialize lt_of_le_of_lt p
  173. 0173apply lt_of_le_of_lt
  174. 0174exact hsum_le_double
  175. 0175exact hdouble_below
  176. 0176have hsum_nonzero : ~(x + x3 = 0)
  177. 0177intro hsumzero
  178. 0178apply hxbounds_left
  179. 0179specialize add_eq_zero_left x
  180. 0180specialize add_eq_zero_left x3
  181. 0181apply add_eq_zero_left
  182. 0182exact hsumzero
  183. 0183have hsumcomm : x3 + x = x + x3
  184. 0184specialize add_comm x3
  185. 0185specialize add_comm x
  186. 0186exact add_comm
  187. 0187have hreverse_sum_bound : Lt(x3 + x,p)
    Exact native replay linehave hreverse_sum_bound : exists gsp_lt_gap_injective_reverse_sum_bound. gsp_lt_gap_injective_reverse_sum_bound + S (x3 + x) = p
  188. 0188rewrite hsumcomm
  189. 0189exact hsum_bound
  190. 0190have hreverse_sum_nonzero : ~(x3 + x = 0)
  191. 0191intro hreversezero
  192. 0192apply hsum_nonzero
  193. 0193trans x3 + x
  194. 0194symm
  195. 0195exact hsumcomm
  196. 0196exact hreversezero
  197. 0197have hsourceeq : x = x3
  198. 0198cases hisigned
  199. 0199cases hisigned_left
  200. 0200cases hjsigned
  201. 0201cases hjsigned_left
  202. 0202specialize gauss_same_sign_scaled_source_unique p
  203. 0203specialize gauss_same_sign_scaled_source_unique h
  204. 0204specialize gauss_same_sign_scaled_source_unique a
  205. 0205specialize gauss_same_sign_scaled_source_unique x
  206. 0206specialize gauss_same_sign_scaled_source_unique x3
  207. 0207specialize gauss_same_sign_scaled_source_unique m
  208. 0208apply gauss_same_sign_scaled_source_unique
  209. 0209exact hp
  210. 0210exact hnotdiv
  211. 0211exact hxbounds_right
  212. 0212exact hybounds_right
  213. 0213left
  214. 0214split
  215. 0215exact hisigned_left_right
  216. 0216exact hjsigned_left_right
  217. 0217cases hjsigned_right
  218. 0218exfalso
  219. 0219specialize gauss_mixed_sign_scaled_source_impossible p
  220. 0220specialize gauss_mixed_sign_scaled_source_impossible h
  221. 0221specialize gauss_mixed_sign_scaled_source_impossible a
  222. 0222specialize gauss_mixed_sign_scaled_source_impossible x
  223. 0223specialize gauss_mixed_sign_scaled_source_impossible x3
  224. 0224specialize gauss_mixed_sign_scaled_source_impossible m
  225. 0225apply gauss_mixed_sign_scaled_source_impossible
  226. 0226exact hpodd
  227. 0227exact hp
  228. 0228exact hnotdiv
  229. 0229exact hsum_bound
  230. 0230exact hsum_nonzero
  231. 0231exact hisigned_left_right
  232. 0232exact hjsigned_right_right
  233. 0233cases hisigned_right
  234. 0234cases hjsigned
  235. 0235cases hjsigned_left
  236. 0236exfalso
  237. 0237specialize gauss_mixed_sign_scaled_source_impossible p
  238. 0238specialize gauss_mixed_sign_scaled_source_impossible h
  239. 0239specialize gauss_mixed_sign_scaled_source_impossible a
  240. 0240specialize gauss_mixed_sign_scaled_source_impossible x3
  241. 0241specialize gauss_mixed_sign_scaled_source_impossible x
  242. 0242specialize gauss_mixed_sign_scaled_source_impossible m
  243. 0243apply gauss_mixed_sign_scaled_source_impossible
  244. 0244exact hpodd
  245. 0245exact hp
  246. 0246exact hnotdiv
  247. 0247exact hreverse_sum_bound
  248. 0248exact hreverse_sum_nonzero
  249. 0249exact hjsigned_left_right
  250. 0250exact hisigned_right_right
  251. 0251cases hjsigned_right
  252. 0252specialize gauss_same_sign_scaled_source_unique p
  253. 0253specialize gauss_same_sign_scaled_source_unique h
  254. 0254specialize gauss_same_sign_scaled_source_unique a
  255. 0255specialize gauss_same_sign_scaled_source_unique x
  256. 0256specialize gauss_same_sign_scaled_source_unique x3
  257. 0257specialize gauss_same_sign_scaled_source_unique m
  258. 0258apply gauss_same_sign_scaled_source_unique
  259. 0259exact hp
  260. 0260exact hnotdiv
  261. 0261exact hxbounds_right
  262. 0262exact hybounds_right
  263. 0263right
  264. 0264split
  265. 0265exact hisigned_right_right
  266. 0266exact hjsigned_right_right
  267. 0267specialize beta_range_injective b
  268. 0268specialize beta_range_injective c
  269. 0269specialize beta_range_injective 1
  270. 0270specialize beta_range_injective h
  271. 0271specialize beta_range_injective i
  272. 0272specialize beta_range_injective j
  273. 0273specialize beta_range_injective x
  274. 0274specialize beta_range_injective x3
  275. 0275apply beta_range_injective
  276. 0276exact hrange
  277. 0277exact hi
  278. 0278exact hj
  279. 0279exact hentryi_witness_witness_witness_left
  280. 0280exact hentryj_witness_witness_witness_left
  281. 0281exact hsourceeq