proposition: Lemma plgf_comm2 : forall A B C D, Parallelogram_flat A B C D -> Parallelogram_flat B A D C.
proof: Proof. intros. unfold Parallelogram_flat in *. spliter. repeat split; Col. Cong. Cong. induction H3. right; assumption. left; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates