Ceva's Theorem. - Mathias Schack Rabing (Arch. Formal Proofs, 2023)

Formalization of Countable Multisets. - Mathias Schack Rabing; Dmitriy Traytel (Arch. Formal Proofs, 2026)

Formalization of Weighted Sets. - Mathias Schack Rabing; Dmitriy Traytel (Arch. Formal Proofs, 2026)