proposition: Lemma ncol_suma__ncol : forall A B C D E F, ~ Col A B C -> SumA A B C B C A D E F -> ~ Col D E F.
proof: Proof. intros A B C D E F HNCol HSuma HCol. apply HNCol, col_suma__col with D E F; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles