no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod (_ : 0 < p) x₁ x₂ ≤ toIocMod (_ : 0 < p) x₁ x₃
rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_right]