Modern proof assistants make it possible to verify proofs and programs, but also to perform computations, and sometimes to find proofs automatically. By using various tools and techniques to solve well-defined classes of goals, infer appropriate data and setup nice notations, or perform high-level reasoning steps, I will show how to obtain robust and elegant proof scripts in two application domains: relation algebra and monoidal categories.