proposition: Lemma osp_bet__osp : forall A B C P Q R, OSP A B C P R -> Bet P Q R -> OSP A B C P Q.
proof: Proof. intros A B C P Q R [S [HPS [HR [_ [Y []]]]]] HBet. destruct (col_dec P R S) as [|HNCol]. { exists S. split; [assumption|]. apply l9_39 with Y P; trivial. destruct HPS as [HP [HS [X []]]]. assert (P <> X /\ S <> X /\ R <> Y) by (repeat split; intro; subst; auto); spliter. assert (X = Y) by (assert_diffs; apply (col2_cop2__eq A B C R S); ColR). subst Y. apply out_bet_out_1 with R; [|assumption]. apply l6_2 with S; auto. } destruct HPS as [HP [HS [X []]]]. assert (HOS : OS X Y P Q). { apply l9_17 with R; [|assumption]. assert (P <> X /\ S <> X /\ R <> Y /\ S <> Y) by (repeat split; intro; subst; auto); spliter. assert (~ Col S X Y) by (intro; apply HNCol; ColR). exists S; repeat split; trivial; try (intro; apply HNCol; ColR). exists X; split; Col. exists Y; split; Col. } destruct HOS as [S' [[HNCol1 [HNCol2 [X' []]]] [HNCol3 [_ [Y' []]]]]]. assert (Coplanar A B C X') by (assert_diffs; apply col_cop2__cop with X Y; Col). assert (Coplanar A B C Y') by (assert_diffs; apply col_cop2__cop with X Y; Col). assert (HS' : ~ Coplanar A B C S'). intro; apply HP, col_cop2__cop with X' S'; Col; intro; subst; Col. exists S'; repeat split; trivial. exists X'; split; assumption. intro; apply HS', col_cop2__cop with Q Y'; Col; intro; subst; Col. exists Y'; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar