proposition: Lemma plg_to_parallelogram : forall A B C D, Plg A B C D -> Parallelogram A B C D.
proof: Proof. intros. unfold Plg in H. spliter. ex_and H0 M. eapply (mid_plg _ _ _ _ M). induction H;[left|right]; assumption. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel