fact: Definition Par A B C D := exists U V u v X, neq A B /\ neq C D /\ Col A B U /\ Col A B V /\ neq U V /\ Col C D u /\ Col C D v /\ neq u v /\ ~ Meet A B C D /\ BetS U X v /\ BetS u X V.
imports: GeoCoq.Axioms.euclidean_axioms