What are there in the rocq system besides the kernel?

A large library of common definitions and axioms.

Powerful tactics for constructing complex proofs semi-automatically.

A special-purpose programming language for defining new proof-automation tactics for specific situations.