proposition: Lemma par_cong_plg_2 : forall A B C D, Par A B C D -> Cong A B C D -> Parallelogram A B C D \/ Parallelogram A B D C.
proof: Proof. intros. assert (HElim : Plg A B C D \/ Plg A B D C) by (apply par_cong_plg; assumption). elim HElim; intro. left; apply plg_to_parallelogram; assumption. right; apply plg_to_parallelogram; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates