proposition: Lemma out_preserves_eq_o : forall A B B' P, ~Col A B P -> Out A B B' -> eq_o A B P A B' P.
proof: Proof. intros. assert(A <> B /\ A <> B'). unfold Out in H0. spliter. split; auto. spliter. unfold eq_o. repeat split. assumption. apply out_col in H0. intro. apply H. ColR. intros. 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. assumption. apply H5. apply out_col in H0. Col. assert(Col A C C1). eapply perp2__col. apply perp_sym. apply perp_comm. apply H3. apply perp_comm. Perp. assert(proj B A C1 A). unfold proj. split; auto. left. repeat split. intro. apply perp_not_col in H14. apply H14. Col. apply perp_comm. Perp. Col. assert(proj P A C C1). eapply proj_col_proj. apply H6. assumption. Col. assert(C= C1). eapply proj_uniqueness. apply H4. assumption. subst C1. clear H17 H6 H14. left. apply midpoint_bet. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec