proposition: Lemma l9_41_2 : forall A B C P Q R, TSP A B C P R -> OSP A B C P Q -> TSP A B C Q R.
proof: Proof. intros A B C P Q R HPR [S [[HP [_ [X []]]] [HQ [HS [Y []]]]]]. assert (P <> X /\ S <> X /\ Q <> Y /\ S <> Y) by (repeat split; intro; subst; auto); spliter. destruct (col_dec P Q S) as [|HNCol]. { assert (X = Y) by (assert_diffs; apply (col2_cop2__eq A B C Q S); ColR). subst Y. apply l9_39 with X P; trivial. apply l6_2 with S; auto. } destruct (inner_pasch P Q S X Y) as [Z []]; trivial. assert (X <> Z) by (intro; subst; apply HNCol; ColR). apply l9_39 with X Z; [|assumption|apply bet_out; auto]. assert (Y <> Z) by (intro; subst; apply HNCol; ColR). apply l9_39 with Y P; [assumption..|apply l6_6, bet_out; auto]. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar