/-- Multiplication distributes over addition on the left argument. -/
theorem addMulDistribLeft (a b c : Nat) : (a + b) * c = a * c + b * c := by
{{PROOF}}