proposition: Lemma ex_points_lg_not_col : forall l P, Q_Cong l -> ~ Q_Cong_Null l -> exists A, exists B, l A B /\ ~Col A B P.
proof: Proof. intros. assert(HH:=another_point P). ex_elim HH A. assert(HH:= not_col_exists P A H1). ex_elim HH Q. exists A. assert(A <> Q). intro. subst Q. apply H2. Col. lg_instance2 l A Q B. exists B. split. auto. intro. apply H2. assert(A <> B). intro. subst B. unfold Out in H5. tauto; apply out_col in H5. apply out_col in H5. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1