proposition: Lemma cop2_os__osp : forall A B C D E X Y, ~ Coplanar A B C X -> Coplanar A B C D -> Coplanar A B C E -> OS D E X Y -> OSP A B C X Y.
proof: Proof. intros A B C D E X Y HX HD HE [Z [HXZ HYZ]]. assert (HTS : TSP A B C X Z) by (apply cop2_ts__tsp with D E; assumption). exists Z; split; [assumption|]. destruct HTS as [_ []]. apply l9_2 in HYZ. apply l9_38, cop2_ts__tsp with D E; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar