proposition: Lemma out_one_side : forall A B X Y, (~ Col A B X \/ ~ Col A B Y) -> Out A X Y -> OS A B X Y.
proof: Proof. intros. induction H. assert(~ Col X A B). intro. apply H. apply col_permutation_1. assumption. assert(HH:=one_side_reflexivity A B X H1). apply (out_out_one_side _ _ _ _ _ HH H0). assert(~ Col Y A B). intro. apply H. apply col_permutation_1. assumption. assert(HH:=one_side_reflexivity A B Y H1). apply one_side_symmetry. apply (out_out_one_side _ _ _ _ _ HH). apply l6_6. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar