∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} [hp' : Fact (0 < p)] {x₁ x₂ x₃ x₄ : α ⧸ AddSubgroup.zmultiples p},
  btw x₁ x₂ x₃ ∧ ¬btw x₃ x₂ x₁ → btw x₂ x₄ x₃ ∧ ¬btw x₃ x₄ x₂ → btw x₁ x₄ x₃ ∧ ¬btw x₃ x₄ x₁