proposition: Lemma par_preserves_conga_os : forall A B C D P , Par A B C D -> Bet A D P -> D <> P -> OS A D B C -> CongA B A P C D P.
proof: Proof. intros. assert(HH:= H2). unfold OS in HH. ex_and HH T. unfold TS in *. spliter. prolong C D C' C D. assert(C' <> D). intro. subst C'. apply cong_symmetry in H10. apply cong_identity in H10. subst D. apply H4. Col. assert(CongA B A D C' D A). eapply l12_21_a. apply (l9_8_2 _ _ C). unfold TS. repeat split; auto. intro. apply H4. apply bet_col in H9. ColR. exists D. split. Col. assumption. apply one_side_symmetry. assumption. apply par_symmetry. eapply (par_col_par_2 _ C). auto. apply bet_col in H9. Col. apply par_symmetry. Par. assert(A <> B). intro. subst B. apply H3. Col. assert(CongA B A D B A P). assert(A <> D). intro. subst D. Col. apply out2__conga. apply out_trivial. auto. repeat split; auto. intro. subst P. apply between_identity in H0. contradiction. apply conga_right_comm. assert(CongA C D P C' D A). eapply l11_14; auto. intro. subst D. apply H4. Col. Between. intro. subst D. Col. eapply conga_trans. apply conga_sym. apply H14. eapply conga_trans. apply H12. apply conga_sym. apply conga_left_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates