proposition: Lemma plg_conga : forall A B C D, A <> B /\ A <> C /\ B <> C -> Parallelogram A B C D -> CongA A B C C D A /\ CongA B C D D A B.
proof: Proof. intros. assert(Cong A B C D /\ Cong A D B C). apply plg_cong. assumption. spliter. assert(HH:= plg_mid A B C D H0). ex_and HH M. split. apply cong3_conga; auto. repeat split; Cong. apply cong3_conga; auto. intro. subst D. apply H. eapply symmetric_point_uniqueness; apply l7_2. apply H5. assumption. repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates