proposition: Lemma cop_out__osp : forall A B C X Y P, ~ Coplanar A B C X -> Coplanar A B C P -> Out P X Y -> OSP A B C X Y.
proof: Proof. intros A B C X Y P HX HP HOut. assert (~ Coplanar A B C Y). assert_diffs; intro; apply HX, col_cop2__cop with P Y; Col. destruct (segment_construction X P P X) as [X' []]. assert (~ Coplanar A B C X'). assert_diffs; intro; apply HX, col_cop2__cop with P X'; Col. exists X'; repeat split; trivial; exists P; split; trivial. apply bet_out__bet with X; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar