Lemmas about canonically ordered semifields.

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