Thomas Braibant, Damien Pous: Tactics for Reasoning Modulo AC in Coq. CPP 2011: 167-182