proposition: Lemma plgs_half_plgs : forall A B C D P Q, Parallelogram_strict A B C D -> Midpoint P A B -> Midpoint Q C D -> Parallelogram_strict A P Q D /\ Parallelogram_strict B P Q C.
proof: Proof. intros. split. eapply plgs_half_plgs_aux. apply H. assumption. assumption. apply plgs_comm2 in H. eapply plgs_half_plgs_aux. apply H. Midpoint. Midpoint. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates