proposition: Lemma eqo_eq_o : forall A B P A1 B1 P1, eqo A B P A1 B1 P1 -> eq_o A B P A1 B1 P1.
proof: Proof. intros. unfold eqo in H. spliter. unfold eq_o. repeat split ; auto. intros. assert(HH:= H1 C C1 B2 M B' C' K). apply HH; auto. unfold proj in *. spliter. induction H13; induction H12. spliter. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. Perp. spliter. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. Perp. spliter. subst P. apply l8_2. apply l8_5. spliter. subst P. apply l8_2. apply l8_5. unfold proj in *. spliter. induction H13; induction H12. spliter. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. Perp. spliter. subst P1. apply l8_2. apply l8_5. spliter. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. Perp. spliter. subst P1. apply l8_2. apply l8_5. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec