proposition: Lemma ncol_conga_ncol : forall A B C D E F, ~ Col A B C -> CongA A B C D E F -> ~ Col D E F.
proof: Proof. intros. intro. apply H. eapply col_conga_col. apply H1. apply conga_sym. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2