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