α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
suffices toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b by
  rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIocDiv hp (-(a + p)) b = -toIcoDiv hp a (-b)
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
rw [← neg_eq_iff_eq_neg, eq_comm]
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIocDiv hp (-(a + p)) b = -toIcoDiv hp a (-b)
apply toIocDiv_eq_of_sub_zsmul_mem_Ioc
case h.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -b - toIcoDiv hp a (-b) • p < a + p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
obtain ⟨hc, ho⟩ := sub_toIcoDiv_zsmul_mem_Ico hp a (-b)
case h.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho✝ : -b - toIcoDiv hp a (-b) • p < a + p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
case h.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -b - toIcoDiv hp a (-b) • p < a + p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
rw [← neg_lt_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at ho
case h.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
hc✝ : a ≤ -b - toIcoDiv hp a (-b) • p
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho✝ : -b - toIcoDiv hp a (-b) • p < a + p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
case h.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho✝ : -b - toIcoDiv hp a (-b) • p < a + p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
rw [← neg_le_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at hc
case h.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
hc✝ : a ≤ -b - toIcoDiv hp a (-b) • p
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho✝ : -b - toIcoDiv hp a (-b) • p < a + p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ -a = -(a + p) + p
case h.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
hc✝ : a ≤ -b - toIcoDiv hp a (-b) • p
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho✝ : -b - toIcoDiv hp a (-b) • p < a + p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
refine' ⟨ho, hc.trans_eq _⟩
no goals
case h.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
hc✝ : a ≤ -b - toIcoDiv hp a (-b) • p
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho✝ : -b - toIcoDiv hp a (-b) • p < a + p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ -a = -(a + p) + p
rw [neg_add, neg_add_cancel_right]
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this