proposition: Lemma plgs_sym : forall A B C D, Parallelogram_strict A B C D -> Parallelogram_strict C D A B.
proof: Proof. unfold Parallelogram_strict. intros; spliter. repeat (split; finish). Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel