Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq