proposition: Lemma plg_sym : forall A B C D, Parallelogram A B C D -> Parallelogram C D A B.
proof: Proof. intros. induction H. left. apply plgs_sym. assumption. right. apply plgf_sym. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel