proposition: Lemma defect_ncol_out__rah : forall A B C D E F, ~ Col A B C -> Defect A B C D E F -> Out E D F -> hypothesis_of_right_saccheri_quadrilaterals.
proof: Proof. intros A B C D E F HNCol HDef HOut. destruct HDef as [G [H [I [HTri HSuppa]]]]. apply (t22_14__rah A B C G H I); trivial. apply (out_suppa__bet D E F); [|apply suppa_sym]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri