As Neel answered, you can (theoretically) prove anything in a proof assistant that you can prove on paper, including idealized run-times or resource usage for a program modeled using a deep embedding (see Shallow versus Deep Embeddings).
How closely your idealized representation of the run-time corresponds to the actual run-time (in milliseconds, say) of a program on a real piece of hardware depends on the fidelity of your model of operational semantics and running time, which is a rather complex question. Certainly proving $O(n)$-type bounds is feasible. Neel mentions CerCo, which allows exploring run-time in terms of assembly instructions corresponding to the source. However, the run-time of a sequence of assembly instructions is also extremely difficult to predict, given cache and pipelining considerations (among others). There is a whole body of work on this, this is one but it's a bit dated. I know of no formalization of such systems in theorem provers though.
If you have a deep embedding, then functions written in your proof language can not directly prove anything about the evaluation behavior, since the un-evaluated programs are indistinguishable from the evaluated ones: if you could prove "fact 6 reduces in $k$ steps" then you could prove the same thing about the numeral 720, which is in reduced form.
However, you could imagine a variant of the factorial function, which returns not only the result of the computation, but also a natural number denoting, say, the number of recursive calls made by the computation. This would look something like this (in OCaml notation):
let fact n = if n == 0 then (1, 0) else
let (k, r) = fact (n-1) in
(n * k, r+1)
It's a bit boring, but now fact 6 is (720, 6) where the second number is the number of recursions, which can be seen as a kind of run-time bound. If the definition required several recursive calls, you would add the recursion depths together to get the final result.
Elaborating on these ideas naturally leads to the kind of work by Danielsson and various others, as mentioned in the comments by gallais. It's perhaps unsurprising that these considerations lead to a "resource monad" in which to describe these recursive definitions.
Finally, it's of academic interest to note that any definition in a total language like Coq or Agda must have an intrinsic run-time upper bound: any program of size $n$ must fully evaluate in time $O(f(n))$ where $f$ is some computable function to be described by some clever proof theorist. Sadly, that bound is so enormous so as to be effectively useless; for example it is easy to describe the Ackermann function in both systems, so $f$ must grow faster than any given tower of exponentials (much, much, much faster).
