proposition: Lemma parallel_2_plg : forall A B C D, ~ Col A B C -> Par A B C D -> Par A D B C -> Parallelogram_strict A B C D.
proof: Proof. intros. assert (Cong A B C D /\ Cong B C D A /\ TS B D A C /\ TS A C B D) by (apply l12_19;Par). unfold Parallelogram_strict; intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates