proposition: Lemma plgs_mid : forall A B C D, Parallelogram_strict A B C D -> exists M, Midpoint M A C /\ Midpoint M B D.
proof: Proof. intros A B C D HPara. destruct HPara as [HTS [HCong HPar]]. destruct (par_cong_mid A B C D) as [M HM]; Col. elim HM; clear HM; intro HM; destruct HM as [HMid1 HMid2]; try (exists M; Col). assert(HAB : A <> B) by (intro; treat_equalities; unfold TS in HTS; spliter; Col). assert(HAC : A <> C) by (intro; treat_equalities; unfold TS in HTS; spliter; Col). assert (HFalse := HTS); apply l9_9 in HFalse; exfalso; apply HFalse; clear HFalse. unfold TS in HTS; spliter; apply l12_6; apply par_not_col_strict with B; Col. assert (Par A C D B); Par; apply l12_17 with M; Midpoint. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates