Lemmas about canonically ordered semifields.

theorem tsub_div {α : Type u_1} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α] (a : α) (b : α) (c : α) : (a - b) / c = a / c - b / c