proposition: Lemma out_preserves_eqo : forall A B P B' P', ~Col A B P -> Out A B B' -> Out A P P' -> eqo A B P A B' P'.
proof: Proof. intros. induction (eq_dec_points P P'). subst P'. apply out_preserves_eqo1. assumption. assumption. unfold eqo. repeat split. assumption. intro. apply H. assert(Col A B B'). apply out_col. assumption. assert(Col A P P'). apply out_col. assumption. assert(Col A P B'). apply (col_transitivity_1 _ P'). intro. subst P'. unfold Out in H1. spliter. auto. Col. Col. eapply (col_transitivity_1 _ B'). intro. subst B'. unfold Out in H0. spliter. auto. Col. Col. intros. assert(B = B2). apply (l6_11_uniqueness A A B2 B'). assumption. assumption. apply l6_6. assumption. apply cong_reflexivity. subst B2. apply l7_3 in H9. subst M. assert(A <> C). apply perp_not_eq_2 in H3. auto. assert(A <> C1). apply perp_not_eq_2 in H5. auto. assert(Perp A B C1 A). eapply perp_col. intro. subst B. apply H. Col. apply H5. apply out_col. apply l6_6. assumption. assert(Col A C C1). eapply perp2__col. apply perp_sym. apply perp_comm. apply H3. apply perp_comm. Perp. induction(eq_dec_points P C). subst P. assert(P'=C1). apply l8_9 in H6. induction H6. assumption. contradiction. assert(HH:= H1). unfold Out in H1. spliter. apply out_col in HH. ColR. subst P'. left. unfold Out in H1. spliter. induction H17. eapply between_exchange3. apply between_symmetry. apply H17. apply midpoint_bet. assumption. eapply outer_transitivity_between2. apply between_symmetry. apply H17. apply midpoint_bet. assumption. assumption. assert(~Col P C A). apply per_not_col. assumption. auto. assumption. assert(C <> C1). intro. subst C1. assert(Col P P' C). eapply per2__col. apply H4. auto. assumption. apply H2. apply (l6_21 A P C P); Col. assert(HH:=diff_col_ex3 A C C1 H15). ex_and HH D. left. unfold Out in H1. spliter. induction H24. assert(Bet A C C1). apply (per_preserves_bet D A A P P' A C C1); Col. apply l8_2. apply l8_5. apply per_col with A; Col. apply per_col with A; ColR. ColR. eapply between_exchange3. apply between_symmetry. apply H25. apply midpoint_bet. assumption. assert(Bet A C1 C). apply (per_preserves_bet D A A P' P A C1 C); Col. apply l8_2. apply l8_5. apply per_col with A; ColR. ColR. apply per_col with A; ColR. apply between_symmetry. apply outer_transitivity_between with C1; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec