proposition: Lemma one_side_symmetry : forall P Q A B, OS P Q A B -> OS P Q B A.
proof: Proof. unfold OS. intros. ex_and H C. exists C. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar