proposition: Lemma plgf_permut : forall A B C D, Parallelogram_flat A B C D -> Parallelogram_flat B C D A.
proof: Proof. intros. unfold Parallelogram_flat in *. spliter. induction(eq_dec_points A B). subst B. apply cong_symmetry in H1. apply cong_identity in H1. subst D. repeat split; Col. apply cong_trivial_identity. induction H3; left; assumption. assert(C <> D). intro. subst D. apply cong_identity in H1. contradiction. repeat split. ColR. Col. Cong. Cong. induction H3. right. auto. left; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel