proof doesnt work

Stream: general

[Leni Greco]

why doesnt this work?

import LeanCourse.Common
import Mathlib.Data.Real.Basic

namespace C03S01

section
variable (f g : ℝ → ℝ)

example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x :=by
  intro a b c
  dsimp
  apply mul_le_mul
  linarith
  apply mf
  exact c
  linarith
  exact nnc

end

[Ruben Van de Velde]

For me, it fails at

unknown package 'LeanCourse'

[Ruben Van de Velde]

Not sure if that answers your question

[Kevin Buzzard]

Calling a proof c is not a great idea. Calling it c when you already have a variable called c is even worse. But I think that rather than answer your question (in case it's homework) I'd prefer to ask you one -- what is your regular maths proof of the result?