proposition: Lemma parallelogram_strict_not_col_4 : forall A B C D, Parallelogram_strict A B C D -> ~ Col A B D.
proof: Proof. intros. apply plgs_one_side in H. destruct H. apply one_side_not_col124 in H. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel