proposition: Lemma sac__pars1423 : forall A B C D, Saccheri A B C D -> Par_strict A D B C.
proof: Proof. intros A B C D HSac. assert(HM := midpoint_existence B C). destruct HM as [M HM]. assert(HN := midpoint_existence A D). destruct HN as [N HN]. assert(HPerp1 := mid2_sac__perp_lower A B C D M N HSac HM HN). assert(HPerp2 := mid2_sac__perp_upper A B C D M N HSac HM HN). unfold Saccheri in HSac. spliter. apply (col_cop_perp2__pars M N); Col; Cop. apply one_side_not_col124 with B. apply l9_17 with C; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma