proposition: Lemma mid2_sac__perp_upper : forall A B C D M N, Saccheri A B C D -> Midpoint M B C -> Midpoint N A D -> Perp B C 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 N A B N D C). destruct HSAS; Cong. { apply l11_16; auto. apply (l8_3 D); Perp; Col. apply (l8_3 A); Col. } apply perp_right_comm. apply (l8_16_2 _ _ _ B); Col. { intro. absurd (Col A D N); [|Col]. apply one_side_not_col124 with B. apply l9_17 with C; trivial. apply midpoint_bet, l7_20_bis; Col. } exists C. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma