proposition: Lemma per__ex_saccheri : forall A B D, Per B A D -> A <> B -> A <> D -> exists C, Saccheri A B C D.
proof: Proof. intros A B D HPer HAB HBD. assert (HNCol : ~ Col B A D) by (apply per_not_col; auto). destruct (l10_15 A D D B) as [C0 []]; Col. assert(~ Col A D C0) by (apply (one_side_not_col123 _ _ _ B); Side). assert_diffs. destruct (segment_construction_3 D C0 A B) as [C []]; auto. exists C. repeat split; Cong. apply (per_col _ _ C0); Col; Perp. apply invert_one_side; apply (out_out_one_side _ _ _ C0); Side. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma