Reconstructing Plane Sets from Projections.
Relations on lines as primitive notions for Euclidean geometry
Routh’s, Menelaus’ and Generalized Ceva’s Theorems
The goal of this article is to formalize Ceva’s theorem that is in the [8] on the web. Alongside with it formalizations of Routh’s, Menelaus’ and generalized form of Ceva’s theorem itself are provided.