proposition: Lemma plgs_cong_2 : forall A B C D, Parallelogram_strict A B C D -> Cong A D B C.
proof: Proof. intros. apply plgs_cong in H. spliter. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates