proposition: Lemma rah_defect__out : hypothesis_of_right_saccheri_quadrilaterals -> forall A B C D E F, Defect A B C D E F -> Out E D F.
proof: Proof. intros rah A B C D E F HDef. destruct HDef as [G [H [I [HTri HSuppa]]]]. apply (bet_suppa__out G H I); trivial. apply (t22_14__bet rah A B C), HTri. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri