Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
In this talk, we introduce the Ssreflect tactic language, as used in the Mathematical Components library. We will focus on the tactics used to make formalization work lighter and easier to maintain.