proposition: Lemma col_pos_or_neg : forall O E X, O <> E -> O <> X -> Col O E X -> Ps O E X \/ Ng O E X.
proof: Proof. intros O E X HOE HOX HCol. unfold Ps, Ng, Out. unfold Col in HCol; intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod