proposition: Lemma rah__triangle : postulate_of_right_saccheri_quadrilaterals -> triangle_postulate.
proof: Proof. intros rah A B C D E F. apply (t22_14__bet rah). Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri