proposition: Lemma sac__coplanar : forall A B C D, Saccheri A B C D -> Coplanar A B C D.
proof: Proof. intros A B C D [_ [_ [_ HOS]]]. apply os__coplanar in HOS; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar