proposition: Lemma col_not_plgs : forall A B C D, Col A B C -> ~Parallelogram_strict A B C D.
proof: Proof. intros. intro. unfold Parallelogram_strict in H0. spliter. unfold TS in H0. repeat split. spliter. apply H0. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel