This paper presents the design, the implementation and experiments of the integration of syntactic, conditional possibly associative-commutative term rewriting into proof assistants based on constructive type theory. Our approach is called external since it consists in performing term rewriting in a specific and efficient environment and to check the computations later in a proof assistant. Two typical systems are considered in this work, \elan, based on the rewriting calculus, as the term rewriting based environment, and \coq, based on the calculus of inductive constructions as the proof assistant. We first formalize the proof terms for deduction by rewriting and strategies in \elan\ using the rewriting calculus with explicit substitutions. We then show how these proof terms can soundly be translated into \coq-syntax where they can be directly type checked. For the method to be applicable for proving equalities modulo an equational theory that contains associativity and commutativity, we provide an effective method to prove equalities modulo associativity and commutativity in \coq\ using \elan. These results have been integrated into an {\elan} based rewriting tactic in \coq.