proposition: Lemma plg_par_2 : forall A B C D, A <> B -> B <> C -> Parallelogram A B C D -> Par A D B C.
proof: Proof. intros. assert (HPar := plg_par A B C D H H0 H1); spliter; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates