proposition: Lemma plg_mid : forall A B C D, Parallelogram A B C D -> exists M, Midpoint M A C /\ Midpoint M B D.
proof: Proof. intros A B C D HPara. elim HPara; clear HPara; intro HPara. { apply plgs_mid; Col. } { apply plgf_mid; Col. } Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates