Library GeoCoq.Tarski_dev.Annexes.saccheri
This development is inspired by The Foundations of Geometry and the Non-Euclidean Plane, by George E Martin, chapters 21 and 22
Section Saccheri.
Context `{T2D:Tarski_2D}.
Lemma sac_perm : ∀ A B C D, Saccheri A B C D → Saccheri D C B A.
Proof.
intros.
unfold Saccheri in ×.
spliter.
repeat split; Perp; Cong; Side.
Qed.
Lemma sac_distincts : ∀ A B C D,
Saccheri A B C D →
A ≠ B ∧ B ≠ C ∧ C ≠ D ∧ A ≠ D ∧ A ≠ C ∧ B ≠ D.
Proof.
intros A B C D HSac.
unfold Saccheri in HSac.
spliter.
assert(¬ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
assert(¬ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side).
assert_diffs.
repeat split; auto.
intro; treat_equalities.
assert(A=D) by (apply (l8_7 B A D); Perp); auto.
Qed.
Lemma lam_perm : ∀ A B C D, Lambert A B C D → Lambert A D C B.
Proof.
intros.
unfold Lambert in ×.
spliter.
repeat split; Perp.
Qed.
The two following lemmas come from Theorem 21.10
Lemma sac__cong : ∀ A B C D, Saccheri A B C D → Cong A C B D.
Proof.
intros A B C D HSac.
assert(Hdiff := sac_distincts A B C D HSac).
unfold Saccheri in HSac.
spliter.
assert(HSAS := l11_49 B A D C D A).
destruct HSAS; Cong.
apply l11_16; Perp.
Qed.
Lemma sac__conga : ∀ A B C D, Saccheri A B C D → CongA A B C B C D.
Proof.
intros A B C D HSac.
assert(Hdiff := sac_distincts A B C D HSac).
assert(HCong := sac__cong A B C D HSac).
unfold Saccheri in HSac.
spliter.
assert(HSSS := l11_51 A B C D C B).
destruct HSSS as [_ []]; Cong; CongA.
Qed.
Lemma lam__os : ∀ A B C D, Lambert A B C D → OS A B C D.
Proof.
intros A B C D HLam.
unfold Lambert in HLam; spliter.
assert(HNCol : ¬ Col A B C) by (apply per_not_col; trivial).
apply l12_6, par_not_col_strict with C; Col.
apply l12_9 with A D; Perp.
Qed.
Lemma per2_os__ncol123 : ∀ A B C D, Per B A D → Per A D C → OS A D B C →
¬ Col A B C.
Proof.
intros A B C D HPer1 HPer2 Hos.
assert(¬ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
assert(¬ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side).
assert_diffs.
apply (par_strict_not_col_1 _ _ _ D).
apply (par_not_col_strict _ _ _ _ D); Col.
apply (l12_9 _ _ _ _ A D); Perp.
Qed.
Lemma per2_os__ncol234 : ∀ A B C D,
Per B A D → Per A D C →
OS A D B C →
¬ Col B C D.
Proof.
intros A B C D HPer1 HPer2 Hos.
assert(¬ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
assert(¬ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side).
assert_diffs.
apply (par_strict_not_col_2 A).
apply (par_not_col_strict _ _ _ _ D); Col.
apply (l12_9 _ _ _ _ A D); Perp.
Qed.
Lemma sac__ncol123 : ∀ A B C D, Saccheri A B C D → ¬ Col A B C.
Proof.
intros A B C D HSac.
unfold Saccheri in HSac.
spliter.
apply (per2_os__ncol123 _ _ _ D); assumption.
Qed.
Lemma sac__ncol124 : ∀ A B C D, Saccheri A B C D → ¬ Col A B D.
Proof.
intros A B C D HSac.
unfold Saccheri in HSac.
spliter.
apply not_col_permutation_1.
apply (one_side_not_col123 _ _ _ C); Side.
Qed.
Lemma sac__ncol134 : ∀ A B C D, Saccheri A B C D → ¬ Col A C D.
Proof.
intros A B C D HSac.
unfold Saccheri in HSac.
spliter.
apply not_col_permutation_1.
apply (one_side_not_col123 _ _ _ B); Side.
Qed.
Lemma sac__ncol234 : ∀ A B C D, Saccheri A B C D → ¬ Col B C D.
Proof.
intros A B C D HSac.
unfold Saccheri in HSac.
spliter.
apply (per2_os__ncol234 A); assumption.
Qed.
The five following lemmas come from Theorem 21.8
Lemma lt_per2_os__lta : ∀ A B C D,
Per B A D → Per A D C →
OS A D B C →
Lt A B C D →
LtA B C D A B C.
Proof.
intros A B C D HPer1 HPer2 Hos Hlt.
apply lt_right_comm in Hlt.
destruct Hlt as [[E []] HNCong].
assert(E≠C) by (intro; subst; auto).
assert(¬ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
assert(¬ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side).
assert_diffs.
assert(HNCol1 := per2_os__ncol123 A B C D HPer1 HPer2 Hos).
assert(HNCol2 := per2_os__ncol234 A B C D HPer1 HPer2 Hos).
assert(HSac : Saccheri A B E D).
{ repeat split; Cong.
apply (per_col _ _ C); Col.
apply (one_side_transitivity _ _ _ C); auto.
apply one_side_symmetry; apply invert_one_side.
apply out_one_side.
right; Col.
apply bet_out; auto.
}
assert(¬ Col E C B) by (intro; apply HNCol2; ColR).
assert(Par_strict A B C D).
{ apply (par_not_col_strict _ _ _ _ D); Col.
apply (l12_9 _ _ _ _ A D); Perp.
}
assert_diffs.
apply (lta_trans _ _ _ B E D).
- assert(HInter := l11_41 E C B D).
destruct HInter; Between.
apply (conga_preserves_lta E C B B E D); try (apply conga_refl); auto.
apply (out_conga E C B B C E); try (apply out_trivial); CongA.
apply bet_out; Between.
- apply (conga_preserves_lta A B E A B C); try (apply conga_refl); auto.
apply sac__conga; auto.
split.
{ ∃ E.
split; CongA.
apply os2__inangle.
- apply l12_6.
apply (par_strict_col_par_strict _ _ _ D); Par; Col.
- apply (one_side_transitivity _ _ _ D).
2: apply invert_one_side; apply one_side_symmetry; apply out_one_side; Col; apply bet_out; Between.
apply not_two_sides_one_side; Col.
intro Hts.
destruct Hts as [_ [_ [I []]]].
assert_diffs.
assert(¬ OS A D B C); auto.
apply l9_9.
repeat split; Col.
∃ I.
split; Col.
assert(A≠I) by (intro; subst; assert_cols; Col).
assert(D≠I) by (intro; subst; assert_cols; Col).
apply out2__bet.
{ apply (col_one_side_out _ A); Col.
apply (one_side_transitivity _ _ _ D).
apply invert_one_side; apply out_one_side; Col; apply bet_out; auto.
apply l12_6; Par.
}
apply (col_one_side_out _ D); Col.
apply (one_side_transitivity _ _ _ A).
apply l12_6; Par.
apply invert_one_side; apply one_side_symmetry; apply out_one_side; Col; apply bet_out; Between.
}
intro.
assert(HUn := conga__or_out_ts A B E C).
destruct HUn; auto.
assert_cols; Col.
assert(¬ TS A B E C); auto.
apply l9_9_bis.
apply l12_6.
apply par_strict_right_comm; apply (par_strict_col_par_strict _ _ _ D); Col.
Qed.
Lemma lt4321_per2_os__lta : ∀ A B C D,
Per B A D → Per A D C →
OS A D B C → Lt D C B A →
LtA A B C B C D.
Proof.
intros.
apply lta_comm, lt_per2_os__lta; Perp; Side.
Qed.
Lemma lta_per2_os__lt : ∀ A B C D,
Per B A D → Per A D C →
OS A D B C → LtA B C D A B C →
Lt A B C D.
Proof.
intros A B C D HPer1 HPer2 Hos HLtA.
destruct (or_lt_cong_gt A B C D) as [Hlt | [Hlt | Hcong]]; trivial; exfalso.
- unfold Gt in Hlt.
apply lt_comm in Hlt.
apply (not_and_lta B C D A B C).
split; trivial.
apply lt4321_per2_os__lta; trivial.
- destruct HLtA as [HLeA HNCongA].
apply HNCongA.
apply conga_sym, sac__conga.
unfold Saccheri; repeat (split; trivial).
Qed.
Lemma lta123234_per2_os__lt : ∀ A B C D,
Per B A D → Per A D C →
OS A D B C → LtA A B C B C D →
Lt D C B A.
Proof.
intros.
apply lta_per2_os__lt; Perp; Side.
apply lta_comm; trivial.
Qed.
Lemma conga_per2_os__cong : ∀ A B C D,
Per B A D → Per A D C →
OS A D B C → CongA B C D A B C →
Cong A B C D.
Proof.
intros A B C D HPer1 HPer2 Hos HCongA.
destruct (or_lt_cong_gt A B C D) as [Hlt | [Hlt | Hcong]]; trivial; exfalso.
- destruct (lt_per2_os__lta A B C D); auto.
- unfold Gt in Hlt.
apply lt_comm in Hlt.
destruct (lt4321_per2_os__lta A B C D); CongA.
Qed.
The two following lemmas constitute Theorem 21.11
Lemma mid2_sac__perp_lower : ∀ 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.
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(¬ Col A D C) by (apply per_not_col; auto).
assert(¬ Col B A D) by (apply per_not_col; auto).
assert(HSAS := l11_49 M B A M C D).
destruct HSAS; Cong.
apply (out_conga C B A B C D); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
apply (l8_16_2 _ _ _ A); Col.
{ intro.
assert(¬ OS A D B C); auto.
apply l9_9.
repeat split; Col.
∃ M.
split; Col; Between.
}
∃ D.
split; auto.
Qed.
Lemma mid2_sac__perp_upper : ∀ 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.
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(¬ Col A D C) by (apply per_not_col; auto).
assert(¬ Col B A D) by (apply per_not_col; auto).
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.
assert(Midpoint N B C) by (apply l7_20_bis; Col).
assert(¬ OS A D B C); auto.
apply l9_9.
repeat split; Col.
∃ N.
split; Col; Between.
}
∃ C.
split; auto.
Qed.
Lemma sac__par_strict1423 : ∀ A B C D, Saccheri A B C D → Par_strict A D B C.
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.
assert_diffs.
apply (par_not_col_strict _ _ _ _ C); Col.
2: apply (one_side_not_col123 _ _ _ B); Side.
apply (l12_9 _ _ _ _ M N); auto.
Qed.
Lemma sac__par_strict1234 : ∀ A B C D, Saccheri A B C D → Par_strict A B C D.
Proof.
intros A B C D HSac.
apply par_not_col_strict with C; Col; [|apply sac__ncol123 with D; trivial].
assert (Hd := sac_distincts A B C D HSac); unfold Saccheri in HSac; spliter.
apply l12_9 with A D; Perp.
Qed.
Lemma sac__par1423 : ∀ A B C D, Saccheri A B C D → Par A D B C.
Proof.
intros A B C D HSac.
apply par_strict_par, sac__par_strict1423; trivial.
Qed.
Lemma sac__par1234 : ∀ A B C D, Saccheri A B C D → Par A B C D.
Proof.
intros A B C D HSac.
apply par_strict_par, sac__par_strict1234; trivial.
Qed.
The four following constitute Theorem 22.3
Lemma mid2_sac__lam6521 : ∀ A B C D M N,
Saccheri A B C D →
Midpoint M B C → Midpoint N A D →
Lambert N M B A.
Proof.
intros A B C D M N HSac HM HN.
unfold Lambert.
assert(Hdiff := sac_distincts A B C D HSac).
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.
assert_diffs.
repeat split; auto.
- apply perp_per_1; auto.
apply (perp_col1 _ _ _ D); Perp; Col.
- apply (l8_3 D); Perp; Col.
- apply perp_per_1; auto.
apply (perp_col1 _ _ _ C); Perp; Col.
Qed.
Lemma mid2_sac__lam6534 : ∀ A B C D M N,
Saccheri A B C D →
Midpoint M B C → Midpoint N A D →
Lambert N M C D.
Proof.
intros A B C D M N HSac HM HN.
apply (mid2_sac__lam6521 _ _ B A); try (apply l7_2); auto.
apply sac_perm; auto.
Qed.
Lemma lam6521_mid2__sac : ∀ A B C D M N,
Lambert N M B A →
Midpoint M B C → Midpoint N A D →
Saccheri A B C D.
Proof.
intros A B C D M N HLam HM HN.
unfold Lambert in HLam.
spliter.
assert_diffs.
assert(Per D A B) by (apply (l8_3 N); Col).
assert(ReflectL D A M N).
{ split.
∃ N; Col.
left; apply (perp_col1 _ _ _ N); Col; Perp.
}
assert(ReflectL A D M N) by (apply l10_4_spec; auto).
assert(ReflectL C B M N).
{ split.
∃ M; Col.
left; apply (perp_col1 _ _ _ M); Col; Perp.
}
assert(ReflectL B C M N) by (apply l10_4_spec; auto).
repeat split; auto.
- Perp.
- apply (image_preserves_per D A B _ _ _ M N); auto.
- apply cong_left_commutativity.
apply (l10_10_spec M N); auto.
- apply (col_one_side _ N); Col.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ M); Col.
apply (par_not_col_strict _ _ _ _ M); Col.
apply (l12_9 _ _ _ _ M N); Perp.
apply (per_not_col); Perp.
Qed.
Lemma lam6534_mid2__sac : ∀ A B C D M N,
Lambert N M C D →
Midpoint M B C → Midpoint N A D →
Saccheri A B C D.
Proof.
intros A B C D M N HLam HM HN.
apply sac_perm.
apply (lam6521_mid2__sac _ _ _ _ M N); Midpoint.
Qed.
The six following lemmas constitute Theorem 22.5
Lemma cong_lam__per : ∀ A B C D,
Lambert A B C D →
Cong A D B C →
Per B C D.
Proof.
unfold Lambert.
intros A B C D HLam HCong.
spliter.
apply l8_2, (l11_17 A D C); auto.
apply sac__conga.
repeat split; Perp; Cong.
apply l12_6.
apply (par_not_col_strict _ _ _ _ C); Col.
apply (l12_9 _ _ _ _ D A); Perp.
apply per_not_col; auto.
Qed.
Lemma lam_lt__acute : ∀ A B C D,
Lambert A B C D →
Lt A D B C →
Acute B C D.
Proof.
unfold Lambert.
intros A B C D HLam HLt.
spliter.
∃ A.
∃ D.
∃ C.
split; trivial.
apply lta_left_comm, lt_per2_os__lta; Perp; [|apply lt_right_comm; trivial].
apply l12_6.
apply (par_not_col_strict _ _ _ _ C); Col.
apply (l12_9 _ _ _ _ D A); Perp.
apply per_not_col; auto.
Qed.
Lemma lam_lt__obtuse : ∀ A B C D,
Lambert A B C D →
Lt B C A D →
Obtuse B C D.
Proof.
unfold Lambert.
intros A B C D HLam HLt.
spliter.
∃ A.
∃ D.
∃ C.
split; trivial.
apply lta_left_comm, lt_per2_os__lta; Perp; [|apply lt_right_comm; trivial].
apply l12_6.
apply (par_not_col_strict _ _ _ _ C); Col.
apply (l12_9 _ _ _ _ D A); Perp.
apply not_col_permutation_4, per_not_col; auto.
Qed.
Lemma lam_per__cong : ∀ A B C D,
Lambert A B C D →
Per B C D →
Cong A D B C.
Proof.
intros A B C D HLam HPer.
assert (HL := HLam).
ex_and HL Hd.
destruct (or_lt_cong_gt A D B C) as [Habs|[HCong|Habs]]; trivial;
exfalso; apply (nlta B C D).
- apply acute_per__lta; trivial.
apply (lam_lt__acute A); trivial.
- apply obtuse_per__lta; trivial.
apply (lam_lt__obtuse A); trivial.
Qed.
Lemma acute_lam__lt : ∀ A B C D,
Lambert A B C D →
Acute B C D →
Lt A D B C.
Proof.
intros A B C D HLam HAcute.
destruct (or_lt_cong_gt A D B C) as [|Habs]; trivial.
exfalso; apply (nlta B C D).
destruct Habs.
- apply acute_obtuse__lta; trivial.
apply (lam_lt__obtuse A); trivial.
- assert (HL := HLam).
ex_and HL Hd.
apply acute_per__lta; trivial.
apply (cong_lam__per A); trivial.
Qed.
Lemma lam_obtuse__lt : ∀ A B C D,
Lambert A B C D →
Obtuse B C D →
Lt B C A D.
Proof.
intros A B C D HLam HObtuse.
destruct (or_lt_cong_gt A D B C) as [Habs|[Habs|HLt]]; trivial;
exfalso; apply (nlta B C D).
- apply acute_obtuse__lta; trivial.
apply (lam_lt__acute A); trivial.
- assert (HL := HLam).
ex_and HL Hd.
apply obtuse_per__lta; trivial.
apply (cong_lam__per A); trivial.
Qed.
The three following lemmas constitute Omar Khayyam's Theorem (22.6)
Lemma cong_sac__per : ∀ A B C D,
Saccheri A B C D →
Cong A D B C ↔ Per A B C.
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(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN).
apply sac_distincts in HSac; spliter.
assert_diffs.
split.
- intro HCong.
apply (per_col _ _ M); Col.
apply l8_2, (cong_lam__per N); auto.
apply cong_commutativity; apply (cong_cong_half_1 _ _ D _ _ C); auto.
- intro HPer.
apply cong_mid2__cong with N M; trivial.
apply cong_commutativity, lam_per__cong; trivial.
apply l8_2, per_col with C; Col.
Qed.
Lemma lt_sac__acute : ∀ A B C D,
Saccheri A B C D →
Lt A D B C ↔ Acute A B C.
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(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN).
assert (HCongA : CongA A B C M B A).
{ apply sac_distincts in HSac; spliter.
assert_diffs.
apply conga_right_comm, out2__conga.
apply out_trivial; auto.
apply bet_out; Between.
}
split.
- intro HLt.
apply (acute_conga__acute M B A); CongA.
apply (lam_lt__acute N); trivial.
apply lt_comm, lt_mid2__lt12 with D C; trivial.
- intro HAcute.
apply lt_mid2__lt13 with N M; trivial.
apply lt_comm, acute_lam__lt; trivial.
apply (acute_conga__acute A B C); trivial.
Qed.
Lemma lt_sac__obtuse : ∀ A B C D,
Saccheri A B C D →
Lt B C A D ↔ Obtuse A B C.
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(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN).
assert (HCongA : CongA A B C M B A).
{ apply sac_distincts in HSac; spliter.
assert_diffs.
apply conga_right_comm, out2__conga.
apply out_trivial; auto.
apply bet_out; Between.
}
split.
- intro HLt.
apply (obtuse_conga__obtuse M B A); CongA.
apply (lam_lt__obtuse N); trivial.
apply lt_comm, lt_mid2__lt12 with C D; trivial.
- intro HObtuse.
apply lt_mid2__lt13 with M N; trivial.
apply lt_comm, lam_obtuse__lt; trivial.
apply (obtuse_conga__obtuse A B C); trivial.
Qed.
Lemma t22_7__per : ∀ A B C D P Q,
Saccheri A B C D →
Bet B P C → Bet A Q D →
A ≠ Q → B ≠ P → P ≠ C →
Per P Q A →
Cong P Q A B →
Per A B C.
Proof.
intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ HCong.
assert(HSac' := HSac).
destruct HSac'.
spliter.
assert(HNCol1 : ¬ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
assert(HNCol2 : ¬ Col B C D) by (apply (per2_os__ncol234 A); auto).
assert_diffs.
assert(Q ≠ D).
{ intro.
subst Q.
destruct HSac.
spliter.
assert(Col C P D) by (apply (per_per_col _ _ A); Perp).
apply HNCol2; ColR.
}
assert(HSac1 : Saccheri A B P Q).
{ repeat split; Cong.
apply (per_col _ _ D); Col.
Perp.
apply (col_one_side _ D); Col;
apply (l9_17 _ _ C); Between.
}
assert(HSac2 : Saccheri D C P Q).
{ repeat split; auto.
apply (per_col _ _ A); Col; Perp.
apply (l8_3 A); Col; Perp.
apply (cong_transitivity _ _ A B); Cong.
apply (col_one_side _ A); Col.
apply (l9_17 _ _ B); Between; Side.
}
apply (bet_suma__per _ _ _ B P C); auto.
apply (conga3_suma__suma B P Q Q P C B P C); try (apply conga_refl); auto.
- ∃ C.
repeat (split; CongA).
apply l9_9.
destruct HSac1.
destruct HSac2.
spliter.
repeat split; auto.
apply (per2_os__ncol234 A); auto.
apply (per2_os__ncol234 D); auto.
∃ P; Col.
- apply (out_conga B P Q A B P); try apply (out_trivial); auto.
apply conga_sym; apply sac__conga; auto.
apply bet_out; auto.
- apply (conga_trans _ _ _ P C D).
apply sac__conga; apply sac_perm; auto.
apply (out_conga B C D A B C); try apply (out_trivial); auto.
apply conga_sym; apply sac__conga; auto.
apply l6_6; apply bet_out; Between.
Qed.
Lemma t22_7__acute : ∀ A B C D P Q,
Saccheri A B C D →
Bet B P C → Bet A Q D →
A ≠ Q → B ≠ P → P ≠ C →
Per P Q A →
Lt P Q A B →
Acute A B C.
Proof.
intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ Hlt.
assert(HSac' := HSac).
destruct HSac'.
spliter.
assert(HNCol1 : ¬ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
assert(HNCol2 : ¬ Col A B C) by (apply (per2_os__ncol123 _ _ _ D); auto).
assert_diffs.
assert(OS A Q B P) by (apply (col_one_side _ D); Col; apply (l9_17 _ _ C); auto).
assert(HNCol3 : ¬ Col A Q P) by (apply (one_side_not_col123 _ _ _ B); Side).
assert(HNCol4 : ¬ Col B P Q).
{ apply (per2_os__ncol234 A); auto.
apply (per_col _ _ D); Col.
Perp.
}
assert_diffs.
assert(Q ≠ D).
{ intro.
subst Q.
assert(Col C P D) by (apply (per_per_col _ _ A); Perp).
assert(Haux : ¬ Col B C D) by (apply (per2_os__ncol234 A); auto).
apply Haux; ColR.
}
assert(HSuma := ex_suma A B C A B C).
destruct HSuma as [R [S [T HSuma]]]; auto.
assert_diffs.
assert(Hlta1 : LtA A B C B P Q).
{ apply (conga_preserves_lta A B P B P Q); try (apply conga_refl); auto.
apply (out_conga A B P A B P); try (apply out_trivial); CongA; apply bet_out; auto.
apply lt4321_per2_os__lta; auto.
apply (per_col _ _ D); Col.
Perp.
apply lt_comm; auto.
}
assert(Hlta2 : LtA A B C Q P C).
{ apply (conga_preserves_lta D C P C P Q); try (apply conga_pseudo_refl); auto.
- apply sac__conga in HSac.
apply (out_conga D C B A B C); try (apply out_trivial); CongA.
apply l6_6; apply bet_out; Between.
- apply lt4321_per2_os__lta; auto.
apply (per_col _ _ A); Perp; Col.
apply (l8_3 A); Perp; Col.
apply (col_one_side _ A); Col; apply (l9_17 _ _ B); Between; Side.
apply (cong2_lt__lt P Q A B); Cong.
}
assert(¬ OS P Q B C).
{ apply l9_9.
repeat split; Col.
intro; apply HNCol4; ColR.
∃ P; Col.
}
assert(SAMS B P Q Q P C).
{ repeat split; auto.
right; intro; Col.
∃ C.
repeat (split; CongA).
intro Hts.
destruct Hts as [_ []]; assert_cols; Col.
}
assert(SAMS A B C A B C).
{ destruct Hlta1.
destruct Hlta2.
apply (sams_lea2__sams _ _ _ _ _ _ B P Q Q P C); auto.
}
apply (nbet_sams_suma__acute _ _ _ R S T); auto.
intro.
apply (nlta R S T).
apply (sams_lta2_suma2__lta A B C A B C _ _ _ B P Q Q P C); auto.
∃ C.
split; CongA.
split; auto.
apply conga_line; auto.
Qed.
Lemma t22_7__obtuse : ∀ A B C D P Q,
Saccheri A B C D →
Bet B P C → Bet A Q D →
A ≠ Q → B ≠ P → P ≠ C →
Per P Q A →
Lt A B P Q →
Obtuse A B C.
Proof.
intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ Hlt.
assert(HSac' := HSac).
destruct HSac'.
spliter.
assert(HNCol1 : ¬ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
assert(HNCol2 : ¬ Col A B C) by (apply (per2_os__ncol123 _ _ _ D); auto).
assert(OS A Q B P) by (apply (col_one_side _ D); Col; apply (l9_17 _ _ C); auto).
assert(HNCol3 : ¬ Col A Q P) by (apply (one_side_not_col123 _ _ _ B); Side).
assert_diffs.
assert(Q ≠ D).
{ intro.
subst Q.
assert(Col C P D) by (apply (per_per_col _ _ A); Perp).
assert(Haux : ¬ Col B C D) by (apply (per2_os__ncol234 A); auto).
apply Haux; ColR.
}
assert(OS D Q C P) by (apply (col_one_side _ A); Col; apply (l9_17 _ _ B); Side; Between).
apply nsams__obtuse; auto.
intro HIsi.
assert(HSuma := ex_suma A B C A B C).
destruct HSuma as [R [S [T HSuma]]]; auto.
assert_diffs.
apply (nlta R S T).
apply (lea123456_lta__lta _ _ _ B P C).
apply l11_31_2; auto.
apply (sams_lta2_suma2__lta B P Q Q P C _ _ _ A B C A B C); auto.
- apply (conga_preserves_lta B P Q A B P); try (apply conga_refl); auto.
apply (out_conga A B P A B P); try (apply out_trivial); CongA; apply bet_out; auto.
apply lt_per2_os__lta; auto.
apply (per_col _ _ D); Col.
Perp.
- apply (conga_preserves_lta Q P C P C D); try (apply conga_refl); auto.
{ apply sac__conga in HSac.
apply (out_conga B C D A B C); try (apply out_trivial); CongA.
apply l6_6; apply bet_out; Between.
}
apply lt4321_per2_os__lta; Side.
apply (per_col _ _ A); Perp; Col.
apply (l8_3 A); Col.
apply (cong2_lt__lt A B P Q); Cong.
- ∃ C.
repeat (split; CongA).
apply l9_9.
assert(HNCol4 : ¬ Col C P Q).
{ apply (per2_os__ncol234 D); auto.
apply (per_col _ _ A); Perp; Col.
apply (l8_3 A); Perp; Col.
}
repeat split; Col.
intro; apply HNCol4; ColR.
∃ P; Col.
Qed.
Lemma t22_7__cong : ∀ A B C D P Q,
Saccheri A B C D →
Bet B P C → Bet A Q D →
A ≠ Q → B ≠ P → P ≠ C →
Per P Q A → Per A B C →
Cong P Q A B.
Proof.
intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ HPer.
assert(Hdiff := sac_distincts A B C D HSac).
spliter.
elim(Cong_dec P Q A B); auto.
intro.
exfalso.
apply (nlta A B C).
elim(le_cases P Q A B).
- intro.
apply acute_per__lta; auto.
apply (t22_7__acute _ _ _ D P Q); auto.
split; auto.
- intro.
apply obtuse_per__lta; auto.
apply (t22_7__obtuse _ _ _ D P Q); auto.
split; Cong.
Qed.
Lemma t22_7__lt5612 : ∀ A B C D P Q,
Saccheri A B C D →
Bet B P C → Bet A Q D →
A ≠ Q → B ≠ P → P ≠ C →
Per P Q A → Acute A B C →
Lt P Q A B.
Proof.
intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ Hacute.
assert(Hdiff := sac_distincts A B C D HSac).
spliter.
elim(Cong_dec P Q A B).
{ intro.
exfalso.
apply (nlta A B C).
apply acute_per__lta; auto.
apply (t22_7__per _ _ _ D P Q); auto.
}
intro.
split; auto.
elim(le_cases P Q A B); auto.
intro.
exfalso.
apply (nlta A B C).
apply acute_obtuse__lta; auto.
apply (t22_7__obtuse _ _ _ D P Q); auto.
split; Cong.
Qed.
Lemma t22_7__lt1256 : ∀ A B C D P Q,
Saccheri A B C D →
Bet B P C → Bet A Q D →
A ≠ Q → B ≠ P → P ≠ C →
Per P Q A → Obtuse A B C →
Lt A B P Q.
Proof.
intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ Hobtuse.
assert(Hdiff := sac_distincts A B C D HSac).
spliter.
elim(Cong_dec P Q A B).
{ intro.
exfalso.
apply (nlta A B C).
apply obtuse_per__lta; auto.
apply (t22_7__per _ _ _ D P Q); auto.
}
intro.
split; Cong.
elim(le_cases P Q A B); auto.
intro.
exfalso.
apply (nlta A B C).
apply acute_obtuse__lta; auto.
apply (t22_7__acute _ _ _ D P Q); auto.
split; auto.
Qed.
Lemma t22_8__per : ∀ A B C D R S,
Saccheri A B C D →
Bet B C R → Bet A D S →
C ≠ R →
Per A S R →
Cong R S A B →
Per A B C.
Proof.
intros A B C D R S HSac HR HS HCR HPer HCong.
assert(Hdiff := sac_distincts A B C D HSac).
assert(HSac' := HSac).
unfold Saccheri in HSac'.
spliter.
assert(A ≠ S) by (intro; treat_equalities; auto).
assert(B ≠ R) by (intro; treat_equalities; auto).
assert(HSac' : Saccheri A B R S).
{ repeat split; Cong.
apply (per_col _ _ D); Col.
apply (col_one_side _ D); Col.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ C); Col.
apply sac__par_strict1423; auto.
}
apply (per_col _ _ R); Col.
apply (t22_7__per _ _ _ S C D); Perp; Cong.
Qed.
Lemma t22_8__acute : ∀ A B C D R S,
Saccheri A B C D →
Bet B C R → Bet A D S →
C ≠ R →
Per A S R →
Lt A B R S →
Acute A B C.
Proof.
intros A B C D R S HSac HR HS HCR HPer Hlt.
assert(Hdiff := sac_distincts A B C D HSac).
assert(HSac' := HSac).
unfold Saccheri in HSac'.
spliter.
assert(R ≠ S) by (intro; subst S; destruct Hlt; assert(A = B); auto; apply (le_zero _ _ R); auto).
assert(A ≠ S) by (intro; treat_equalities; auto).
assert(B ≠ R) by (intro; treat_equalities; auto).
assert(HNCol1 : ¬ Col A S R) by (apply per_not_col; auto).
assert(D ≠ S).
{ intro.
subst S.
assert(Col C R D) by (apply (per_per_col _ _ A); Perp).
assert(Haux : ¬ Col B C D) by (apply (per2_os__ncol234 A); auto).
apply Haux; ColR.
}
assert(HJ := Hlt).
apply lt_right_comm in HJ.
destruct HJ as [[J []] _].
assert_diffs.
assert(J ≠ R) by (intro; subst J; destruct Hlt; Cong).
assert(CongA A B C B C D) by (apply sac__conga; auto).
apply (acute_lea_acute _ _ _ B C D); Lea.
apply (acute_chara _ _ _ R); auto.
assert(HSac1 : Saccheri A B J S).
{ repeat split; Cong.
apply (per_col _ _ D); Col.
apply (per_col _ _ R); Col.
apply (one_side_transitivity _ _ _ R).
2: apply invert_one_side; apply out_one_side; Col; apply l6_6; apply bet_out; auto.
apply (col_one_side _ D); Col.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ C); Col.
apply sac__par_strict1423; auto.
}
assert(HSac2 : Saccheri D C J S).
{ repeat split; auto.
apply (per_col _ _ A); Perp; Col.
apply (per_col _ _ R); Col; apply (l8_3 A); Col.
apply (cong_transitivity _ _ A B); Cong.
apply (one_side_transitivity _ _ _ R).
2: apply invert_one_side; apply out_one_side; try (left; intro; apply HNCol1; ColR); apply l6_6; apply bet_out; auto.
apply (col_one_side _ A); Col.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ B); Col.
apply par_strict_comm.
apply sac__par_strict1423; auto.
}
assert(CongA A B J B J S) by (apply sac__conga; auto).
assert(CongA D C J C J S) by (apply sac__conga; auto).
assert(HNCol2 : ¬ Col B J S) by (apply (sac__ncol234 A); auto).
assert(HNCol3 : ¬ Col B J R) by (intro; apply HNCol2; ColR).
assert(HNCol4 : ¬ Col B J C) by (intro; apply HNCol3; ColR).
assert(HNCol5 : ¬ Col D C J) by (apply (sac__ncol123 _ _ _ S); auto).
assert_diffs.
assert(TS C J D R).
{ apply (l9_8_2 _ _ S).
repeat split; auto; try (intro; apply HNCol2; ColR); ∃ J; Col.
assert(HPars := sac__par_strict1423 D C J S HSac2).
apply l12_6; Par.
}
apply (sams_lta2_suma2__lta A B J J B C _ _ _ D C J J C R).
- assert(OS S R C B).
{ apply invert_one_side.
apply out_one_side.
right; intro; apply HNCol2; ColR.
apply bet_out; Between.
}
apply (conga_preserves_lta S J B S J C); CongA.
split.
{ ∃ B.
split; CongA.
apply os_ts__inangle.
- apply l9_2.
apply (l9_8_2 _ _ R).
repeat split; Col; ∃ J; Col; Between.
apply invert_one_side.
apply out_one_side; Col.
apply l6_6.
apply bet_out; auto.
- apply invert_one_side.
apply (col_one_side _ R); Col.
}
intro Habs.
apply conga__or_out_ts in Habs.
destruct Habs.
assert_cols; Col.
assert(¬ TS S J B C); auto.
apply l9_9_bis.
apply (col_one_side _ R); Col; Side.
- apply (conga_preserves_lta C B J J C R); try (apply conga_refl); CongA.
assert (HInter := l11_41 C B J R).
destruct HInter; Col.
- repeat split; auto.
right; intro; apply HNCol5; Col.
∃ R.
split; CongA; split.
apply l9_9; auto.
apply l9_9_bis.
apply l12_6.
apply (par_not_col_strict _ _ _ _ J); Col.
apply (par_col_par _ _ _ S); Col.
unfold Saccheri in HSac2.
spliter.
apply (l12_9 _ _ _ _ D S); Perp.
- ∃ C.
repeat (split; CongA).
apply l9_9.
apply (l9_8_2 _ _ S).
2: apply l12_6; assert(HPars := sac__par_strict1423 A B J S HSac1); Par.
apply l9_2.
apply (l9_8_2 _ _ R).
repeat split; Col; ∃ J; split; Col; Between.
apply out_one_side; Col.
apply l6_6.
apply bet_out; auto.
- ∃ R.
repeat (split; CongA).
apply l9_9; auto.
Qed.
Lemma t22_8__obtuse : ∀ A B C D R S,
Saccheri A B C D →
Bet B C R → Bet A D S →
C ≠ R →
Per A S R →
Lt R S A B →
Obtuse A B C.
Proof.
intros A B C D R S HSac HR HS HCR HPer Hlt.
assert(Hdiff := sac_distincts A B C D HSac).
assert(HSac' := HSac).
unfold Saccheri in HSac'.
spliter.
assert(A ≠ S) by (intro; treat_equalities; auto).
assert(B ≠ R) by (intro; treat_equalities; auto).
assert(D ≠ S).
{ intro.
subst S.
assert(Col C R D) by (apply (per_per_col _ _ A); Perp).
assert(Haux : ¬ Col B C D) by (apply (per2_os__ncol234 A); auto).
apply Haux; ColR.
}
assert(HPars := sac__par_strict1423 A B C D HSac).
assert(OS A S B R).
{ apply (col_one_side _ D); Col.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ C); Col.
}
assert(HNCol1 : ¬ Col A S R) by (apply (one_side_not_col123 _ _ _ B); Side).
assert(HI := l5_5_1 S R A B).
destruct HI as [I []].
destruct Hlt; Le.
assert_diffs.
assert(R ≠ I) by (intro; subst I; destruct Hlt; Cong).
assert(CongA A B C B C D) by (apply sac__conga; auto).
apply (obtuse_gea_obtuse _ _ _ B C D).
2: apply conga__lea; CongA.
apply (obtuse_chara _ _ _ R); auto.
assert(HSac1 : Saccheri A B I S).
{ repeat split; Cong.
apply (per_col _ _ D); Col.
apply (per_col _ _ R); Col.
apply (one_side_transitivity _ _ _ R).
2: apply invert_one_side; apply out_one_side; Col; apply bet_out; auto.
apply (col_one_side _ D); Col.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ C); Col.
}
assert(HSac2 : Saccheri D C I S).
{ repeat split; auto.
apply (per_col _ _ A); Perp; Col.
apply (per_col _ _ R); Col; apply (l8_3 A); Col.
apply (cong_transitivity _ _ A B); Cong.
apply (one_side_transitivity _ _ _ R).
2: apply invert_one_side; apply out_one_side; try (left; intro; apply HNCol1; ColR); apply bet_out; auto.
apply (col_one_side _ A); Col.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ B); Col; Par.
}
assert(CongA A B I B I S) by (apply sac__conga; auto).
assert(CongA D C I C I S) by (apply sac__conga; auto).
assert(HNCol2 : ¬ Col C I S) by (apply (sac__ncol234 D); auto).
assert(HNCol3 : ¬ Col C I R) by (intro; apply HNCol2; ColR).
assert(HNCol4 : ¬ Col C I B) by (intro; apply HNCol3; ColR).
assert(HNCol5 : ¬ Col D C I) by (apply (sac__ncol123 _ _ _ S); auto).
assert_diffs.
assert(TS C R I D).
{ apply l9_2.
apply (l9_8_2 _ _ S).
repeat split; auto; try (intro; apply HNCol2; ColR); ∃ R; Col.
apply one_side_symmetry.
apply (col_one_side _ B); Col.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ A); Col; Par.
}
apply(sams_lta2_suma2__lta456 I C R _ _ _ D C I I B C _ _ _ A B I).
- apply lta_left_comm.
assert (HInter := l11_41 C B I R).
destruct HInter; Col.
- assert(OS R S C B).
{ apply out_one_side.
right; intro; apply HNCol2; ColR.
apply bet_out; Between.
}
apply (conga_preserves_lta S I C S I B); CongA.
split.
{ ∃ C.
split; CongA.
apply os2__inangle.
- apply invert_one_side.
apply (col_one_side _ R); Col; Side.
- apply (one_side_transitivity _ _ _ R).
2: apply invert_one_side; apply out_one_side; Col; apply l6_6; apply bet_out; auto.
apply out_one_side.
right; intro; apply HNCol3; ColR.
apply l6_6.
apply bet_out; Between.
}
intro Habs.
apply conga__or_out_ts in Habs.
destruct Habs.
assert_cols; Col.
assert(¬ TS S I C B); auto.
apply l9_9_bis.
apply (col_one_side _ R); Col; Side.
- repeat split; auto.
right; intro; apply HNCol4; ColR.
∃ D.
split; CongA; split.
apply l9_9; auto.
apply l9_9_bis.
apply (one_side_transitivity _ _ _ S).
apply out_one_side; Col; apply bet_out; Between.
apply l12_6.
assert(Haux := sac__par_strict1423 D C I S HSac2); Par.
- ∃ D.
repeat (split; CongA).
apply l9_9; auto.
- ∃ A.
repeat (split; CongA).
apply l9_9.
apply l9_2.
apply (l9_8_2 _ _ S).
repeat split; Col; try (intro; apply HNCol2; ColR); ∃ R; split; Col.
apply one_side_symmetry.
apply l12_6.
apply (par_strict_col_par_strict _ _ _ D); Col; Par.
Qed.
Lemma t22_8__cong : ∀ A B C D R S,
Saccheri A B C D → Bet B C R → Bet A D S →
C ≠ R → Per A S R → Per A B C → Cong R S A B.
Proof.
intros A B C D R S HSac.
intros.
elim(Cong_dec R S A B); auto.
intro.
assert(Hdiff := sac_distincts A B C D HSac).
spliter.
exfalso.
apply (nlta A B C).
elim(le_cases R S A B).
- intro.
apply obtuse_per__lta; auto.
apply (t22_8__obtuse _ _ _ D R S); auto.
split; auto.
- intro.
apply acute_per__lta; auto.
apply (t22_8__acute _ _ _ D R S); auto.
split; Cong.
Qed.
Lemma t22_8__lt1256 : ∀ A B C D R S,
Saccheri A B C D →
Bet B C R → Bet A D S →
C ≠ R →
Per A S R → Acute A B C →
Lt A B R S.
Proof.
intros A B C D R S HSac.
intros.
assert_diffs.
elim(Cong_dec R S A B).
{ intro.
exfalso.
apply (nlta A B C).
apply acute_per__lta; auto.
apply (t22_8__per _ _ _ D R S); auto.
}
intro.
elim(le_cases R S A B).
2: intro; split; Cong.
intro.
exfalso.
apply (nlta A B C).
apply acute_obtuse__lta; auto.
apply (t22_8__obtuse _ _ _ D R S); auto.
split; auto.
Qed.
Lemma t22_8__lt5612 : ∀ A B C D R S,
Saccheri A B C D →
Bet B C R → Bet A D S →
C ≠ R →
Per A S R → Obtuse A B C →
Lt R S A B.
Proof.
intros A B C D R S HSac.
intros.
assert_diffs.
elim(Cong_dec R S A B).
{ intro.
exfalso.
apply (nlta A B C).
apply obtuse_per__lta; auto.
apply (t22_8__per _ _ _ D R S); auto.
}
intro.
elim(le_cases R S A B).
intro; split; auto.
intro.
exfalso.
apply (nlta A B C).
apply acute_obtuse__lta; auto.
apply (t22_8__acute _ _ _ D R S); auto.
split; Cong.
Qed.
Lemma t22_9__per : ∀ N M P Q R S,
Lambert N M P Q → Lambert N M R S →
Bet M P R → Bet N Q S →
(Per S R M ↔ Per Q P M).
Proof.
intros N M P Q R S HLamP HLamR HR HS.
elim(eq_dec_points P R).
{ intro.
unfold Lambert in ×.
spliter.
treat_equalities.
assert(Q = S).
2: subst; split; auto.
apply (l8_18_uniqueness N Q P); Col.
apply per_not_col; auto.
Perp.
apply (perp_col _ S); Perp; Col.
}
intro.
assert(HP' := symmetric_point_construction P M).
destruct HP' as [P' HP'].
apply l7_2 in HP'.
assert(HQ' := symmetric_point_construction Q N).
destruct HQ' as [Q' HQ'].
apply l7_2 in HQ'.
assert(HR' := symmetric_point_construction R M).
destruct HR' as [R' HR'].
apply l7_2 in HR'.
assert(HS' := symmetric_point_construction S N).
destruct HS' as [S' HS'].
apply l7_2 in HS'.
assert(HSacR := lam6534_mid2__sac S' R' R S M N HLamR HR' HS').
assert(HSacP := lam6534_mid2__sac Q' P' P Q M N HLamP HP' HQ').
assert(Cong S' R' R S ∧ Cong Q' P' P Q) by (unfold Saccheri in *; spliter; split; auto).
unfold Lambert in ×.
spliter.
assert(HCongaR := sac__conga S' R' R S HSacR).
assert(HCongaQ := sac__conga Q' P' P Q HSacP).
assert(Bet P' P R) by (apply (outer_transitivity_between2 _ M); Between).
assert(Bet Q' Q S) by (apply (outer_transitivity_between2 _ N); Between).
assert(Bet R' P R) by (apply (between_exchange2 _ M); Between).
assert(Bet S' Q S) by (apply (between_exchange2 _ N); Between).
assert_diffs.
assert(Per Q' S R) by (apply (l8_3 N); auto; ColR).
assert(Per S' Q P) by (apply (l8_3 N); auto; ColR).
split.
- intro.
apply (per_col _ _ P'); Col.
apply (l11_17 Q' P' P); CongA.
apply (t22_8__per _ _ _ Q R S); auto.
apply cong_symmetry.
apply (cong_transitivity _ _ S' R'); auto.
apply (cong_transitivity _ _ P Q); auto.
apply (t22_7__cong _ _ R S); auto; try (intro; treat_equalities; auto).
Perp.
apply (l11_17 S R R'); CongA.
apply (per_col _ _ M); Col.
- intro.
apply (per_col _ _ R'); Col.
apply (l11_17 S' R' R); CongA.
apply (t22_7__per _ _ _ S P Q); auto; try (intro; treat_equalities; auto).
Perp.
apply cong_symmetry.
apply (cong_transitivity _ _ Q' P'); auto.
apply (cong_transitivity _ _ R S); auto.
apply (t22_8__cong _ _ P Q); auto.
apply (l11_17 Q P P'); CongA.
apply (per_col _ _ M); Col.
Qed.
Lemma t22_9__acute : ∀ N M P Q R S,
Lambert N M P Q → Lambert N M R S →
Bet M P R → Bet N Q S →
(Acute S R M ↔ Acute Q P M).
Proof.
intros N M P Q R S HLamP HLamR HR HS.
elim(eq_dec_points P R).
{ intro.
unfold Lambert in ×.
spliter.
treat_equalities.
assert(Q = S).
2: subst; split; auto.
apply (l8_18_uniqueness N Q P); Col.
apply per_not_col; auto.
Perp.
apply (perp_col _ S); Perp; Col.
}
intro.
assert(HP' := symmetric_point_construction P M).
destruct HP' as [P' HP'].
apply l7_2 in HP'.
assert(HQ' := symmetric_point_construction Q N).
destruct HQ' as [Q' HQ'].
apply l7_2 in HQ'.
assert(HR' := symmetric_point_construction R M).
destruct HR' as [R' HR'].
apply l7_2 in HR'.
assert(HS' := symmetric_point_construction S N).
destruct HS' as [S' HS'].
apply l7_2 in HS'.
assert(HSacR := lam6534_mid2__sac S' R' R S M N HLamR HR' HS').
assert(HSacP := lam6534_mid2__sac Q' P' P Q M N HLamP HP' HQ').
assert(Cong S' R' R S ∧ Cong Q' P' P Q) by (unfold Saccheri in *; spliter; split; auto).
unfold Lambert in ×.
spliter.
assert(HCongaR := sac__conga S' R' R S HSacR).
assert(HCongaQ := sac__conga Q' P' P Q HSacP).
assert(Bet P' P R) by (apply (outer_transitivity_between2 _ M); Between).
assert(Bet Q' Q S) by (apply (outer_transitivity_between2 _ N); Between).
assert(Bet R' P R) by (apply (between_exchange2 _ M); Between).
assert(Bet S' Q S) by (apply (between_exchange2 _ N); Between).
assert_diffs.
assert(Per Q' S R) by (apply (l8_3 N); auto; ColR).
assert(Per S' Q P) by (apply (l8_3 N); auto; ColR).
split.
- intro.
apply (acute_conga__acute Q' P' P).
2: apply (out_conga Q' P' P Q P P'); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
apply (t22_8__acute _ _ _ Q R S); auto.
apply (cong2_lt__lt P Q S' R'); Cong.
apply (t22_7__lt5612 _ _ R S); Perp; try (intro; treat_equalities; auto).
apply (acute_conga__acute S R M); auto.
apply (out_conga S R R' S' R' R); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
- intro.
apply (acute_conga__acute S' R' R).
2: apply (out_conga S' R' R S R R'); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
apply (t22_7__acute _ _ _ S P Q); Perp; try (intro; treat_equalities; auto).
apply (cong2_lt__lt Q' P' R S); Cong.
apply (t22_8__lt1256 _ _ P Q); auto.
apply (acute_conga__acute Q P M); auto.
apply (out_conga Q P P' Q' P' P); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
Qed.
Lemma t22_9__obtuse : ∀ N M P Q R S,
Lambert N M P Q → Lambert N M R S →
Bet M P R → Bet N Q S →
(Obtuse S R M ↔ Obtuse Q P M).
Proof.
intros N M P Q R S HLamP HLamR HR HS.
split.
- intro.
assert(H' := HLamP).
unfold Lambert in H'.
spliter.
assert_diffs.
elim(angle_partition Q P M); auto.
{ intro.
exfalso.
apply (nlta S R M).
apply acute_obtuse__lta; auto.
apply (t22_9__acute N _ P Q); auto.
}
intro HUn.
destruct HUn; auto.
exfalso.
apply (nlta S R M).
apply obtuse_per__lta; auto.
apply (t22_9__per N _ P Q); auto.
- intro.
assert(H' := HLamR).
unfold Lambert in H'.
spliter.
assert_diffs.
elim(angle_partition S R M); auto.
{ intro.
exfalso.
apply (nlta Q P M).
apply acute_obtuse__lta; auto.
apply (t22_9__acute N _ _ _ R S); auto.
}
intro HUn.
destruct HUn; auto.
exfalso.
apply (nlta Q P M).
apply obtuse_per__lta; auto.
apply (t22_9__per N _ _ _ R S); auto.
Qed.
The two following lemmas come from Theorem 22.4
Lemma cong2_lam2__cong : ∀ N M P Q N' M' P' Q',
Lambert N M P Q → Lambert N' M' P' Q' →
Cong N Q N' Q' → Cong P Q P' Q' →
Cong N M N' M'.
Proof.
intros N M P Q N' M' P' Q' HLam HLam' HCong1 HCong2.
unfold Lambert in ×.
spliter.
assert(¬ Col N M P) by (apply per_not_col; auto).
assert(¬ Col M N Q) by (apply per_not_col; auto).
assert(¬ Col M' N' Q') by (apply per_not_col; auto).
assert_diffs.
assert(Par_strict N Q M P ∧ Par_strict N' Q' M' P').
{ split;
[apply (par_not_col_strict _ _ _ _ M)|apply (par_not_col_strict _ _ _ _ M')]; Col;
[apply (l12_9 _ _ _ _ N M)|apply (l12_9 _ _ _ _ N' M')]; Perp.
}
spliter.
assert(OS N Q M P ∧ OS N' Q' M' P' ∧ OS P M N Q ∧ OS P' M' N' Q').
{ repeat split;
apply l12_6; Par.
}
assert(OS P Q M N ∧ OS P' Q' M' N').
{ split;
apply l12_6;
apply par_strict_symmetry;
[apply (par_not_col_strict _ _ _ _ Q)|apply (par_not_col_strict _ _ _ _ Q')]; Col;
[apply (l12_9 _ _ _ _ N Q)|apply (l12_9 _ _ _ _ N' Q')]; Perp.
}
spliter.
assert(HSAS := l11_49 N Q P N' Q' P').
destruct HSAS as [HCong3 [HConga1 HConga2]]; Cong.
apply l11_16; auto.
assert(CongA M N P M' N' P').
{ apply (l11_22b _ _ _ Q _ _ _ Q').
split; auto; split; auto; split; auto.
apply l11_16; auto.
}
assert(HAAS := l11_50_2 P N M P' N' M').
destruct HAAS as [HCong4 [HCong5 HCong6]]; Col; Cong.
apply l11_16; auto.
CongA.
Qed.
Lemma cong2_lam2__conga : ∀ N M P Q N' M' P' Q',
Lambert N M P Q → Lambert N' M' P' Q' →
Cong N Q N' Q' → Cong P Q P' Q' →
CongA M P Q M' P' Q'.
Proof.
intros N M P Q N' M' P' Q' HLam HLam' HCong1 HCong2.
unfold Lambert in ×.
spliter.
assert(¬ Col N M P) by (apply per_not_col; auto).
assert(¬ Col M N Q) by (apply per_not_col; auto).
assert(¬ Col M' N' Q') by (apply per_not_col; auto).
assert_diffs.
assert(Par_strict N Q M P ∧ Par_strict N' Q' M' P').
{ split;
[apply (par_not_col_strict _ _ _ _ M)|apply (par_not_col_strict _ _ _ _ M')]; Col;
[apply (l12_9 _ _ _ _ N M)|apply (l12_9 _ _ _ _ N' M')]; Perp.
}
spliter.
assert(OS N Q M P ∧ OS N' Q' M' P' ∧ OS P M N Q ∧ OS P' M' N' Q').
{ repeat split;
apply l12_6; Par.
}
assert(OS P Q M N ∧ OS P' Q' M' N').
{ split;
apply l12_6;
apply par_strict_symmetry;
[apply (par_not_col_strict _ _ _ _ Q)|apply (par_not_col_strict _ _ _ _ Q')]; Col;
[apply (l12_9 _ _ _ _ N Q)|apply (l12_9 _ _ _ _ N' Q')]; Perp.
}
spliter.
assert(HSAS := l11_49 N Q P N' Q' P').
destruct HSAS as [HCong3 [HConga1 HConga2]]; Cong.
apply l11_16; auto.
assert(CongA M N P M' N' P').
{ apply (l11_22b _ _ _ Q _ _ _ Q').
split; auto; split; auto; split; auto.
apply l11_16; auto.
}
assert(HAAS := l11_50_2 P N M P' N' M').
destruct HAAS as [HCong4 [HCong5 HCong6]]; Col; Cong.
apply l11_16; auto.
CongA.
apply (l11_22a _ _ _ N _ _ _ N').
split.
apply l9_31; Side.
split.
apply l9_31; Side.
split; CongA.
Qed.
Lemma cong2_sac2__cong : ∀ A B C D A' B' C' D',
Saccheri A B C D → Saccheri A' B' C' D' →
Cong A B A' B' → Cong A D A' D' →
Cong B C B' C'.
Proof.
intros A B C D A' B' C' D' HSac HSac' HCongB HCongL.
assert(Hdiff := sac_distincts A B C D HSac).
assert(Hdiff' := sac_distincts A' B' C' D' HSac').
unfold Saccheri in ×.
spliter.
destruct (l11_49 B A D B' A' D') as [HCongD [HConga1 HConga2]]; Cong.
apply l11_16; auto.
destruct (l11_49 B D C B' D' C'); Cong.
2:apply (cong_transitivity _ _ A B); Cong; apply (cong_transitivity _ _ A' B'); Cong.
apply (l11_22b _ _ _ A _ _ _ A').
split; Side.
split; Side.
split; CongA.
apply l11_16; auto.
Qed.
Lemma sac__perp1214 : ∀ A B C D, Saccheri A B C D → Perp A B A D.
Proof.
intros A B C D HSac.
assert (Hdiff := sac_distincts A B C D HSac).
unfold Saccheri in HSac; spliter.
apply perp_left_comm, per_perp; auto.
Qed.
Lemma sac__perp3414 : ∀ A B C D, Saccheri A B C D → Perp C D A D.
Proof.
intros A B C D HSac.
apply perp_comm, (sac__perp1214 _ _ B), sac_perm; trivial.
Qed.
Lemma sac2__sac : ∀ A B C D E F, Saccheri A B C D → Saccheri A B E F → D≠F → Saccheri D C E F.
Proof.
intros A B C D E F HSac HSac2 H.
assert(HPerp := sac__perp1214 _ _ _ _ HSac); assert(HPerp2 := sac__perp1214 _ _ _ _ HSac2).
assert(HPerp3 := sac__perp3414 _ _ _ _ HSac); assert(HPerp4 := sac__perp3414 _ _ _ _ HSac2).
assert(Col A D F) by (apply perp_perp_col with A B; Perp).
assert(Hdiff := sac_distincts _ _ _ _ HSac).
assert(Hdiff2 := sac_distincts _ _ _ _ HSac2).
unfold Saccheri in *; spliter; repeat split.
- apply perp_per_1; auto.
apply perp_col0 with D A; Col; Perp.
- apply perp_per_1; auto.
apply perp_sym, perp_col0 with F A; Col; Perp.
- apply cong_transitivity with A B; Cong.
- apply one_side_transitivity with B.
apply col_one_side with A; Col; Side.
apply invert_one_side, col_one_side with A; Col; Side.
Qed.
This comes from Martin's proof in Theorem 22.10
Lemma three_hypotheses_aux : ∀ 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.
intros A B C D M N A' B' C' D' M' N' HSac HSac' HM HM' HN HN' Hle.
assert(H := A).
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 A C D) by (apply (sac__ncol134 _ B); auto).
assert_diffs.
clear H.
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); assert_cols; Col.
split; auto.
apply (one_side_not_col123 _ _ _ C); Side.
}
assert(Perp A D H G) by (assert_cols; 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 (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); auto.
apply perp_right_comm; apply (perp_col1 _ _ _ N); Col; Perp.
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(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; auto.
apply perp_left_comm.
apply (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 (per_per_col _ _ M); auto.
Perp.
apply (l8_3 A); Col.
}
repeat split; auto.
intro; subst; assert_cols; Col.
apply perp_per_1; auto.
apply perp_left_comm.
apply (perp_col _ M); Col; Perp.
}
assert(Par_strict N D M C).
{ unfold Lambert in HLam1.
spliter.
apply (par_not_col_strict _ _ _ _ C); Col.
apply (l12_9 _ _ _ _ M N); Perp.
intro; apply HNCol1; ColR.
}
assert(Bet N M L).
{ assert(HCong := cong2_lam2__cong N' M' C' D' N L G H).
apply l6_13_1.
2: 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); auto; try ColR.
apply l12_6.
unfold Lambert in HLam2.
spliter.
apply (par_not_col_strict _ _ _ _ G); Col.
apply (l12_9 _ _ _ _ L N); Perp.
apply per_not_col; auto.
}
assert(HNCol4 : ¬ Col N M C) by (unfold Lambert in HLam1; spliter; apply per_not_col; auto).
assert(HNCol5 : ¬ Col N D M) by (apply (par_strict_not_col_1 _ _ _ C); auto).
assert(HK : ∃ K, Col K M C ∧ Bet G K H).
{ elim(eq_dec_points L M).
{ intro.
subst L.
∃ G.
split; Between.
apply col_permutation_5.
unfold Lambert in ×.
spliter.
apply (per_per_col _ _ N); Perp.
}
intro.
assert(HNCol6 : ¬ Col L M C) by (intro; apply HNCol4; ColR).
assert(Hts : TS M C G H).
2: unfold TS in Hts; spliter; auto.
apply (l9_8_2 _ _ L).
- apply l9_2.
apply (l9_8_2 _ _ N).
2: apply l12_6; apply (par_strict_col_par_strict _ _ _ D); Par; ColR.
repeat split; Col.
∃ M; Col.
- apply l12_6.
apply (par_not_col_strict _ _ _ _ L); Col.
unfold Lambert in ×.
spliter.
apply (l12_9 _ _ _ _ M N); Perp.
}
destruct HK as [K []].
assert(HNCol6 : ¬ Col H M C) by (apply (par_not_col N D); Col).
assert(K ≠ H) by (intro; subst K; auto).
assert(Par_strict M N C D).
{ unfold Lambert in ×.
spliter.
apply (par_not_col_strict _ _ _ _ C); Col.
apply (l12_9 _ _ _ _ N D); Perp.
}
assert(HNCol7 : ¬ Col N C D) by (apply (par_strict_not_col_2 M); auto).
assert(Par_strict M N H K).
{ unfold Lambert in ×.
spliter.
apply (par_not_col_strict _ _ _ _ H); Col.
apply (l12_9 _ _ _ _ N D).
Perp.
apply (perp_col _ G); Col; apply (perp_col1 _ _ _ H); Perp; Col.
}
assert(HNCol8 : ¬ 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; auto.
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.
}
assert(HConga := sac__conga A B C D HSac).
assert(CongA A' B' C' H G L).
{ apply (conga_trans _ _ _ M' C' D').
{ apply (out_conga A' B' C' B' C' D'); try (apply out_trivial); try (apply sac__conga); auto.
apply l6_6; apply bet_out; Between.
}
apply conga_right_comm.
apply (cong2_lam2__conga N' _ _ _ N); Cong.
}
assert(HPar : Par C D K H).
{ unfold Lambert in ×.
spliter.
apply (l12_9 _ _ _ _ N D).
Perp.
apply perp_comm; apply (perp_col _ G); Col; apply (perp_col1 _ _ _ A); Perp; Col.
}
assert(Bet M C K → Bet N D H).
{ intro.
elim(eq_dec_points D H).
intro; subst; Between.
intro HDH.
apply between_symmetry.
apply not_out_bet; Col.
intro.
assert(Out C K M).
2: assert(Habs := l6_4_1 K M C); destruct Habs; Between.
apply (col_one_side_out _ D); Col.
apply (one_side_transitivity _ _ _ N).
2: apply l12_6; Par.
apply (one_side_transitivity _ _ _ H).
2: apply invert_one_side; apply out_one_side; Col.
apply l12_6.
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.
2: ColR.
apply perp_left_comm.
apply (perp_col _ G); Perp; ColR.
}
assert(Bet M K C → Bet N H D).
{ intro.
elim(eq_dec_points D H).
intro; subst; Between.
intro HDH.
apply between_symmetry.
apply not_out_bet; Col.
intro.
assert(Out K C M).
2: assert(Habs := l6_4_1 C M K); destruct Habs; Between.
apply (col_one_side_out _ H); Col.
apply (one_side_transitivity _ _ _ N).
2: apply l12_6; Par.
apply (one_side_transitivity _ _ _ D).
2: apply invert_one_side; apply out_one_side; Col.
apply l12_6.
destruct HPar; Par.
exfalso.
unfold Lambert in ×.
spliter.
apply HDH.
apply (l8_18_uniqueness C D N); Col.
Perp.
ColR.
apply (perp_col _ H); auto.
2: ColR.
apply perp_left_comm.
apply (perp_col _ G); Perp; ColR.
}
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 (out_conga A B C D C B); try (apply out_trivial); CongA.
apply l6_6.
apply bet_out; Between.
}
destruct HMout as [_ [_ [HMCK|HMKC]]].
apply (t22_9__per N _ C D); auto.
apply (t22_9__per N _ _ _ C D); auto.
- intro.
apply (l11_17 D C M).
2: apply (out_conga D C B A B C); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
assert(Per H K M).
{ apply l8_2.
apply (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.
- intro.
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 (out_conga A B C D C B); try (apply out_trivial); CongA.
apply l6_6.
apply bet_out; Between.
}
destruct HMout as [_ [_ [HMCK|HMKC]]].
apply (t22_9__acute N _ C D); auto.
apply (t22_9__acute N _ _ _ C D); auto.
- intro.
apply (acute_conga__acute D C M).
2: apply (out_conga D C B A B C); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
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.
Qed.
Saccheri's three hypotheses
Definition hypothesis_of_right_saccheri_quadrilaterals := ∀ A B C D, Saccheri A B C D → Per A B C.
Definition hypothesis_of_acute_saccheri_quadrilaterals := ∀ A B C D, Saccheri A B C D → Acute A B C.
Definition hypothesis_of_obtuse_saccheri_quadrilaterals := ∀ A B C D, Saccheri A B C D → Obtuse A B C.
Lemma per_sac__rah : ∀ A B C D,
Saccheri A B C D → Per A B C → hypothesis_of_right_saccheri_quadrilaterals.
Proof.
intros A B C D HSac HPer A' B' C' D' HSac'.
assert(HM := midpoint_existence B C).
assert(HM' := midpoint_existence B' C').
assert(HN := midpoint_existence A D).
assert(HN' := midpoint_existence A' D').
destruct HM as [M].
destruct HM' as [M'].
destruct HN as [N].
destruct HN' as [N'].
elim(le_cases M N M' N');
intro Hle;
[assert(Haux := three_hypotheses_aux A B C D M N A' B' C' D' M' N')
|assert(Haux := three_hypotheses_aux A' B' C' D' M' N' A B C D M N)];
destruct Haux as [[] _]; auto.
Qed.
Lemma acute_sac__aah : ∀ A B C D,
Saccheri A B C D → Acute A B C → hypothesis_of_acute_saccheri_quadrilaterals.
Proof.
intros A B C D HSac HPer A' B' C' D' HSac'.
assert(HM := midpoint_existence B C).
assert(HM' := midpoint_existence B' C').
assert(HN := midpoint_existence A D).
assert(HN' := midpoint_existence A' D').
destruct HM as [M].
destruct HM' as [M'].
destruct HN as [N].
destruct HN' as [N'].
elim(le_cases M N M' N');
intro Hle;
[assert(Haux := three_hypotheses_aux A B C D M N A' B' C' D' M' N')
|assert(Haux := three_hypotheses_aux A' B' C' D' M' N' A B C D M N)];
destruct Haux as [_ []]; auto.
Qed.
Lemma obtuse_sac__oah : ∀ A B C D,
Saccheri A B C D → Obtuse A B C → hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
intros A B C D HSac HPer A' B' C' D' HSac'.
assert(Hdiff := sac_distincts A B C D HSac).
assert(Hdiff' := sac_distincts A' B' C' D' HSac').
spliter.
elim(angle_partition A' B' C'); auto.
{ intro Hacute'.
exfalso.
apply (nlta A B C).
apply (acute_obtuse__lta); auto.
assert(aah := acute_sac__aah A' B' C' D' HSac' Hacute').
apply (aah _ _ _ D); auto.
}
intro HUn.
destruct HUn as [HPer'|]; auto.
exfalso.
apply (nlta A B C).
apply (obtuse_per__lta); auto.
assert(rah := per_sac__rah A' B' C' D' HSac' HPer').
apply (rah _ _ _ D); auto.
Qed.
Lemma per__ex_saccheri : ∀ A B D, Per B A D → A ≠ B → A ≠ D →
∃ C, Saccheri A B C D.
Proof.
intros A B D HPer HAB HBD.
assert (HNCol : ¬ Col B A D) by (apply per_not_col; auto).
destruct (l10_15 A D D B) as [C0 []]; Col.
assert(¬ Col A D C0) by (apply (one_side_not_col123 _ _ _ B); Side).
assert_diffs.
destruct (segment_construction_3 D C0 A B) as [C []]; auto.
∃ C.
repeat split; Cong.
apply (per_col _ _ C0); Col; Perp.
apply invert_one_side; apply (out_out_one_side _ _ _ C0); Side.
Qed.
Lemma ex_saccheri : ∃ A B C D, Saccheri A B C D.
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.
∃ A; ∃ B; ∃ C; ∃ D; trivial.
Qed.
Lemma ex_lambert : ∃ A B C D, Lambert A B C D.
Proof.
destruct ex_saccheri as [D [C [C' [D' HSac]]]].
destruct (midpoint_existence D D') as [A HA].
destruct (midpoint_existence C C') as [B HB].
∃ A, B, C, D.
apply mid2_sac__lam6521 with C' D'; trivial.
Qed.
Lemma saccheri_s_three_hypotheses :
hypothesis_of_acute_saccheri_quadrilaterals ∨ hypothesis_of_right_saccheri_quadrilaterals ∨ hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
destruct ex_saccheri as [A [B [C [D HSac]]]].
assert(Hdiff := sac_distincts A B C D HSac).
spliter.
elim(angle_partition A B C); auto; [|intro HUn; destruct HUn].
intro; left; apply (acute_sac__aah A B C D); trivial.
right; left; apply (per_sac__rah A B C D); trivial.
right; right; apply (obtuse_sac__oah A B C D); trivial.
Qed.
Lemma not_aah :
hypothesis_of_right_saccheri_quadrilaterals ∨ hypothesis_of_obtuse_saccheri_quadrilaterals → ¬ hypothesis_of_acute_saccheri_quadrilaterals.
Proof.
intros HUn aah.
destruct ex_saccheri as [A [B [C [D HSac]]]].
assert(Hdiff := sac_distincts A B C D HSac).
spliter.
apply (nlta A B C).
assert(Acute A B C) by (apply (aah _ _ _ D); auto).
destruct HUn as [rah|oah].
- apply (acute_per__lta); auto.
apply (rah _ _ _ D); auto.
- apply (acute_obtuse__lta); auto.
apply (oah _ _ _ D); auto.
Qed.
Lemma not_rah :
hypothesis_of_acute_saccheri_quadrilaterals ∨ hypothesis_of_obtuse_saccheri_quadrilaterals → ¬ hypothesis_of_right_saccheri_quadrilaterals.
Proof.
intros HUn rah.
destruct ex_saccheri as [A [B [C [D HSac]]]].
assert(Hdiff := sac_distincts A B C D HSac).
spliter.
apply (nlta A B C).
assert(Per A B C) by (apply (rah _ _ _ D); auto).
destruct HUn as [aah|oah].
- apply (acute_per__lta); auto.
apply (aah _ _ _ D); auto.
- apply (obtuse_per__lta); auto.
apply (oah _ _ _ D); auto.
Qed.
Lemma not_oah :
hypothesis_of_acute_saccheri_quadrilaterals ∨ hypothesis_of_right_saccheri_quadrilaterals → ¬ hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
intros HUn oah.
destruct ex_saccheri as [A [B [C [D HSac]]]].
assert(Hdiff := sac_distincts A B C D HSac).
spliter.
apply (nlta A B C).
assert(Obtuse A B C) by (apply (oah _ _ _ D); auto).
destruct HUn as [aah|rah].
- apply (acute_obtuse__lta); auto.
apply (aah _ _ _ D); auto.
- apply (obtuse_per__lta); auto.
apply (rah _ _ _ D); auto.
Qed.
Lemma lam_per__rah : ∀ A B C D,
Lambert A B C D → (Per B C D ↔ hypothesis_of_right_saccheri_quadrilaterals).
Proof.
intros A B C D HLam.
assert(HC' := symmetric_point_construction C B).
destruct HC' as [C'].
assert(HD' := symmetric_point_construction D A).
destruct HD' as [D'].
split.
- intro.
apply (per_sac__rah D C C' D').
apply (lam6521_mid2__sac _ _ _ _ B A); auto.
unfold Lambert in HLam.
spliter.
apply l8_2.
apply (l8_3 B); Col.
- intro rah.
apply (l8_3 C'); Col.
2: unfold Lambert in HLam; spliter; assert_diffs; auto.
apply l8_2.
apply (rah _ _ _ D').
apply (lam6521_mid2__sac _ _ _ _ B A); auto.
Qed.
Lemma lam_acute__aah : ∀ A B C D,
Lambert A B C D → (Acute B C D ↔ hypothesis_of_acute_saccheri_quadrilaterals).
Proof.
intros A B C D HLam.
assert(HC' := symmetric_point_construction C B).
destruct HC' as [C'].
assert(HD' := symmetric_point_construction D A).
destruct HD' as [D'].
split.
- intro.
apply (acute_sac__aah D C C' D').
apply (lam6521_mid2__sac _ _ _ _ B A); auto.
unfold Lambert in HLam.
spliter.
assert_diffs.
apply (acute_conga__acute B C D); auto.
apply (out_conga B C D D C B); try (apply out_trivial); CongA.
apply bet_out; Between.
- intro aah.
apply (acute_conga__acute D C C'); auto.
apply (aah _ _ _ D'); apply (lam6521_mid2__sac _ _ _ _ B A); auto.
unfold Lambert in HLam.
spliter.
assert_diffs.
apply (out_conga D C B B C D); try (apply out_trivial); CongA.
apply bet_out; Between.
Qed.
Lemma lam_obtuse__oah : ∀ A B C D,
Lambert A B C D → (Obtuse B C D ↔ hypothesis_of_obtuse_saccheri_quadrilaterals).
Proof.
intros A B C D HLam.
assert(HC' := symmetric_point_construction C B).
destruct HC' as [C'].
assert(HD' := symmetric_point_construction D A).
destruct HD' as [D'].
split.
- intro.
apply (obtuse_sac__oah D C C' D').
apply (lam6521_mid2__sac _ _ _ _ B A); auto.
unfold Lambert in HLam.
spliter.
assert_diffs.
apply (obtuse_conga__obtuse B C D); auto.
apply (out_conga B C D D C B); try (apply out_trivial); CongA.
apply bet_out; Between.
- intro oah.
apply (obtuse_conga__obtuse D C C'); auto.
apply (oah _ _ _ D'); apply (lam6521_mid2__sac _ _ _ _ B A); auto.
unfold Lambert in HLam.
spliter.
assert_diffs.
apply (out_conga D C B B C D); try (apply out_trivial); CongA.
apply bet_out; Between.
Qed.
Lemma t22_11__per : ∀ A B C D,
Saccheri A B C D → (CongA A B D B D C ↔ Per A B C).
Proof.
intros A B C D HSac.
split.
- intro.
apply (cong_sac__per _ _ _ D); auto.
unfold Saccheri in HSac.
spliter.
assert(HSAS := l11_49 A B D C D B).
destruct HSAS; Cong; CongA.
- intro HPer.
apply <- (cong_sac__per A B C D) in HPer; trivial.
assert(Hdiff := sac_distincts A B C D HSac).
unfold Saccheri in HSac.
spliter.
assert(HSSS := l11_51 A B D C D B).
destruct HSSS as [_ []]; Cong; CongA.
Qed.
Lemma t22_11__acute : ∀ A B C D,
Saccheri A B C D → (LtA A B D B D C ↔ Acute A B C).
Proof.
intros A B C D HSac.
split.
- intro.
apply (lt_sac__acute _ _ _ D); auto.
unfold Saccheri in HSac.
spliter.
apply lt_right_comm.
apply (t18_18 D _ _ B); Cong.
apply lta_left_comm; auto.
- intro Hacute.
apply <- (lt_sac__acute A B C D) in Hacute; trivial.
assert(Hdiff := sac_distincts A B C D HSac).
unfold Saccheri in HSac.
spliter.
apply lta_left_comm.
apply t18_19; Cong.
apply lt_right_comm; Cong.
Qed.
Lemma t22_11__obtuse : ∀ A B C D,
Saccheri A B C D → (LtA B D C A B D ↔ Obtuse A B C).
Proof.
intros A B C D HSac.
split.
- intro.
apply (lt_sac__obtuse _ _ _ D); auto.
unfold Saccheri in HSac.
spliter.
apply lt_right_comm.
apply (t18_18 B _ _ D); Cong.
apply lta_left_comm; auto.
- intro Hobtuse.
apply <- (lt_sac__obtuse A B C D) in Hobtuse; trivial.
assert(Hdiff := sac_distincts A B C D HSac).
unfold Saccheri in HSac.
spliter.
apply lta_left_comm.
apply t18_19; Cong.
apply lt_right_comm; Cong.
Qed.
Lemma t22_12__rah : ∀ A B C,
A ≠ B → B ≠ C → Per A B C →
(SumA B C A C A B A B C ↔ hypothesis_of_right_saccheri_quadrilaterals).
Proof.
intros A B C HAB HBC HPer.
assert(¬ Col A B C) by (apply per_not_col; auto).
assert(HD0 := l10_15 B C C A).
destruct HD0 as [D0 []]; Col.
assert_diffs.
assert(HD := segment_construction_3 C D0 A B).
destruct HD as [D []]; auto.
assert(HSac : Saccheri B A D C).
{ repeat split; Cong.
apply (per_col _ _ D0); Col; Perp.
apply invert_one_side.
apply (out_out_one_side _ _ _ D0); Side.
}
clear dependent D0.
assert_diffs.
assert(HPars1 := sac__par_strict1423 B A D C HSac).
assert(HPars2 : Par_strict A B C D).
{ unfold Saccheri in HSac.
spliter.
apply (par_not_col_strict _ _ _ _ C); Col.
apply (l12_9 _ _ _ _ B C); Perp.
}
assert(TS C A B D) by (apply l9_31; apply l12_6; Par).
assert(CongA B C D A B C) by (unfold Saccheri in HSac; spliter; apply l11_16; auto).
split.
- intro.
apply (per_sac__rah B A D C); auto.
apply (t22_11__per _ _ _ C); auto.
apply conga_left_comm.
unfold Saccheri in HSac.
spliter.
apply (sams2_suma2__conga456 B C A _ _ _ _ _ _ A B C); try (apply sams123231); auto.
{ repeat split; auto.
right; intro; assert_cols; Col.
∃ D.
split; CongA; split; Side.
}
∃ D.
repeat (split; CongA); Side.
- intro rah.
apply (conga3_suma__suma B C A A C D B C D); try (apply conga_refl); auto.
∃ D; repeat (split; CongA); Side.
apply conga_sym.
apply conga_left_comm.
apply t22_11__per; auto.
apply (rah _ _ _ C); auto.
Qed.
Lemma t22_12__aah : ∀ A B C P Q R,
Per A B C → SumA B C A C A B P Q R →
(Acute P Q R ↔ hypothesis_of_acute_saccheri_quadrilaterals).
Proof.
intros A B C P Q R HPer HSuma.
suma.assert_diffs.
assert(¬ Col A B C) by (apply per_not_col; auto).
assert(HD0 := l10_15 B C C A).
destruct HD0 as [D0 []]; Col.
assert_diffs.
assert(HD := segment_construction_3 C D0 A B).
destruct HD as [D []]; auto.
assert(HSac : Saccheri B A D C).
{ repeat split; Cong.
apply (per_col _ _ D0); Col; Perp.
apply invert_one_side.
apply (out_out_one_side _ _ _ D0); Side.
}
clear dependent D0.
assert_diffs.
assert(HPars1 := sac__par_strict1423 B A D C HSac).
assert(HPars2 : Par_strict A B C D).
{ unfold Saccheri in HSac.
spliter.
apply (par_not_col_strict _ _ _ _ C); Col.
apply (l12_9 _ _ _ _ B C); Perp.
}
assert(TS C A B D) by (apply l9_31; apply l12_6; Par).
assert(CongA B C D A B C) by (unfold Saccheri in HSac; spliter; apply l11_16; auto).
split.
- intro.
apply (acute_sac__aah B A D C); auto.
apply (t22_11__acute _ _ _ C); auto.
unfold Saccheri in HSac.
spliter.
apply lta_left_comm.
apply (sams_lea_lta789_suma2__lta456 B C A _ _ _ P Q R B C A _ _ _ B C D); auto.
apply lea_refl; auto.
apply acute_per__lta; auto.
SumA.
∃ D; repeat (split; CongA); Side.
- intro aah.
∃ B.
∃ C.
∃ D.
split.
unfold Saccheri in HSac; spliter; auto.
apply (sams_lea_lta456_suma2__lta B C A C A B _ _ _ B C A A C D); auto.
apply lea_refl; auto.
apply lta_left_comm; apply t22_11__acute; try (apply (aah _ _ _ C)); auto.
2: ∃ D; repeat (split; CongA); Side.
split; auto; split.
right; intro; assert_cols; Col.
∃ D; split; CongA.
split; eauto with side.
Qed.
Lemma t22_12__oah : ∀ A B C P Q R,
Per A B C → SumA B C A C A B P Q R →
(Obtuse P Q R ↔ hypothesis_of_obtuse_saccheri_quadrilaterals).
Proof.
intros A B C P Q R HPer HSuma.
suma.assert_diffs.
assert(¬ Col A B C) by (apply per_not_col; auto).
assert(HD0 := l10_15 B C C A).
destruct HD0 as [D0 []]; Col.
assert_diffs.
assert(HD := segment_construction_3 C D0 A B).
destruct HD as [D []]; auto.
assert(HSac : Saccheri B A D C).
{ repeat split; Cong.
apply (per_col _ _ D0); Col; Perp.
apply invert_one_side.
apply (out_out_one_side _ _ _ D0); Side.
}
clear dependent D0.
assert_diffs.
assert(HPars1 := sac__par_strict1423 B A D C HSac).
assert(HPars2 : Par_strict A B C D).
{ unfold Saccheri in HSac.
spliter.
apply (par_not_col_strict _ _ _ _ C); Col.
apply (l12_9 _ _ _ _ B C); Perp.
}
assert(TS C A B D) by (apply l9_31; apply l12_6; Par).
assert(CongA B C D A B C) by (unfold Saccheri in HSac; spliter; apply l11_16; auto).
split.
- intro.
apply (obtuse_sac__oah B A D C); auto.
apply (t22_11__obtuse _ _ _ C); auto.
unfold Saccheri in HSac.
spliter.
apply lta_right_comm.
apply (sams_lea_lta789_suma2__lta456 B C A _ _ _ B C D B C A _ _ _ P Q R); auto.
apply lea_refl; auto.
apply obtuse_per__lta; auto.
2: ∃ D; repeat (split; CongA); Side.
split; auto; split.
right; intro; assert_cols; Col.
∃ D; split; CongA.
split; Side.
- intro oah.
∃ B.
∃ C.
∃ D.
split.
unfold Saccheri in HSac; spliter; auto.
apply (sams_lea_lta456_suma2__lta B C A A C D _ _ _ B C A C A B); auto.
apply lea_refl; auto.
apply lta_right_comm; apply t22_11__obtuse; try (apply (oah _ _ _ C)); auto.
SumA.
∃ D; repeat (split; CongA); Side.
Qed.
Lemma t22_14__bet_aux : ∀ A B C P Q R,
hypothesis_of_right_saccheri_quadrilaterals →
¬ Col A B C → TriSumA A B C P Q R → Acute A B C → Acute A C B → Bet P Q R.
Proof.
intros A B C P Q R rah HNCol HTri HacuteB HacuteC.
apply trisuma_perm_312 in HTri.
destruct HTri as [D [E [F []]]].
assert(HA' := l8_18_existence B C A).
destruct HA' as [A' []]; Col.
assert(Out B A' C) by (apply (acute_col_perp__out A); auto).
assert(Out C A' B) by (apply (acute_col_perp__out A); Col; Perp).
assert(Bet B A' C) by (apply (out2__bet); [|apply l6_6]; auto).
assert_diffs.
assert(Per B A' A) by (apply perp_per_1; auto; apply perp_left_comm; apply (perp_col _ C); Col).
assert(Per C A' A) by (apply (l8_3 B); Col).
assert(CongA B A' A C A' A) by (apply l11_16; auto).
assert(CongA A B C A B A') by (apply (out_conga A B A' A B A'); try (apply out_trivial); CongA).
assert(CongA B C A A' C A) by (apply (out_conga A' C A A' C A); try (apply out_trivial); CongA).
assert(¬ Col B A A') by (intro; apply HNCol; ColR).
assert(¬ Col C A A') by (intro; apply HNCol; ColR).
assert(TS A A' B C) by (repeat split; try (∃ A'); Col).
apply (bet_conga_bet B A' C); auto.
apply (suma2__conga D E F B C A); auto.
apply (suma_assoc B A' A C A A' _ _ _ _ _ _ _ _ _ A A' C).
apply (conga2_sams__sams C A' A A' A C); try (apply sams123231); CongA.
apply (conga2_sams__sams A' A C A C A'); try (apply sams123231); CongA.
2: apply (conga3_suma__suma A' A C A C A' C A' A); try (apply t22_12__rah); CongA.
2: ∃ C; repeat (split; CongA); Side.
apply suma_sym.
apply (suma_assoc _ _ _ A' A B A B C _ _ _ C A B); auto.
split; auto; split;
[right; intro; assert_cols|
∃ B; split; CongA; split; Side; apply l9_9_bis; apply (out_one_side)]; Col.
apply (conga2_sams__sams A' A B A B A'); try (apply sams123231); CongA.
∃ B; repeat (split; CongA); Side.
apply (conga3_suma__suma A' A B A B A' B A' A); try (apply t22_12__rah); CongA.
Qed.
Under the right angle hypothesis,
the sum of the three angles of a triangle is equal to 180
Lemma t22_14__bet :
hypothesis_of_right_saccheri_quadrilaterals →
∀ A B C P Q R, TriSumA A B C P Q R → Bet P Q R.
Proof.
intros rah A B C P Q R HTri.
elim(Col_dec A B C).
intro; apply (col_trisuma__bet A B C); auto.
intro.
assert_diffs.
elim(angle_partition A B C); auto.
intro; elim(angle_partition A C B); auto.
- intro.
apply (t22_14__bet_aux A B C); auto.
- intro.
assert(HInter := l11_43 C A B).
destruct HInter; Col.
apply (t22_14__bet_aux C A B); Col.
apply trisuma_perm_312; auto.
- intro.
assert(HInter := l11_43 B A C).
destruct HInter; Col.
apply (t22_14__bet_aux B A C); Col.
apply trisuma_perm_213; auto.
Qed.
Lemma t22_14__sams_nbet_aux : ∀ A B C D E F P Q R,
hypothesis_of_acute_saccheri_quadrilaterals →
¬ Col A B C →
SumA C A B A B C D E F → SumA D E F B C A P Q R →
Acute A B C → Acute A C B →
SAMS D E F B C A ∧ ¬ Bet P Q R.
Proof.
intros A B C D E F P Q R aah HNCol HSuma1 HSuma2 HacuteB HacuteC.
assert(H := A).
assert(HA' := l8_18_existence B C A).
destruct HA' as [A' []]; Col.
assert(Out B A' C) by (apply (acute_col_perp__out A); auto).
assert(Out C A' B) by (apply (acute_col_perp__out A); Col; Perp).
assert(Bet B A' C) by (apply (out2__bet); [|apply l6_6]; auto).
assert_diffs.
assert(Per B A' A) by (apply perp_per_1; auto; apply perp_left_comm; apply (perp_col _ C); Col).
assert(Per C A' A) by (apply (l8_3 B); Col).
assert(CongA B A' A C A' A) by (apply l11_16; auto).
assert(CongA A B C A B A') by (apply (out_conga A B A' A B A'); try (apply out_trivial); CongA).
assert(CongA B C A A' C A) by (apply (out_conga A' C A A' C A); try (apply out_trivial); CongA).
assert(¬ Col B A A') by (intro; apply HNCol; ColR).
assert(¬ Col C A A') by (intro; apply HNCol; ColR).
assert(TS A A' B C) by (repeat split; try (∃ A'); Col).
assert(HSuma3 := ex_suma B A' A C A A').
clear H.
destruct HSuma3 as [G [H [I HSuma3]]]; auto.
suma.assert_diffs.
assert(LtA D E F G H I).
{ assert(HSuma4 := ex_suma A' A B A B C).
destruct HSuma4 as [V [W [X HSuma4]]]; auto.
suma.assert_diffs.
apply (sams_lea_lta456_suma2__lta C A A' V W X _ _ _ C A A' B A' A); Lea.
apply (acute_per__lta); auto; apply (t22_12__aah B A' A); auto; apply (conga3_suma__suma A' A B A B C V W X); CongA.
apply (conga2_sams__sams C A A' A A' C); SumA; CongA.
2: apply suma_sym; auto.
apply (suma_assoc _ _ _ A' A B A B C _ _ _ C A B); auto.
split; auto; split;
[right; intro; assert_cols|
∃ B; split; CongA; split; Side; apply l9_9_bis; apply (out_one_side)]; Col.
apply (conga2_sams__sams A' A B A B A'); SumA; CongA.
∃ B; repeat (split; CongA); Side.
}
assert(HSuma4 := ex_suma C A A' B C A).
destruct HSuma4 as [J [K [L HSuma4]]]; auto.
suma.assert_diffs.
assert(LtA J K L A A' C).
apply (acute_per__lta); Perp; apply (t22_12__aah C A' A); auto; apply (conga3_suma__suma C A A' B C A J K L); CongA.
assert(SAMS G H I B C A).
{ apply (sams_assoc B A' A C A A' _ _ _ _ _ _ J K L); auto.
apply (conga2_sams__sams C A' A A' A C); SumA; CongA.
apply (conga2_sams__sams A' A C A C A'); SumA; CongA.
apply (sams_chara _ _ _ _ _ _ C); Lea.
}
assert(HSuma5 := ex_suma G H I B C A).
destruct HSuma5 as [S [T [U HSuma5]]]; auto.
suma.assert_diffs.
assert(LtA S T U B A' C).
{ apply (sams_lea_lta456_suma2__lta B A' A J K L _ _ _ B A' A A A' C); Lea.
apply (sams_chara _ _ _ _ _ _ C); Lea.
2: ∃ C; repeat(split; CongA); Side.
apply (suma_assoc _ _ _ C A A' B C A _ _ _ G H I); auto;
[apply (conga2_sams__sams C A' A A' A C)|apply (conga2_sams__sams A' A C A C A')];
SumA; CongA.
}
split.
apply (sams_lea2__sams _ _ _ _ _ _ G H I B C A); Lea.
intro.
apply (nlta P Q R).
apply (conga_preserves_lta P Q R B A' C).
apply conga_refl; auto.
apply conga_line; auto.
apply (lta_trans _ _ _ S T U); auto.
apply (sams_lea_lta123_suma2__lta D E F B C A _ _ _ G H I B C A); Lea.
Qed.
Under the Acute angle hypothesis,
the sum of the three angles of a triangle is less than 180
Lemma t22_14__sams_nbet :
hypothesis_of_acute_saccheri_quadrilaterals →
∀ A B C D E F P Q R, ¬ Col A B C →
SumA C A B A B C D E F → SumA D E F B C A P Q R →
SAMS D E F B C A ∧ ¬ Bet P Q R.
Proof.
intros aah A B C D E F P Q R HNCol HSuma1 HSuma2.
assert(H := A).
assert_diffs.
elim(angle_partition A B C); auto.
intro; elim(angle_partition A C B); auto.
- intro.
apply (t22_14__sams_nbet_aux A B C); auto.
- intro.
assert(HInter := l11_43 C A B).
destruct HInter; Col.
assert(HSuma3 := ex_suma B C A C A B).
clear H.
destruct HSuma3 as [G [H [I HSuma3]]]; auto.
suma.assert_diffs.
assert(HInter := t22_14__sams_nbet_aux C A B G H I P Q R).
destruct HInter as [HIsi HNBet]; Col.
apply (suma_assoc B C A C A B _ _ _ _ _ _ _ _ _ D E F); SumA.
split; auto.
apply sams_sym; apply (sams_assoc _ _ _ C A B A B C G H I); SumA.
- intro.
assert (HInter := l11_43 B A C).
destruct HInter; Col.
assert(HInter := t22_14__sams_nbet_aux B A C D E F P Q R).
destruct HInter as [HIsi HNBet]; Col; SumA.
Qed.
Lemma t22_14__nsams_aux : ∀ A B C D E F,
hypothesis_of_obtuse_saccheri_quadrilaterals →
¬ Col A B C →
SumA C A B A B C D E F → Acute A B C → Acute A C B →
¬ SAMS D E F B C A.
Proof.
intros A B C D E F oah HNCol HSuma1 HacuteB HacuteC HIsi.
assert(HA' := l8_18_existence B C A).
destruct HA' as [A' []]; Col.
assert(Out B A' C) by (apply (acute_col_perp__out A); auto).
assert(Out C A' B) by (apply (acute_col_perp__out A); Col; Perp).
assert(Bet B A' C) by (apply (out2__bet); [|apply l6_6]; auto).
assert_diffs.
assert(Per B A' A) by (apply perp_per_1; auto; apply perp_left_comm; apply (perp_col _ C); Col).
assert(Per C A' A) by (apply (l8_3 B); Col).
assert(CongA B A' A C A' A) by (apply l11_16; auto).
assert(CongA A B C A B A') by (apply (out_conga A B A' A B A'); try (apply out_trivial); CongA).
assert(CongA B C A A' C A) by (apply (out_conga A' C A A' C A); try (apply out_trivial); CongA).
assert(¬ Col B A A') by (intro; apply HNCol; ColR).
assert(¬ Col C A A') by (intro; apply HNCol; ColR).
assert(TS A A' B C) by (repeat split; try (∃ A'); Col).
assert(HSuma2 := ex_suma D E F B C A).
destruct HSuma2 as [P [Q [R HSuma2]]]; suma.assert_diffs; auto.
absurd (LtA B A' C P Q R).
apply (lea__nlta); apply l11_31_2; auto.
assert(HSuma3 := ex_suma B A' A C A A').
clear H.
destruct HSuma3 as [G [H [I HSuma3]]]; auto.
assert(LtA G H I D E F).
{ assert(HSuma4 := ex_suma A' A B A B C).
destruct HSuma4 as [V [W [X HSuma4]]]; auto.
suma.assert_diffs.
assert(SAMS C A A' A' A B).
{ split; auto; split.
right; intro; assert_cols; Col.
∃ B.
repeat (split; CongA); Side.
apply l9_9_bis; apply out_one_side; Col.
}
assert(SAMS A' A B A B C) by (apply (conga2_sams__sams A' A B A B A'); SumA; CongA).
assert(SumA C A A' A' A B C A B) by (∃ B; repeat (split; CongA); Side).
apply (sams_lea_lta456_suma2__lta C A A' B A' A _ _ _ C A A' V W X); Lea.
apply (obtuse_per__lta); auto; apply (t22_12__oah B A' A); auto; apply (conga3_suma__suma A' A B A B C V W X); CongA.
apply (sams_assoc _ _ _ A' A B A B C C A B); SumA.
SumA.
apply (suma_assoc _ _ _ A' A B A B C _ _ _ C A B); auto.
}
assert(HSuma4 := ex_suma C A A' B C A).
destruct HSuma4 as [J [K [L HSuma4]]]; auto.
suma.assert_diffs.
assert(LtA A A' C J K L).
apply (obtuse_per__lta); Perp; apply (t22_12__oah C A' A); auto; apply (conga3_suma__suma C A A' B C A J K L); CongA.
assert(HSuma5 := ex_suma B A' A J K L).
destruct HSuma5 as [S [T [U HSuma5]]]; auto.
suma.assert_diffs.
apply (lta_trans _ _ _ S T U).
- apply (sams_lea_lta456_suma2__lta B A' A A A' C _ _ _ B A' A J K L); Lea.
2: ∃ C; repeat (split; CongA); Side.
apply (sams_assoc _ _ _ C A A' B C A G H I); auto.
apply (conga2_sams__sams C A' A C A A'); SumA; CongA.
apply (conga2_sams__sams C A A' A' C A); SumA; CongA.
apply (sams_lea2__sams _ _ _ _ _ _ D E F B C A); Lea.
- apply (sams_lea_lta123_suma2__lta G H I B C A _ _ _ D E F B C A); Lea.
apply (suma_assoc B A' A C A A' _ _ _ _ _ _ _ _ _ J K L); auto.
apply (conga2_sams__sams C A' A C A A'); SumA; CongA.
apply (conga2_sams__sams C A A' A' C A); SumA; CongA.
Qed.
Under the Obtuse angle hypothesis,
the sum of the three angles of a triangle is greater than 180
Lemma t22_14__nsams :
hypothesis_of_obtuse_saccheri_quadrilaterals →
∀ A B C D E F, ¬ Col A B C →
SumA C A B A B C D E F →
¬ SAMS D E F B C A.
Proof.
intros oah A B C D E F HNCol HSuma1.
assert(H := A).
assert_diffs.
elim(angle_partition A B C); auto.
intro; elim(angle_partition A C B); auto.
- intro.
apply (t22_14__nsams_aux A B C); auto.
- intro.
assert(HInter := l11_43 C A B).
destruct HInter; Col.
assert(HSuma3 := ex_suma B C A C A B).
clear H.
destruct HSuma3 as [G [H [I HSuma3]]]; auto.
suma.assert_diffs.
assert(HNIsi := t22_14__nsams_aux C A B G H I).
intro HIsi.
absurd(SAMS G H I A B C).
apply HNIsi; Col.
apply (sams_assoc B C A C A B _ _ _ _ _ _ D E F); SumA.
- intro.
assert (HInter := l11_43 B A C).
destruct HInter; Col.
intro.
absurd(SAMS D E F A C B).
apply (t22_14__nsams_aux B A C D E F); Col; SumA.
SumA.
Qed.
If the sum of the angles of a not-degenerate triangle is equal to 180,
then the right angle hypothesis holds
Lemma t22_14__rah : ∀ A B C P Q R,
¬ Col A B C → TriSumA A B C P Q R → Bet P Q R → hypothesis_of_right_saccheri_quadrilaterals.
Proof.
intros A B C P Q R HNCol HTri HBet.
apply trisuma_perm_312 in HTri.
elim(saccheri_s_three_hypotheses).
2: intro HUn; destruct HUn as [|oah]; auto.
- intro aah.
exfalso.
destruct HTri as [D [E [F []]]].
assert(HInter := t22_14__sams_nbet aah A B C D E F P Q R).
destruct HInter; auto.
- exfalso.
destruct HTri as [D [E [F [HSuma1 HSuma2]]]].
apply (t22_14__nsams oah A B C D E F); auto.
destruct HSuma2 as [G [HConga1 [HNos HConga2]]].
apply conga_sym in HConga1.
assert_diffs.
apply (sams_chara _ _ _ _ _ _ G); Lea.
apply (bet_conga_bet P Q R); CongA.
Qed.
If the sum of the angles of a triangle is less than 180,
then the Acute angle hypothesis holds
Lemma t22_14__aah : ∀ A B C D E F P Q R,
SumA C A B A B C D E F → SumA D E F B C A P Q R →
SAMS D E F B C A →
¬ Bet P Q R →
hypothesis_of_acute_saccheri_quadrilaterals.
Proof.
intros A B C D E F P Q R HSuma1 HSuma2 HIsi HNBet.
elim(saccheri_s_three_hypotheses); auto.
intro HUn.
exfalso.
destruct HUn as [rah|oah].
2: elim(Col_dec A B C).
- apply HNBet.
apply (t22_14__bet rah A B C).
apply trisuma_perm_231.
∃ D; ∃ E; ∃ F.
split; auto.
- intro.
apply HNBet.
apply (col_trisuma__bet C A B); Col.
∃ D; ∃ E; ∃ F.
split; auto.
- intro.
absurd(SAMS D E F B C A); auto.
apply t22_14__nsams; auto.
Qed.
If the sum of the angles of a triangle is greater than 180,
then the Obtuse angle hypothesis holds
Lemma t22_14__oah : ∀ A B C D E F,
SumA C A B A B C D E F → ¬ SAMS D E F B C A → hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
intros A B C D E F HSuma1 HNIsi.
elim(Col_dec A B C).
{ intro HCol.
exfalso.
apply HNIsi.
suma.assert_diffs.
elim(bet_dec A B C).
- intro.
apply (conga2_sams__sams A B C B C A); try (apply conga_refl); SumA.
apply (out213_suma__conga C A B); auto.
apply l6_6; apply bet_out; auto.
- intro.
apply (conga2_sams__sams C A B B C A); try (apply conga_refl); SumA.
apply (out546_suma__conga _ _ _ A B C); auto.
apply not_bet_out; auto.
}
intro HNCol.
elim(saccheri_s_three_hypotheses).
2: intro HUn; destruct HUn as [rah|]; auto.
- intro aah.
exfalso.
suma.assert_diffs.
assert(HSuma2 := ex_suma D E F B C A).
destruct HSuma2 as [P [Q [R HSuma2]]]; auto.
assert(HInter := t22_14__sams_nbet aah A B C D E F P Q R).
destruct HInter; auto.
- exfalso.
suma.assert_diffs.
apply HNIsi.
assert(¬ Col D E F) by (apply (ncol_suma__ncol C A B); Col).
assert(HD' := ex_conga_ts B C A F E D).
destruct HD' as [D' []]; Col.
suma.assert_diffs.
apply (sams_chara _ _ _ _ _ _ D'); Lea.
apply (t22_14__bet rah C A B).
∃ D; ∃ E; ∃ F.
split; auto.
∃ D'; repeat (split; CongA); Side.
Qed.
If C is on the circle of diameter AB, then we have the angles equation A + B = C
Lemma cong_mid__suma : ∀ A B C M,
¬ Col A B C →
Midpoint M A B → Cong M A M C →
SumA C A B A B C A C B.
Proof.
intros A B C M HNCol HM HCong.
assert_diffs.
assert(CongA A B C M C B).
{ apply (out_conga M B C M C B); try (apply out_trivial); auto.
2: apply bet_out; Between.
apply l11_44_1_a.
intro; apply HNCol; ColR.
apply (cong_transitivity _ _ M A); eCong.
}
assert(CongA B A C M C A).
{ apply (out_conga M A C M C A); try (apply out_trivial); auto.
2: apply bet_out; Between.
apply l11_44_1_a; Cong.
intro; apply HNCol; ColR.
}
apply (conga3_suma__suma A C M M C B A C B); CongA.
∃ B.
repeat (split; CongA).
apply l9_9.
repeat split; auto; try (intro; apply HNCol; ColR).
∃ M.
split; Col; Between.
Qed.
The three following lemmas link Saccheri's three hypotheses
with triangles A B C having C on the circle of diameter AB;
the first one states the equivalence between the right angle hypothesis and Thales' theorem
Lemma t22_17__rah : ∀ A B C M,
¬ Col A B C →
Midpoint M A B → Cong M A M C →
(Per A C B ↔ hypothesis_of_right_saccheri_quadrilaterals).
Proof.
intros A B C M HNCol HM HCong.
assert_diffs.
assert(SumA C A B A B C A C B) by (apply (cong_mid__suma _ _ _ M); auto).
assert(HSuma := ex_suma A C B B C A).
destruct HSuma as [P [Q [R]]]; auto.
split.
- intro.
apply (t22_14__rah C A B P Q R); Col.
∃ A; ∃ C; ∃ B; auto.
apply (per2_suma__bet A C B B C A); Perp.
- intro rah.
apply (bet_suma__per _ _ _ P Q R); SumA.
apply (t22_14__bet rah C A B).
∃ A; ∃ C; ∃ B; auto.
Qed.
Lemma t22_17__oah : ∀ A B C M,
¬ Col A B C →
Midpoint M A B → Cong M A M C →
(Obtuse A C B ↔ hypothesis_of_obtuse_saccheri_quadrilaterals).
Proof.
intros A B C M HNCol HM HCong.
assert_diffs.
assert(SumA C A B A B C A C B) by (apply (cong_mid__suma _ _ _ M); auto).
assert(HSuma := ex_suma A C B B C A).
destruct HSuma as [P [Q [R]]]; auto.
split.
- intro.
apply (t22_14__oah A B C B C A); Col; SumA.
apply obtuse__nsams; apply obtuse_sym; auto.
- intro oah.
apply obtuse_sym.
apply nsams__obtuse; auto.
apply (t22_14__nsams oah A B C); Col; SumA.
Qed.
Lemma t22_17__aah : ∀ A B C M,
¬ Col A B C →
Midpoint M A B → Cong M A M C →
(Acute A C B ↔ hypothesis_of_acute_saccheri_quadrilaterals).
Proof.
intros A B C M HNCol HM HCong.
assert_diffs.
split.
- intro.
elim(saccheri_s_three_hypotheses); auto.
intro HUn.
exfalso.
apply (nlta A C B).
destruct HUn as [rah|oah].
apply (acute_per__lta); auto; rewrite (t22_17__rah _ _ _ M); auto.
apply (acute_obtuse__lta); auto; rewrite (t22_17__oah _ _ _ M); auto.
- intro.
elim(angle_partition A C B); auto.
intro HUn.
absurd(hypothesis_of_acute_saccheri_quadrilaterals); auto.
apply not_aah.
destruct HUn.
left; apply (t22_17__rah A B C M); auto.
right; apply (t22_17__oah A B C M); auto.
Qed.
Lemma t22_20 : ¬ hypothesis_of_obtuse_saccheri_quadrilaterals →
∀ A B C D E F, SumA A B C B C A D E F → SAMS D E F C A B.
Proof.
intros noah A B C D E F HS.
elim(sams_dec D E F C A B); trivial.
intro HNI; exfalso.
apply noah, (t22_14__oah B C A D E F); trivial.
Qed.
Lemma absolute_exterior_angle_theorem : ¬ hypothesis_of_obtuse_saccheri_quadrilaterals →
∀ A B C D E F B', ¬ Col A B C → Bet B A B' → A ≠ B' → SumA A B C B C A D E F →
LeA D E F C A B'.
Proof.
intros noah A B C D E F B' HNCol HBet HAB' HSuma.
assert (HIsi := t22_20 noah A B C D E F HSuma).
assert_diffs.
apply sams_chara with B; SumA.
Qed.
End Saccheri.
Hint Resolve sac__par_strict1423 sac__par_strict1234 sac__par1423 sac__par1234 : Par.