proposition: Lemma one_side_transitivity : forall P Q A B C, OS P Q A B -> OS P Q B C -> OS P Q A C.
proof: Proof. intros. unfold OS in *. ex_and H X. ex_and H0 Y. exists X. split. assumption. apply l9_2. eapply l9_8_2. apply l9_2. apply H2. eapply l9_8_1. apply l9_2. apply H0. apply l9_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar