Lemmas about canonically ordered semifields. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem tsub_div {α : Type u_1} [canonically_linear_ordered_semifield α] [has_sub α] [has_ordered_sub α] (a b c : α) :

(a - b) / c = a / c - b / c