proposition: Lemma NCol_perm : forall A B C, ~ Col 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.
proof: Proof. intros. repeat split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch04_cong_bet