proposition: Lemma plg_uniqueness : forall A B C D D', Parallelogram A B C D -> Parallelogram A B C D' -> D = D'.
proof: Proof. intros. apply plg_mid in H. apply plg_mid in H0. ex_and H M. ex_and H0 M'. assert(M = M'). eapply l7_17. apply H. assumption. subst M'. eapply symmetric_point_uniqueness. apply H1. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates