proposition: Lemma ts_cong_par_cong_par : forall A B A' B', TS A A' B B' -> Cong A B A' B' -> Par A B A' B' -> Cong A B' A' B /\ Par A B' A' B.
proof: Proof. intros A B A' B' HTS HCong HPar. assert(HAB : A <> B) by (intro; treat_equalities; unfold TS in *; spliter; Col). destruct (par_cong_mid A B A' B') as [M HM]; Col. elim HM; clear HM; intro HM; destruct HM as [HMid1 HMid2]. { assert(HAB' : A <> B') by (intro; treat_equalities; unfold TS in HTS; spliter; Col). split; try apply l7_13 with M; try apply l12_17 with M; Midpoint. } { assert(HAA' : A <> A') 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 A' B' B); Par; apply l12_17 with M; Midpoint. } Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates