proposition: Lemma parallelogram_equiv_plg : forall A B C D, Parallelogram A B C D <-> Plg A B C D.
proof: Proof. intros. split. apply parallelogram_to_plg. apply plg_to_parallelogram. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates