proposition: Lemma one_side_chara : forall P Q A B, OS P Q A B -> (forall X, Col X P Q -> ~ Bet A X B).
proof: Proof. intros. assert(~ Col A P Q). destruct H as [R [[] _]]; assumption. assert(~ Col B P Q). destruct H as [R [_ []]]; assumption. apply l9_9_bis in H. intro. apply H. unfold TS. repeat split. assumption. assumption. exists X. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar