proposition: Lemma mid2_sac__perp_lower : forall A B C D M N, Saccheri A B C D -> Midpoint M B C -> Midpoint N A D -> Perp A D M N.
proof: Proof. intros A B C D M N HSac HM HN. assert(Hdiff := sac_distincts A B C D HSac). assert(HConga := sac__conga A B C D HSac). unfold Saccheri in HSac. spliter. assert_diffs. assert(HSAS := l11_49 M B A M C D). destruct HSAS; Cong. apply (l11_10 C B A B C D); [CongA|Out..]. apply (l8_16_2 _ _ _ A); Col. { apply one_side_not_col124 with B. apply l9_17 with C; Between. } exists D. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma