proposition: Lemma plgs_permut : forall A B C D, Parallelogram_strict A B C D -> Parallelogram_strict B C D A.
proof: Proof. intros A B C D HPara. destruct HPara as [HTS [HCong HPar]]. destruct (ts_cong_par_cong_par A B C D) as [HCong' HPar']; Col. destruct (par_cong_mid A B C D) as [M HM]; Col. elim HM; clear HM; intro HM; destruct HM as [HMid1 HMid2]. { assert (HAM : A <> M) by (intro; treat_equalities; unfold TS in HTS; spliter; Col). assert (HCM : C <> M) by (intro; treat_equalities; unfold TS in HTS; spliter; Col). assert (HBD : B <> D) by (intro; subst D; apply (not_two_sides_id B A C HTS)). destruct HTS as [HAC [HABC HTS]]. repeat split; [intro; apply HABC; ColR..| |Par|Cong]. exists M; split; [Col|Between]. } { exfalso; apply (l9_9 A C B D HTS). unfold TS in HTS; spliter. apply l12_6; apply par_not_col_strict with B; Col. apply par_right_comm; apply l12_17 with M; Midpoint. intro; subst; Col. } Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates