proposition: Lemma plgs_cong : forall A B C D, Parallelogram_strict A B C D -> Cong A B C D /\ Cong A D B C.
proof: Proof. intros A B C D HPara. destruct HPara as [HTS [HCong HPar]]; split; Col. destruct (ts_cong_par_cong_par A B C D) as [HCong' HPar']; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates