proposition: Lemma os_cong_par_cong_par : forall A B A' B', OS A A' B B' -> Cong A B A' B' -> Par A B A' B' -> Cong A A' B B' /\ Par A A' B B'.
proof: Proof. intros. induction H1. assert(A <> B /\ A <> A'). unfold OS in H. ex_and H C. unfold TS in H. spliter. split. intro. subst B. apply H. Col. intro. subst A'. Col. spliter. assert(HH:= (par_strict_cong_mid1 A B A' B' H1 H0 )). induction HH. spliter. apply l9_9 in H4. contradiction. spliter. ex_and H5 M. assert(HH:= mid_par_cong A B B' A' M H2 H3). assert(Cong A B B' A' /\ Cong A A' B' B /\ Par A B B' A' /\ Par A A' B' B). apply HH. assumption. assumption. spliter. split. Cong. Par. spliter. unfold OS in H. ex_and H C. unfold TS in H5. spliter. apply False_ind. apply H5. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates