Theorem: Usa2023P2.lemma_1 (Compfiles/Usa2023P2.lean)

State before:
a b c : ℝ+
⊢ (a + b) / c = a / c + b / c
Tactic:
rw [division_def, add_mul, ←division_def, ←division_def]
State after:
no goals