fact: Definition posidonius_postulate := exists A1 A2 B1 B2, ~ Col A1 A2 B1 /\ B1 <> B2 /\ Coplanar A1 A2 B1 B2 /\ forall A3 A4 B3 B4, Col A1 A2 A3 -> Col B1 B2 B3 -> Perp A1 A2 A3 B3 -> Col A1 A2 A4 -> Col B1 B2 B4 -> Perp A1 A2 A4 B4 -> Cong A3 B3 A4 B4.
imports: GeoCoq.Tarski_dev.Definitions