proposition: Lemma parallelogram_to_plg : forall A B C D, Parallelogram A B C D -> Plg A B C D.
proof: Proof. intros A B C D HPara. destruct (plg_mid A B C D) as [M HM]; Col. split; try (exists M; Col). elim HPara; clear HPara; intro HPara; try (apply plgs_diff in HPara; spliter; Col); unfold Parallelogram_flat in HPara; spliter; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates