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