Disclaimer: I am not even an expert user of these two kinds of software.
I understand that the trivial difference between proof assistants and CAS is that in proof assistants, the goal is to show that the given proposition reduces to a tautology. Whereas CAS are used to perform various transformations on mathematical expressions to find results that are useful.
When we are doing mathematics on paper, the techniques used while deriving something are not all that different from the techniques used while proving something. In each case, we start with an expression, and apply one (previously established) rule after another, until we reach our goal. As far as I know, the rules that are applied in derivations are exactly the same as the rules applied while proving something. Looking at it in another way, the human skills honed on derivations are perfectly applicable while performing proofs.
When comparing computer systems, the list of computer algebra systems has no titles in common with the list of proof assistants. From my lay perspective, to name a specific example, I think we can use CAS to derive the roots of a generalized quadratic equation, but only when we have the formula, can we use a proof assistant to verify it.
So, given the vast amount of mathematical knowledge encoded in the libraries of both CAS and proof assistants, why can't we use a CAS to perform proofs, and why can't we use proof assistants for deriving anything beyond tautologies?