abel
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ I.a₁ + I.a₂ + I.b₁ + I.b₂ = I.a₁ + I.b₁ + (I.a₂ + I.b₂)
no goals