proposition: Lemma NCol_cases : forall A B C, ~ Col A B C \/ ~ Col A C B \/ ~ Col B A C \/ ~ Col B C A \/ ~ Col C A B \/ ~ Col C B A -> ~ Col A B C.
proof: Proof. intros. decompose [or] H; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch04_cong_bet