CoqHammer has some limited support for MathComp and proofs by reflection out of the box, see the website. However, for arithmetic goals, it’s possible to escape from the MathComp world via mczify. The idea is to first canonize a MathComp arithmetic goal via the zify tactic, and then apply the hammer tactic on the resulting goal (assuming lia with mczify doesn’t do the job directly).
2 Likes