α : Type ?u.198618
β : Type ?u.198621
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < c → c < b → a ≠ ⊤
⊢ (b - c) * a = b * a - c * a
α : Type ?u.198618
β : Type ?u.198621
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < c → c < b → a ≠ ⊤
⊢ a * (b - c) = a * b - a * c
simp only [mul_comm a]
no goals
α : Type ?u.198618
β : Type ?u.198621
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < c → c < b → a ≠ ⊤
⊢ (b - c) * a = b * a - c * a
exact sub_mul h