proposition: Lemma parallelogram_strict_not_col : forall A B C D, Parallelogram_strict A B C D -> ~ Col A B C.
proof: Proof. unfold Parallelogram_strict. intros. spliter. apply two_sides_not_col in H. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel