proposition: Lemma not_neg_pos : forall O E A, E <> O -> Col O E A -> ~Ng O E A -> Ps O E A \/ A = O.
proof: Proof. intros. induction(eq_dec_points A O). { right; auto. } { left. unfold Out. apply l6_4_2. split; Col. intro. apply H1. unfold Ng. repeat split; auto. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order