proposition: Lemma three_hypotheses_aux : forall A B C D M N A' B' C' D' M' N', Saccheri A B C D -> Saccheri A' B' C' D' -> Midpoint M B C -> Midpoint M' B' C' -> Midpoint N A D -> Midpoint N' A' D' -> Le M N M' N' -> (Per A B C <-> Per A' B' C') /\ (Acute A B C <-> Acute A' B' C').
proof: Proof. intros A B C D M N A' B' C' D' M' N' HSac HSac' HM HM' HN HN' Hle. assert(HLam1 := mid2_sac__lam6534 A B C D M N HSac HM HN). assert(HLam1' := mid2_sac__lam6534 A' B' C' D' M' N' HSac' HM' HN'). assert(Hdiff := sac_distincts A B C D HSac). assert(Hdiff' := sac_distincts A' B' C' D' HSac'). spliter. assert(HNCol1 : ~ Col C D A) by (apply (par_strict_not_col_3 _ B), sac__pars1234, HSac). assert_diffs. rename H into HA'B'. assert(HH := segment_construction_3 N D N' D'). destruct HH as [H []]; auto. assert(Col A D H) by ColR. assert(G0 := l10_15 A D H C). destruct G0 as [G0 []]; Col. assert_diffs. assert(HG := segment_construction_3 H G0 C' D'). destruct HG as [G []]; auto. assert_diffs. assert(OS N D C G). { apply invert_one_side. apply (col_one_side _ A); Col. apply invert_one_side. apply (one_side_transitivity _ _ _ G0); auto. apply(l9_19 _ _ _ _ H); Col. split; auto. apply one_side_not_col124 with C; assumption. } assert(Perp A D H G) by (apply (perp_col1 _ _ _ G0); Perp; Col). clear dependent G0. assert(HNCol2 : ~ Col M N H). { unfold Lambert in HLam1. spliter. apply per_not_col; auto. apply (per_col _ _ D); auto; ColR. } assert (HCop : Coplanar A D M G). { apply coplanar_trans_1 with C; Col. apply coplanar_perm_12, col_cop__cop with B; Col; Cop. apply coplanar_perm_5, col_cop__cop with N; Col; Cop. } assert (HNCol3 : ~ Col M N G). { unfold Lambert in HLam1. spliter. apply (one_side_not_col123 _ _ _ H). apply l12_6. apply (par_not_col_strict _ _ _ _ H); Col. apply (l12_9 _ _ _ _ A D); Cop; [|Perp]. apply perp_right_comm; apply (perp_col1 _ _ _ N); Col; Perp. } assert_diffs. assert(A <> H) by (intro; subst H; assert(Habs := l6_4_1 D A N); destruct Habs; Between). assert(Col H A N) by ColR. assert(HL := l8_18_existence M N G). destruct HL as [L []]; auto. assert(HNCol4 : ~ Col M A D). apply sac__pars1423 in HSac; apply (par_not_col B C); Par; Col. assert(HLam2 : Lambert N L G H). { assert(Per N H G). { apply (l8_3 A); Col. apply (perp_per_1); auto. apply perp_comm. apply (perp_col _ D); Col. } assert(~ Col N H G) by (apply per_not_col; auto). assert(Per A N M). { apply perp_per_1, perp_left_comm, (perp_col _ D); Col. apply (mid2_sac__perp_lower _ B C); auto. } assert(Per L N H) by (apply (l8_3 M); Col; apply (per_col _ _ A); Col; Perp). assert(N <> L). { intro. subst L. assert(Col G H N); Col. apply cop_per2__col with M; [|Perp..|apply (l8_3 A); Col]. apply coplanar_pseudo_trans with A D M; Cop; Col. } repeat split; auto. intro; subst; apply HNCol3; assumption. apply perp_per_1, perp_left_comm, (perp_col _ M); Col; Perp. apply coplanar_pseudo_trans with A D M; [Col|Cop| |Cop..]. exists N; left; split; Col. } assert(Par_strict N D M C) by (apply lam__pars1423, HLam1). assert(Bet N M L). { destruct (cong2_lam2__cong_conga N' M' C' D' N L G H); Cong. apply l6_13_1; [|apply (l5_6 M N M' N'); Cong]. apply (col_one_side_out _ D); Col. apply (one_side_transitivity _ _ _ G). apply (one_side_transitivity _ _ _ C); auto; apply l12_6; auto. apply (col_one_side _ H); [ColR..|]. apply one_side_symmetry, l12_6, lam__pars1423, HLam2. } assert(HNCol5 : ~ Col N M C) by (unfold Lambert in HLam1; spliter; apply per_not_col; auto). assert(HNCol6 : ~ Col N D M) by (apply (par_strict_not_col_1 _ _ _ C); auto). assert (Coplanar M C D A). apply pars__coplanar, par_strict_col_par_strict with N; Col; Par. assert(HK : exists K, Col K M C /\ Bet G K H). { elim(eq_dec_points L M). { intro. subst L. exists G. split; Between. apply col_permutation_5. unfold Lambert in *. spliter. apply cop_per2__col with N; Perp. apply coplanar_pseudo_trans with A D M; Col; Cop. } intro. assert(HNCol7 : ~ Col L M C) by (intro; apply HNCol5; ColR). assert(Hts : TS M C G H); [|unfold TS in Hts; spliter; auto]. apply (l9_8_2 _ _ L). - apply l9_2. apply (l9_8_2 _ _ N). repeat split; Col; exists M; Col. apply l12_6, (par_strict_col_par_strict _ _ _ D); Par; ColR. - apply l12_6, (par_not_col_strict _ _ _ _ L); Col. unfold Lambert in *. spliter. apply (l12_9 _ _ _ _ M N); Perp; [Cop..|]. apply coplanar_pseudo_trans with A D M; Col; Cop. } destruct HK as [K []]. assert(HNCol7 : ~ Col H M C) by (apply (par_not_col N D); Col). assert(K <> H) by (intro; subst K; auto). assert(Par_strict N M C D) by (apply lam__pars1234, HLam1). assert(HNCol8 : ~ Col N C D) by (apply (par_strict_not_col_2 M); Par). assert(Par_strict M N H K). { apply par_strict_col_par_strict with G; Col. apply par_strict_comm, par_strict_symmetry, par_strict_col_par_strict with L; Col. apply par_strict_symmetry, lam__pars1234, HLam2. } assert(HNCol9 : ~ Col N H K) by (apply (par_strict_not_col_2 M); auto). assert(HMout : Out M C K). { apply (col_one_side_out _ N); Col. apply (one_side_transitivity _ _ _ D). apply l12_6; Par. apply (one_side_transitivity _ _ _ H). apply invert_one_side; apply out_one_side; Col. apply l12_6; auto. } assert_diffs. assert(HLam3 : Lambert N M K H). { unfold Lambert in *. spliter. repeat split; auto. apply (l8_3 L); Col. apply (per_col _ _ G); Col. apply (per_col _ _ C); Col. apply coplanar_perm_7, pars__coplanar; assumption. } assert(HConga := sac__conga A B C D HSac). assert(CongA A' B' C' H G L). { apply (conga_trans _ _ _ M' C' D'). apply (l11_10 A' B' C' B' C' D'); [apply sac__conga, HSac'|Out..]. apply conga_right_comm, (cong2_lam2__cong_conga N' _ _ _ N); Cong. } assert((Bet M C K -> Bet N D H) /\ (Bet M K C -> Bet N H D)). { destruct(eq_dec_points D H) as [|HDH]. subst; split; intro; Between. assert(HPar : Par C D K H). { unfold Lambert in *. spliter. apply (l12_9 _ _ _ _ N D); [|Cop..|Perp|]. apply os__coplanar, par_strict_all_one_side with M; Par; Col. apply perp_comm, (perp_col _ G); Col; apply (perp_col1 _ _ _ A); Perp; Col. } assert (Par_strict C D K H). { destruct HPar; auto. exfalso. unfold Lambert in *. spliter. apply HDH. apply (l8_18_uniqueness C D N); Col. Perp. ColR. apply (perp_col _ H); auto; [|ColR]. apply perp_left_comm, (perp_col _ G); Perp; ColR. } split; intro; apply between_symmetry, not_out_bet; Col; intro. - assert(Out C K M); [|assert(Habs := l6_4_1 K M C); destruct Habs; Between]. apply (col_one_side_out _ D); Col. apply (one_side_transitivity _ _ _ N); [|Side]. apply (one_side_transitivity _ _ _ H); [Side|apply invert_one_side; apply out_one_side; Col]. - assert(Out K C M); [|assert(Habs := l6_4_1 C M K); destruct Habs; Between]. apply (col_one_side_out _ H); Col. apply (one_side_transitivity _ _ _ N); [|Side]. apply (one_side_transitivity _ _ _ D); [Side|apply invert_one_side; apply out_one_side; Col]. } spliter; split; split; intro. - apply (l11_17 L G H); CongA. apply (t22_9__per N _ K M); try (apply lam_perm); Between. apply l8_2. assert(Per D C M). { apply (l11_17 A B C); auto. apply (l11_10 A B C D C B); [CongA|Out..]. } destruct HMout as [_ [_ [HMCK|HMKC]]]. apply (t22_9__per N _ C D); auto. apply (t22_9__per N _ _ _ C D); auto. - apply (l11_17 D C M). { assert(Per H K M). apply l8_2, (t22_9__per N _ _ _ G L); try (apply lam_perm); Between. apply (l11_17 A' B' C'); CongA. destruct HMout as [_ [_ [HMCK|HMKC]]]. apply (t22_9__per N _ _ _ K H); auto. apply (t22_9__per N _ K H); auto. } apply (l11_10 D C B A B C); [CongA|Out..]. - apply (acute_conga__acute L G H); CongA. apply (t22_9__acute N _ K M); try (apply lam_perm); Between. apply acute_sym. assert(Acute D C M). { apply (acute_conga__acute A B C); auto. apply (l11_10 A B C D C B); [CongA|Out..]. } destruct HMout as [_ [_ [HMCK|HMKC]]]. apply (t22_9__acute N _ C D); auto. apply (t22_9__acute N _ _ _ C D); auto. - apply (acute_conga__acute D C M). { assert(Acute H K M). apply acute_sym. apply (t22_9__acute N _ _ _ G L); try (apply lam_perm); Between. apply (acute_conga__acute A' B' C'); CongA. destruct HMout as [_ [_ [HMCK|HMKC]]]. apply (t22_9__acute N _ _ _ K H); auto. apply (t22_9__acute N _ K H); auto. } apply (l11_10 D C B A B C); [CongA|Out..]. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma