proposition: Lemma plgs_not_col : forall A B C D, Parallelogram_strict A B C D -> ~ Col A B C /\ ~ Col B C D /\ ~ Col C D A /\ ~ Col A B D.
proof: Proof. intros. repeat split. apply parallelogram_strict_not_col in H; assumption. apply parallelogram_strict_not_col_2 in H; assumption. apply parallelogram_strict_not_col_3 in H; assumption. apply parallelogram_strict_not_col_4 in H; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel