proposition: Lemma ex_saccheri : exists A B C D, Saccheri A B C D.
proof: Proof. destruct lower_dim_ex as [A [D [E]]]. assert(HNCol : ~ Col A D E) by (unfold Col; assumption). destruct (l10_15 A D A E) as [B []]; Col. assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ E); Side). assert_diffs. destruct (per__ex_saccheri A B D) as [C HSac]; Perp. exists A; exists B; exists C; exists D; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma