proposition: Lemma out_preserves_eqo1 : forall A B P B', ~Col A B P -> Out A B B' -> eqo A B P A B' P.
proof: Proof. intros. unfold eqo. repeat split. assumption. assert(HH:=H0). unfold Out in H0. spliter. apply out_col in HH. intro. apply H. ColR. 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 H7. subst M. assert(Perp A B C1 A). eapply perp_col. intro. subst B. apply H. Col. apply H3. apply out_col in H5. assumption. assert(A <> C). apply perp_not_eq_2 in H1. auto. assert(A <> C1). apply perp_not_eq_2 in H3. auto. assert(Col A C C1). eapply perp2__col. apply perp_sym. apply perp_right_comm. apply H1. apply perp_sym. Perp. induction (eq_dec_points P C). subst P. apply l8_9 in H4. induction H4. subst C1. unfold Midpoint in H9. spliter. left. assumption. subst C1. apply perp_not_eq_2 in H3. tauto. Col. assert(P <> C1). intro. subst P. apply H14. apply l8_9 in H2. induction H2. assumption. subst C. tauto. Col. assert(C1=C). apply per_id with P A; Col. subst C1. unfold Midpoint in H9. spliter. left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec