proposition: Lemma eq_o_eqo : forall A B P A1 B1 P1, eq_o A B P A1 B1 P1 -> eqo A B P A1 B1 P1.
proof: Proof. intros. unfold eq_o in H. spliter. unfold eqo. repeat split; auto. intros. eapply H1. apply H2. apply per_proj. apply perp_not_eq_2 in H2. auto. assumption. apply l8_5. Col. apply H4. apply per_proj. apply perp_not_eq_2 in H4. auto. assumption. apply l8_5. Col. apply H6. assumption. apply H8. apply H9. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec