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