proposition: Lemma plg_col_plgf : forall A B C D, Col A B C -> Parallelogram A B C D -> Parallelogram_flat A B C D.
proof: Proof. intros. induction H0. eapply (col_not_plgs A B C D) in H. contradiction. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel