proposition: Lemma orthonormal_family_axiom_implies_not_two_sides_one_side : orthonormal_family_axiom -> (forall A B C X Y, ~ Coplanar A B C X -> ~ Coplanar A B C Y -> ~ TSP A B C X Y -> OSP A B C X Y).
proof: Proof. intros up A B C X Y HX HY HNTS. destruct (l11_62_existence_bis A B C X HX) as [P HOrth]. assert (HOrth1 := HOrth). apply orth_at_chara in HOrth1. destruct HOrth1 as [HNCol [HPX [HP HOrth1]]]. destruct (l8_21_3 A B C P Y HP HY) as [X' [T [HOrth' [HT HBet]]]]. apply (col_cop_orth__orth_at _ _ _ _ _ P) in HOrth'; Col. assert (~ Coplanar A B C X') by (apply orth_at__ncop with P, HOrth'). assert (HTS : TSP A B C Y X'). repeat split; trivial; exists T; split; assumption. exists X'; split; [|assumption]. repeat split; trivial. exists P; split; [assumption|]. apply not_out_bet. apply col_permutation_1, (orthonormal_family_axiom_implies_orth_at2__col up A B C); assumption. intro; apply HNTS. apply l9_41_2 with X'. apply l9_38, HTS. apply osp_symmetry, cop_out__osp with P; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv