proposition: Lemma plg_conga1 : forall A B C D, A <> B -> A <> C -> Plg A B C D -> CongA B A C D C A.
proof: Proof. intros. apply cong3_conga; auto. assert(HH := plg_to_parallelogram A B C D H1). apply plg_cong in HH. spliter. repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates