proposition: Lemma plgs_pars_1: forall A B C D : Tpoint, Parallelogram_strict A B C D -> Par_strict A B C D.
proof: Proof. intros. assert (HPar := plgs_par_strict A B C D H); spliter; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates