proposition: Lemma par_2_plg : forall A B C D, ~ Col A B C -> Par A B C D -> Par A D B C -> Parallelogram A B C D.
proof: Proof. intros. assert (H2 := parallel_2_plg A B C D H H0 H1). apply Parallelogram_strict_Parallelogram; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates