proposition: Lemma plgs_irreflexive : forall A B, ~ Parallelogram_strict A B A B.
proof: Proof. intros. intro. unfold Parallelogram_strict in H. spliter. unfold TS in H. spliter. apply H2. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel