The [assert] tactic in Coq is used to interrupt a proof and prove a useful related theorem. That can help structure proofs, and help with problematic [rewrite] instances.
Textbook: https://clarksmr.github.io/sf-lectures/textbook/lf/toc.html
Supporting materials: https://github.com/clarksmr/sf-lectures/tree/main/notes/lf
