proposition: Lemma plgs__pars : forall A B C D, Parallelogram_strict A B C D -> Par_strict A B C D.
proof: Proof. intros. assert (HH := H). unfold Parallelogram_strict in HH; spliter. destruct H1; auto; spliter. apply parallelogram_strict_not_col_2 in H. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel