proposition: Lemma plg_existence : forall A B C, A <> B -> exists D, Parallelogram A B C D.
proof: Proof. intros. assert(HH:=midpoint_existence A C). ex_and HH M. prolong B M D B M. assert(Midpoint M B D). unfold Midpoint. split; Cong. exists D. induction (eq_dec_points A C). subst C. apply l7_3 in H0. subst M. right. apply bet_col in H1. repeat split; Col; Cong. right. intro. subst D. apply l7_3 in H3. contradiction. apply (mid_plg _ _ _ _ M). left. assumption. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel