proposition: Lemma right_saccheris : forall A B C D, Saccheri A B C D -> Per A B C.
proof: Proof. apply postulates_in_euclidean_context; simpl; repeat (try (left; reflexivity); right). Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec