proposition: Lemma plgf_not_point : forall A B, Parallelogram_flat A A B B -> A <> B.
proof: Proof. intros. unfold Parallelogram_flat in H. spliter. intro. subst B. induction H3; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel