## Proofs by reflection and uses of type classes

When performing proofs about mathematical formulas, it is often enough to perform small computation on the shape of the statement rather than complex reasoning on the meaning of all its components. These computations can be programmed directly in Coq, as long as we define a language to describe the shapes…