Library GeoCoq.Tarski_dev.Annexes.suma
Require Export GeoCoq.Tarski_dev.Ch11_angles.
Section Suma_1.
Context `{T2D:Tarski_2D}.
Lemma suma_distincts : ∀ A B C D E F G H I, SumA A B C D E F G H I →
A≠B ∧ B≠C ∧ D≠E ∧ E≠F ∧ G≠H ∧ H≠I.
Proof.
intros A B C D E F G H I Hsuma.
destruct Hsuma as [J HJ].
spliter.
assert_diffs.
repeat split; auto.
Qed.
Lemma ex_suma : ∀ A B C D E F, A≠B → B≠C → D≠E → E≠F →
∃ G H I, SumA A B C D E F G H I.
Proof.
intros A B C D E F HAB HBC HDE HEF.
∃ A.
∃ B.
elim (Col_dec A B C).
{ intro HColB.
assert (HJ : ∃ J, CongA D E F C B J) by (apply angle_construction_3; auto).
destruct HJ as [J HConga].
assert_diffs.
∃ J.
∃ J.
repeat (split; CongA).
apply (col123__nos); Col.
}
intro HNColB.
elim (Col_dec D E F).
{ intro HColE.
elim (bet_dec D E F).
{ intro HEBet.
assert (HJ : ∃ J, Midpoint B C J) by (apply symmetric_point_construction).
destruct HJ as [J HMid].
assert_diffs.
destruct HMid as [HJBet HCong].
∃ J.
∃ J.
split.
apply conga_line; Between; repeat split; auto; intro; treat_equalities; absurde.
split; CongA.
apply col124__nos; Col.
}
intro HENBet.
assert (HEOut : Out E D F) by (apply l6_4_2; auto).
∃ C.
∃ C.
split.
apply (out_conga C B C D E D); auto; try (apply out_trivial); CongA.
split; CongA.
apply col124__nos; Col.
}
intro HNColE.
assert (HJ : ∃ J, CongA D E F C B J ∧ TS C B J A) by (apply ex_conga_ts; Col).
destruct HJ as [J [HConga HTwo]].
assert_diffs.
∃ J.
∃ J.
repeat (split; CongA).
apply l9_9; apply l9_2; apply invert_two_sides; auto.
Qed.
Section Suma_1.
Context `{T2D:Tarski_2D}.
Lemma suma_distincts : ∀ A B C D E F G H I, SumA A B C D E F G H I →
A≠B ∧ B≠C ∧ D≠E ∧ E≠F ∧ G≠H ∧ H≠I.
Proof.
intros A B C D E F G H I Hsuma.
destruct Hsuma as [J HJ].
spliter.
assert_diffs.
repeat split; auto.
Qed.
Lemma ex_suma : ∀ A B C D E F, A≠B → B≠C → D≠E → E≠F →
∃ G H I, SumA A B C D E F G H I.
Proof.
intros A B C D E F HAB HBC HDE HEF.
∃ A.
∃ B.
elim (Col_dec A B C).
{ intro HColB.
assert (HJ : ∃ J, CongA D E F C B J) by (apply angle_construction_3; auto).
destruct HJ as [J HConga].
assert_diffs.
∃ J.
∃ J.
repeat (split; CongA).
apply (col123__nos); Col.
}
intro HNColB.
elim (Col_dec D E F).
{ intro HColE.
elim (bet_dec D E F).
{ intro HEBet.
assert (HJ : ∃ J, Midpoint B C J) by (apply symmetric_point_construction).
destruct HJ as [J HMid].
assert_diffs.
destruct HMid as [HJBet HCong].
∃ J.
∃ J.
split.
apply conga_line; Between; repeat split; auto; intro; treat_equalities; absurde.
split; CongA.
apply col124__nos; Col.
}
intro HENBet.
assert (HEOut : Out E D F) by (apply l6_4_2; auto).
∃ C.
∃ C.
split.
apply (out_conga C B C D E D); auto; try (apply out_trivial); CongA.
split; CongA.
apply col124__nos; Col.
}
intro HNColE.
assert (HJ : ∃ J, CongA D E F C B J ∧ TS C B J A) by (apply ex_conga_ts; Col).
destruct HJ as [J [HConga HTwo]].
assert_diffs.
∃ J.
∃ J.
repeat (split; CongA).
apply l9_9; apply l9_2; apply invert_two_sides; auto.
Qed.
Unicity of the sum.
Lemma suma2__conga : ∀ A B C D E F G H I G' H' I',
SumA A B C D E F G H I → SumA A B C D E F G' H' I' → CongA G H I G' H' I'.
Proof.
intros A B C D E F G H I G' H' I' Hsuma Hsuma'.
destruct Hsuma as [J [HJ1 [HJ2 HJ3]]].
destruct Hsuma' as [J' [HJ'1 [HJ'2 HJ'3]]].
assert_diffs.
assert (HcongaC : CongA C B J C B J') by (apply (conga_trans C B J D E F); auto; apply conga_sym; auto).
assert (HcongaA : CongA A B J A B J').
{ elim (Col_dec A B C).
{ intro HColB.
elim (bet_dec A B C).
{ intro HBBet.
apply (l11_13 C B J C B J'); Between.
}
intro HBNBet.
assert (HBOut : Out B A C) by (apply l6_4_2; auto).
apply (l11_10 C B J C B J'); try (apply out_trivial); auto.
}
intro HNColB.
elim (Col_dec D E F).
{ intro HColE.
apply (out_conga A B J A B J); try (apply out_trivial); CongA.
elim (bet_dec D E F).
{ intro HEBet.
apply l6_3_2; repeat split; auto.
∃ C.
split; auto; split; apply (bet_conga_bet D E F); CongA.
}
intro HENBet.
assert (HEOut : Out E D F) by (apply l6_4_2; auto).
apply (l6_7 B J C); apply (out_conga_out D E F); CongA.
}
intro HNColE.
apply (l11_22a A B J C A B J' C); auto.
repeat (split; try (apply not_one_side_two_sides); CongA); apply (ncol_conga_ncol D E F); CongA.
}
apply (conga_trans G H I A B J).
CongA.
apply (conga_trans A B J A B J'); auto.
Qed.
Commutativity of the sum.
Lemma suma_sym : ∀ A B C D E F G H I, SumA A B C D E F G H I → SumA D E F A B C G H I.
Proof.
intros A B C D E F G H I Hsuma.
destruct Hsuma as [J [HCongaBCJ [HNOne HCongaABJ]]].
assert_diffs.
elim (Col_dec A B C).
{ intro HColB.
elim (bet_dec A B C).
{ intro HBBet.
assert (HK : ∃ K, Midpoint E F K) by (apply symmetric_point_construction).
destruct HK as [K [HKBet HCong]].
assert_diffs.
∃ K.
split; try (apply conga_line; auto).
split.
intro HOne; assert (¬ Col E F K) by (apply (one_side_not_col123 E F K D); apply one_side_symmetry; auto); assert_cols; Col.
apply (conga_trans D E K A B J); auto.
apply conga_left_comm; apply (l11_13 F E D C B J); Between; CongA.
}
intro HBNBet.
assert (HBOut : Out B A C) by (apply l6_4_2; auto).
∃ F.
split.
apply (l11_10 F E F C B C); try (apply out_trivial); CongA.
split.
apply col124__nos; Col.
apply (conga_trans D E F A B J); auto.
apply conga_sym.
apply (l11_10 C B J D E F); try (apply out_trivial); auto.
}
intro HNColB.
elim (Col_dec D E F).
{ intro HColE.
assert (HK : ∃ K, CongA A B C F E K) by (apply angle_construction_3; auto).
destruct HK as [K HConga].
assert_diffs.
∃ K.
split; CongA.
split.
intro HOne; assert (¬ Col E F D) by (apply (one_side_not_col123 E F D K); auto); Col.
apply (conga_trans D E K A B J); auto.
elim (bet_dec D E F).
{ intro HEBet.
apply conga_sym; apply conga_left_comm.
apply (l11_13 C B A F); CongA; Between.
apply (bet_conga_bet D E F); CongA.
}
intro HENBet.
assert (HEOut : Out E D F) by (apply l6_4_2; auto).
apply conga_sym.
apply (l11_10 A B C F E K); try (apply out_trivial); auto.
apply (out_conga_out D E F); CongA.
}
intro HNColE.
assert (HK : ∃ K, CongA A B C F E K ∧ TS F E K D) by (apply ex_conga_ts; Col).
destruct HK as [K [HConga HTwo]].
∃ K.
split; CongA.
split.
apply l9_9; apply l9_2; apply invert_two_sides; auto.
apply (conga_trans D E K A B J); auto.
apply conga_sym; apply conga_right_comm.
apply (l11_22a A B J C K E D F).
split.
apply not_one_side_two_sides; Col.
intro; assert (Col D E F) by (apply (col_conga_col C B J D E F); Col); Col.
split.
apply invert_two_sides; auto.
split; CongA.
Qed.
CongA preserves SumA.
Lemma conga3_suma__suma : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
SumA A B C D E F G H I →
CongA A B C A' B' C' →
CongA D E F D' E' F' →
CongA G H I G' H' I' →
SumA A' B' C' D' E' F' G' H' I'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I' Hsuma HCongaB HCongaE HCongaH.
assert (Hsuma' : SumA D' E' F' A B C G' H' I').
{ apply suma_sym.
destruct Hsuma as [J [HJ1 [HJ2 HJ3]]].
∃ J.
split.
apply (conga_trans C B J D E F); auto.
split; auto.
apply (conga_trans A B J G H I); auto.
}
apply suma_sym.
destruct Hsuma' as [J [HJ1 [HJ2 HJ3]]].
∃ J.
split.
apply (conga_trans F' E' J A B C); auto.
split; auto.
Qed.
Out preserves SumA.
Lemma out6_suma__suma : ∀ A B C D E F G H I A' C' D' F' G' I',
SumA A B C D E F G H I → Out B A A' → Out B C C' → Out E D D' →
Out E F F' → Out H G G' → Out H I I' → SumA A' B C' D' E F' G' H I'.
Proof.
intros.
assert_diffs.
apply (conga3_suma__suma A B C D E F G H I); auto.
apply (out_conga A B C A B C); try (apply out_trivial); CongA.
apply (out_conga D E F D E F); try (apply out_trivial); CongA.
apply (out_conga G H I G H I); try (apply out_trivial); CongA.
Qed.
ABC + 0 = ABC (two lemmas)
Lemma out546_suma__conga : ∀ A B C D E F G H I, SumA A B C D E F G H I →
Out E D F → CongA A B C G H I.
Proof.
intros A B C D E F G H I Hsuma Hout.
assert(A≠B∧B≠C∧D≠E∧E≠F∧G≠H∧H≠I) by (apply suma_distincts; auto).
spliter.
apply (suma2__conga A B C D E F A B C); auto.
∃ C.
split.
apply (out_conga C B C D E D); try (apply out_trivial); CongA.
split; CongA.
apply col124__nos; Col.
Qed.
Lemma out546__suma : ∀ A B C D E F, A ≠ B → B ≠ C → Out E D F → SumA A B C D E F A B C.
Proof.
intros A B C D E F HAB HBC Hout.
assert_diffs.
destruct (ex_suma A B C D E F) as [G [H [I Hsuma]]]; auto.
apply (conga3_suma__suma A B C D E F G H I); try (apply conga_refl); auto.
apply conga_sym, out546_suma__conga with D E F; auto.
Qed.
0 + DEF = DEF (two lemmas)
Lemma out213_suma__conga : ∀ A B C D E F G H I, SumA A B C D E F G H I →
Out B A C → CongA D E F G H I.
Proof.
intros A B C D E F G H I Hsuma Hout.
apply (out546_suma__conga D E F A B C); auto.
apply suma_sym; auto.
Qed.
Lemma out213__suma : ∀ A B C D E F, D ≠ E → E ≠ F → Out B A C → SumA A B C D E F D E F.
Proof.
intros; apply suma_sym, out546__suma; auto.
Qed.
Some permutation properties:
Lemma suma_left_comm : ∀ A B C D E F G H I,
SumA A B C D E F G H I → SumA C B A D E F G H I.
Proof.
intros A B C D E F G H I Hsuma.
assert(Hd := suma_distincts A B C D E F G H I Hsuma).
spliter.
apply (conga3_suma__suma A B C D E F G H I); CongA.
Qed.
Lemma suma_middle_comm : ∀ A B C D E F G H I,
SumA A B C D E F G H I → SumA A B C F E D G H I.
Proof.
intros A B C D E F G H I Hsuma.
assert(Hd := suma_distincts A B C D E F G H I Hsuma).
spliter.
apply (conga3_suma__suma A B C D E F G H I); CongA.
Qed.
Lemma suma_right_comm : ∀ A B C D E F G H I,
SumA A B C D E F G H I → SumA A B C D E F I H G.
Proof.
intros A B C D E F G H I Hsuma.
assert(Hd := suma_distincts A B C D E F G H I Hsuma).
spliter.
apply (conga3_suma__suma A B C D E F G H I); CongA.
Qed.
Lemma suma_comm : ∀ A B C D E F G H I,
SumA A B C D E F G H I → SumA C B A F E D I H G.
Proof.
intros A B C D E F G H I Hsuma.
assert(Hd := suma_distincts A B C D E F G H I Hsuma).
spliter.
apply (conga3_suma__suma A B C D E F G H I); CongA.
Qed.
Basic cases of sum
Lemma inangle__suma : ∀ A B C P, InAngle P A B C → SumA A B P P B C A B C.
Proof.
intros A B C P HInangle.
assert (Hcopy := HInangle); destruct Hcopy as [HAB [HCB [HPB _]]].
∃ C; repeat (split; CongA).
elim (Col_dec B P A).
apply col123__nos.
intro HNCol.
elim (Col_dec B P C).
apply col124__nos.
intro HNCol2.
apply l9_9, invert_two_sides, in_angle_two_sides; Col.
Qed.
Lemma bet__suma : ∀ A B C P, A ≠ B → B ≠ C → P ≠ B → Bet A B C →
SumA A B P P B C A B C.
Proof.
intros A B C P HAB HBC HPB HBet.
apply inangle__suma.
apply in_angle_line; auto.
Qed.
Characterization of SAMS using LeA.
Lemma sams_chara : ∀ A B C D E F A', A≠B → A'≠B → Bet A B A' →
(SAMS A B C D E F ↔ LeA D E F C B A').
Proof.
intros A B C D E F A' HAB HA'B HABA'.
split.
- intro Hint.
destruct Hint as [_ [HUn [J [HJ1 [HJ2 HJ3]]]]].
assert_diffs.
destruct HUn as [HEOut | HBNBet].
apply l11_31_1; auto.
elim (Col_dec A B C).
{ intro HColB.
apply l11_31_2; auto.
apply (bet_out_out_bet A B A'); try (apply out_trivial); auto.
apply l6_4_2; auto.
}
intro HNColB.
elim (Col_dec D E F).
{ intro HColE.
elim (bet_dec D E F).
{ intro HDEF.
exfalso.
apply HJ3.
assert (HCBJ : Bet C B J) by (apply (bet_conga_bet D E F); CongA; Between); assert_cols.
repeat split; Col.
intro; apply HNColB; apply (l6_16_1 B J C A); Col.
∃ B.
split; Col; Between.
}
intro; apply l11_31_1; auto; apply l6_4_2; auto.
}
intro HNColE.
apply (l11_30 C B J C B A'); try (apply conga_refl); auto.
∃ J.
split; CongA.
apply l11_24; apply (in_angle_reverse A); auto.
assert (HTwo : TS B C A J).
{ apply not_one_side_two_sides; auto.
apply (ncol_conga_ncol D E F); CongA.
}
destruct HTwo as [_ [_ [X [HXCol HXBet]]]].
repeat split; auto.
∃ X.
split; auto.
elim (eq_dec_points B X); auto.
intro HBX.
right.
apply (col_one_side_out B A X C); Col.
apply invert_one_side.
apply (one_side_transitivity A B X J).
{ apply out_one_side.
left; intro; apply HNColB; apply (l6_16_1 B X); Col.
assert (HAX : A≠X) by (intro; treat_equalities; Col).
repeat split; auto.
intro; treat_equalities; auto.
}
apply one_side_symmetry.
apply not_two_sides_one_side; Col.
intro; apply HNColB. apply (l6_16_1 B X); Col. apply (col_transitivity_2 J); Col.
intro; treat_equalities; auto.
- intro Hlea.
assert_diffs.
split; auto.
elim (Col_dec A B C).
{ intro HColB.
elim (bet_dec A B C).
{ intro HBBet.
assert (HEOut : Out E D F).
{ assert (Out B C A') by (apply (l6_3_2); repeat split; auto; ∃ A; repeat split; Between).
apply (out_conga_out C B A'); auto.
apply lea_asym; auto.
apply l11_31_1; auto.
}
split; try left; auto.
∃ C.
split.
apply (out_conga C B C D E D); try (apply out_trivial); CongA.
split.
apply col124__nos; Col.
apply not_two_sides_id.
}
intro HBNBet.
assert (HBOut : Out B A C) by (apply not_bet_out; auto).
split.
right; auto.
assert (HJ : ∃ J : Tpoint, CongA D E F C B J) by (apply (angle_construction_3 D E F C B); auto).
destruct HJ as [J HJ].
∃ J.
split; CongA.
split.
apply col123__nos; Col.
intro HTwo; destruct HTwo as [HBA [HNCol _]]; Col.
}
intro HNColB.
assert (HNColB' : ¬ Col A' B C) by (intro; apply HNColB; apply (l6_16_1 B A'); Col).
elim (Col_dec D E F).
{ intro HNColE.
assert (HEOut : Out E D F).
{ apply not_bet_out; auto.
intro HEBet.
apply HNColB'.
apply bet_col; apply between_symmetry.
apply (bet_lea__bet D E F); auto.
}
split.
left; auto.
∃ C.
split.
apply (out_conga C B C D E D); try (apply out_trivial); CongA.
split.
apply col124__nos; Col.
apply not_two_sides_id.
}
intro HNColE.
split.
right; intro; Col.
assert (HJ : ∃ J, CongA D E F C B J ∧ TS C B J A) by (apply ex_conga_ts; Col).
destruct HJ as [J [HCongaJ HTwo]].
assert_diffs.
∃ J.
split; CongA.
split.
apply l9_9; apply l9_2; apply invert_two_sides; auto.
elim (Col_dec A B J).
{ intro HColJ.
intro HTwo'.
destruct HTwo' as [HBA [HNColC [HNColJ _]]].
Col.
}
intro HNColJ.
assert (HF : ¬ TS A' B C J).
{ apply l9_9_bis.
apply one_side_symmetry.
apply (in_angle_one_side); auto.
intro; apply HNColJ; apply (l6_16_1 B A'); Col.
apply l11_24.
destruct Hlea as [K [HInAngle HCongaK]].
apply (conga_preserves_in_angle C B A' K C B A' J); CongA.
apply (conga_trans C B K D E F); CongA.
∃ A; split; auto.
repeat (split; Col).
∃ B; split; Between; Col.
}
intro; apply HF.
apply (col_preserves_two_sides A B); Col.
Qed.
Lemma sams_distincts : ∀ A B C D E F, SAMS A B C D E F →
A≠B ∧ B≠C ∧ D≠E ∧ E≠F.
Proof.
intros A B C D E F Hisi.
destruct Hisi as [HP1 [HP2 [J HJ]]].
spliter.
assert_diffs.
repeat split; auto.
Qed.
Lemma sams_sym : ∀ A B C D E F, SAMS A B C D E F →
SAMS D E F A B C.
Proof.
intros A B C D E F Hisi.
assert(A≠B∧B≠C∧D≠E∧E≠F) by (apply sams_distincts; auto).
spliter.
assert(HD' : ∃ D', Midpoint E D D') by apply symmetric_point_construction.
destruct HD' as [D'].
assert(HA' : ∃ A', Midpoint B A A') by apply symmetric_point_construction.
destruct HA' as [A'].
assert_diffs.
apply (sams_chara D E F A B C D'); Between.
apply lea_right_comm.
apply (l11_36 D _ _ A'); Between.
apply lea_right_comm.
apply (sams_chara A); Between.
Qed.
Lemma sams_right_comm : ∀ A B C D E F, SAMS A B C D E F →
SAMS A B C F E D.
Proof.
intros A B C D E F Hisi.
destruct Hisi as [HAB [HUn [J [HJ1 [HJ2 HJ3]]]]].
split; auto.
split.
{ destruct HUn.
left; apply l6_6; auto.
right; auto.
}
∃ J.
split.
apply conga_right_comm; auto.
split; auto.
Qed.
Lemma sams_left_comm : ∀ A B C D E F, SAMS A B C D E F →
SAMS C B A D E F.
Proof.
intros.
apply sams_sym.
apply sams_right_comm.
apply sams_sym.
assumption.
Qed.
Lemma sams_comm : ∀ A B C D E F, SAMS A B C D E F →
SAMS C B A F E D.
Proof.
intros.
apply sams_left_comm.
apply sams_right_comm.
assumption.
Qed.
Lemma conga2_sams__sams : ∀ A B C D E F A' B' C' D' E' F',
CongA A B C A' B' C' → CongA D E F D' E' F' →
SAMS A B C D E F → SAMS A' B' C' D' E' F'.
Proof.
intros A B C D E F A' B' C' D' E' F' HCongaB HCongaE Hisi.
assert(HA0 : ∃ A0, Midpoint B A A0) by apply symmetric_point_construction.
destruct HA0 as [A0].
assert(HA'0 : ∃ A'0, Midpoint B' A' A'0) by apply symmetric_point_construction.
destruct HA'0 as [A'0].
assert_diffs.
apply (sams_chara _ _ _ _ _ _ A'0); Between.
apply (l11_30 D E F C B A0); try (apply (sams_chara A)); Between.
apply conga_comm.
apply (l11_13 A B C A'); Between.
Qed.
Lemma out546__sams : ∀ A B C D E F, A ≠ B → B ≠ C → Out E D F → SAMS A B C D E F.
Proof.
intros A B C D E F HAB HBC HOut.
destruct (segment_construction A B A B) as [A' [HBet HCong]].
assert_diffs.
apply sams_chara with A'; auto.
apply l11_31_1; auto.
Qed.
Lemma out213__sams : ∀ A B C D E F, D ≠ E → E ≠ F → Out B A C → SAMS A B C D E F.
Proof.
intros; apply sams_sym, out546__sams; trivial.
Qed.
Lemma bet_suma__sams : ∀ A B C D E F G H I, SumA A B C D E F G H I → Bet G H I →
SAMS A B C D E F.
Proof.
intros A B C D E F G H I HSuma HBet.
destruct HSuma as [A' [HConga1 [HNOS HConga2]]].
apply (bet_conga_bet _ _ _ A B A') in HBet; CongA.
assert_diffs.
repeat split; auto.
- elim (bet_dec A B C).
{ intro HBet'; left.
apply (l11_21_a C B A'); trivial.
apply l6_2 with A; Between.
}
intro HNBet; auto.
- ∃ A'; repeat (split; auto).
intro HTS; destruct HTS as [_ []]; assert_cols; Col.
Qed.
Lemma inangle__sams : ∀ A B C P, InAngle P A B C → SAMS A B P P B C.
Proof.
intros A B C P HInangle.
assert (Hcopy := HInangle); destruct Hcopy as [HAB [HCB [HPB HX]]].
repeat split; auto.
{ destruct (bet_dec A B P) as [HBet|]; [left|auto].
apply l6_2 with A; Between.
destruct HX as [X [HBet1 [HXB|HOut]]]; [subst X; Between|].
assert (HBet2 : Bet X B A) by (assert_diffs; apply (l6_2 P); Between; apply l6_6, HOut).
eBetween.
}
∃ C; split; CongA.
destruct (Col_dec B P A) as [HCol|HNCol].
split; [apply col123__nos, HCol|intro HTS; destruct HTS as []; Col].
split.
- destruct (Col_dec B P C) as [HCol1|HNCol1].
apply col124__nos, HCol1.
apply l9_9, invert_two_sides, in_angle_two_sides; Col.
- destruct (Col_dec A B C) as [HCol1|HNCol1].
intro HTS; destruct HTS as [_ []]; Col.
apply l9_9_bis, in_angle_one_side; Col.
Qed.
End Suma_1.
Ltac assert_diffs :=
repeat
match goal with
| H:(¬Col ?X1 ?X2 ?X3) |- _ ⇒
let h := fresh in
not_exist_hyp3 X1 X2 X1 X3 X2 X3;
assert (h := not_col_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps
| H:(¬Bet ?X1 ?X2 ?X3) |- _ ⇒
let h := fresh in
not_exist_hyp2 X1 X2 X2 X3;
assert (h := not_bet_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps
| H:Bet ?A ?B ?C, H2 : ?A ≠ ?B |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A C);
assert (T:= bet_neq12__neq A B C H H2);clean_reap_hyps
| H:Bet ?A ?B ?C, H2 : ?B ≠ ?A |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A C);
assert (T:= bet_neq21__neq A B C H H2);clean_reap_hyps
| H:Bet ?A ?B ?C, H2 : ?B ≠ ?C |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A C);
assert (T:= bet_neq23__neq A B C H H2);clean_reap_hyps
| H:Bet ?A ?B ?C, H2 : ?C ≠ ?B |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A C);
assert (T:= bet_neq32__neq A B C H H2);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?A ≠ ?B |-_ ⇒
let T:= fresh in (not_exist_hyp_comm C D);
assert (T:= cong_diff A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?B ≠ ?A |-_ ⇒
let T:= fresh in (not_exist_hyp_comm C D);
assert (T:= cong_diff_2 A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?C ≠ ?D |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A B);
assert (T:= cong_diff_3 A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?D ≠ ?C |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A B);
assert (T:= cong_diff_4 A B C D H2 H);clean_reap_hyps
| H:Le ?A ?B ?C ?D, H2 : ?A ≠ ?B |-_ ⇒
let T:= fresh in (not_exist_hyp_comm C D);
assert (T:= le_diff A B C D H2 H);clean_reap_hyps
| H:Lt ?A ?B ?C ?D |-_ ⇒
let T:= fresh in (not_exist_hyp_comm C D);
assert (T:= lt_diff A B C D H);clean_reap_hyps
| H:Midpoint ?I ?A ?B, H2 : ?A≠?B |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B I A);
assert (T:= midpoint_distinct_1 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:Midpoint ?I ?A ?B, H2 : ?B≠?A |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B I A);
assert (T:= midpoint_distinct_1 I A B (swap_diff B A H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:Midpoint ?I ?A ?B, H2 : ?I≠?A |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B A B);
assert (T:= midpoint_distinct_2 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:Midpoint ?I ?A ?B, H2 : ?A≠?I |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B A B);
assert (T:= midpoint_distinct_2 I A B (swap_diff A I H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:Midpoint ?I ?A ?B, H2 : ?I≠?B |- _ ⇒
let T:= fresh in (not_exist_hyp2 I A A B);
assert (T:= midpoint_distinct_3 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:Midpoint ?I ?A ?B, H2 : ?B≠?I |- _ ⇒
let T:= fresh in (not_exist_hyp2 I A A B);
assert (T:= midpoint_distinct_3 I A B (swap_diff B I H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:Perp ?A ?B ?C ?D |- _ ⇒
let T:= fresh in (not_exist_hyp2 A B C D);
assert (T:= perp_distinct A B C D H);
decompose [and] T;clear T;clean_reap_hyps
| H:Perp_at ?X ?A ?B ?C ?D |- _ ⇒
let T:= fresh in (not_exist_hyp2 A B C D);
assert (T:= perp_in_distinct X A B C D H);
decompose [and] T;clear T;clean_reap_hyps
| H:Out ?A ?B ?C |- _ ⇒
let T:= fresh in (not_exist_hyp2 A B A C);
assert (T:= out_distinct A B C H);
decompose [and] T;clear T;clean_reap_hyps
| H:TS ?A ?B ?C ?D |- _ ⇒
let h := fresh in
not_exist_hyp6 A B A C A D B C B D C D;
assert (h := ts_distincts A B C D H);decompose [and] h;clear h;clean_reap_hyps
| H:OS ?A ?B ?C ?D |- _ ⇒
let h := fresh in
not_exist_hyp5 A B A C A D B C B D;
assert (h := os_distincts A B C D H);decompose [and] h;clear h;clean_reap_hyps
| H:CongA ?A ?B ?C ?A' ?B' ?C' |- _ ⇒
let T:= fresh in (not_exist_hyp_comm A B);
assert (T:= conga_diff1 A B C A' B' C' H);clean_reap_hyps
| H:CongA ?A ?B ?C ?A' ?B' ?C' |- _ ⇒
let T:= fresh in (not_exist_hyp_comm B C);
assert (T:= conga_diff2 A B C A' B' C' H);clean_reap_hyps
| H:CongA ?A ?B ?C ?A' ?B' ?C' |- _ ⇒
let T:= fresh in (not_exist_hyp_comm A' B');
assert (T:= conga_diff45 A B C A' B' C' H);clean_reap_hyps
| H:CongA ?A ?B ?C ?A' ?B' ?C' |- _ ⇒
let T:= fresh in (not_exist_hyp_comm B' C');
assert (T:= conga_diff56 A B C A' B' C' H);clean_reap_hyps
| H:SumA ?A ?B ?C ?D ?E ?F ?G ?I ?J |- _ ⇒
let h := fresh in
not_exist_hyp6 A B B C D E E F G I I J;
assert (h := suma_distincts A B C D E F G I J H);decompose [and] h;clear h;clean_reap_hyps
| H:SAMS ?A ?B ?C ?D ?E ?F |- _ ⇒
let h := fresh in
not_exist_hyp4 A B B C D E E F;
assert (h := sams_distincts A B C D E F H);decompose [and] h;clear h;clean_reap_hyps
| H:(InAngle ?P ?A ?B ?C) |- _ ⇒
let h := fresh in
not_exist_hyp3 A B C B P B;
assert (h := inangle_distincts A B C P H);decompose [and] h;clear h;clean_reap_hyps
| H:LeA ?A ?B ?C ?D ?E ?F |- _ ⇒
let h := fresh in
not_exist_hyp4 A B B C D E E F;
assert (h := lea_distincts A B C D E F H);decompose [and] h;clear h;clean_reap_hyps
| H:LtA ?A ?B ?C ?D ?E ?F |- _ ⇒
let h := fresh in
not_exist_hyp4 A B B C D E E F;
assert (h := lta_distincts A B C D E F H);decompose [and] h;clear h;clean_reap_hyps
| H:(Acute ?A ?B ?C) |- _ ⇒
let h := fresh in
not_exist_hyp2 A B B C;
assert (h := acute_distincts A B C H);decompose [and] h;clear h;clean_reap_hyps
| H:(Obtuse ?A ?B ?C) |- _ ⇒
let h := fresh in
not_exist_hyp2 A B B C;
assert (h := obtuse_distincts A B C H);decompose [and] h;clear h;clean_reap_hyps
end.
Hint Resolve suma_sym suma_left_comm suma_middle_comm
suma_right_comm suma_comm bet__suma inangle__suma
sams_right_comm sams_comm sams_left_comm
sams_sym out213__sams out546__sams inangle__sams : suma.
Ltac SumA := eauto with suma.
Section Suma_2.
Context `{T2D:Tarski_2D}.
ABC <= ABC + DEF.
Lemma sams_suma__lea123789 : ∀ A B C D E F G H I, SumA A B C D E F G H I →
SAMS A B C D E F → LeA A B C G H I.
Proof.
intros A B C D E F G H I Hsuma Hisi.
assert_diffs.
spliter.
elim(Col_dec A B C).
{ intro HColB.
elim(bet_dec A B C).
{ intro HBBet.
destruct Hisi as [_[[HEout|]]]; try solve[exfalso; auto].
apply conga__lea.
apply (out546_suma__conga _ _ _ D E F); auto.
}
intro HBout.
apply l11_31_1; auto.
apply not_bet_out; auto.
}
intro HNColB.
elim(Col_dec D E F).
{ intro HColE.
elim(bet_dec D E F).
{ intro HEBet.
apply sams_sym in Hisi.
destruct Hisi as [_[[HBout|]]]; try solve[exfalso; auto].
apply l11_31_1; auto.
}
intro HEout.
apply conga__lea.
apply (out546_suma__conga _ _ _ D E F); auto.
apply not_bet_out; auto.
}
intro HNColE.
elim(Col_dec G H I).
{ intro HColH.
elim(bet_dec G H I).
apply l11_31_2; auto.
intro HHout.
apply not_bet_out in HHout; auto.
exfalso.
destruct Hisi as [_ [HUn _]].
destruct HUn as [HEout | HBNBet].
apply HNColE; apply col_permutation_4; apply out_col; auto.
destruct Hsuma as [J [HJ1 [HJ2 HJ3]]].
apply HJ2.
apply conga_sym in HJ3.
apply out_conga_out in HJ3; auto.
apply (l9_19 _ _ _ _ B); try split; Col.
}
intro HNColH.
destruct Hisi as [_ [_ [J [HJ1 [HJ2 HJ3]]]]].
assert_diffs.
assert(HNColJ : ¬ Col J B C).
{ intro HColJ.
apply HNColE.
apply (col_conga_col J B C); CongA.
}
assert(HCongaJ : CongA A B J G H I).
{ apply (suma2__conga A B C D E F); auto.
∃ J.
repeat (split; CongA).
}
assert(HNColJ2 : ¬ Col J B A).
{ intro HColJ.
apply HNColH.
apply (col_conga_col A B J); Col.
}
apply (l11_30 A B C A B J); CongA.
∃ C.
split; CongA.
apply not_one_side_two_sides in HJ2; auto.
destruct HJ2 as [a [b [X [HColX HXBet]]]].
repeat split; auto.
∃ X.
split; auto.
right.
assert(HNColX : ¬Col X A B).
{ intro.
apply HNColJ2.
apply col_permutation_1; apply (col_transitivity_1 A X); Col.
intro; subst X; Col.
}
assert_diffs.
apply (col_one_side_out _ A); Col.
apply invert_one_side.
apply (one_side_transitivity _ _ _ J).
- apply out_one_side.
left; Col.
apply bet_out; auto.
- apply one_side_symmetry.
apply not_two_sides_one_side; Col.
Qed.
DEF <= ABC + DEF.
Lemma sams_suma__lea456789 : ∀ A B C D E F G H I, SumA A B C D E F G H I →
SAMS A B C D E F → LeA D E F G H I.
Proof.
intros A B C D E F G H I Hsuma Hisi.
apply (sams_suma__lea123789 D E F A B C G H I); SumA.
Qed.
LeA preserves SAMS.
Lemma sams_lea2__sams : ∀ A B C D E F A' B' C' D' E' F',
SAMS A' B' C' D' E' F' → LeA A B C A' B' C' → LeA D E F D' E' F' →
SAMS A B C D E F.
Proof.
intros A B C D E F A' B' C' D' E' F' Hisi HleaB HleaE.
assert(HA0 : ∃ A0, Midpoint B A A0) by apply symmetric_point_construction.
destruct HA0 as [A0].
assert(HA'0 : ∃ A'0, Midpoint B' A' A'0) by apply symmetric_point_construction.
destruct HA'0 as [A'0].
assert_diffs.
apply (sams_chara _ _ _ _ _ _ A0); Between.
apply (lea_trans D E F D' E' F'); auto.
apply (lea_trans D' E' F' C' B' A'0).
- apply (sams_chara A'); Between.
- apply lea_comm.
apply (l11_36 A B C A'); Between.
Qed.
Lemma sams_lea456_suma2__lea : ∀ A B C D E F G H I D' E' F' G' H' I',
LeA D E F D' E' F' → SAMS A B C D' E' F' → SumA A B C D E F G H I →
SumA A B C D' E' F' G' H' I' → LeA G H I G' H' I'.
Proof.
intros A B C D E F G H I D' E' F' G' H' I' Hlea Hisi' Hsuma Hsuma'.
assert_diffs.
elim(out_dec E' D' F').
{ intro HE'out.
apply conga__lea.
apply (conga_trans _ _ _ A B C).
apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto; apply (out_lea__out _ _ _ D' E' F'); auto.
apply (out546_suma__conga _ _ _ D' E' F'); auto.
}
intro HE'Nout.
elim(Col_dec A B C).
{ intro HColB.
destruct Hisi' as [_ [[HE'out|HBNBet]_]].
exfalso; auto.
apply not_bet_out in HColB; auto.
apply (l11_30 D E F D' E' F'); auto; apply (out213_suma__conga A B C); auto.
}
intro HNColB.
elim(Col_dec D' E' F').
{ intro HColE'.
apply sams_sym in Hisi'.
destruct Hisi' as [_ [[HBout|HE'NBet]_]]; exfalso.
apply HNColB; assert_cols; Col.
apply not_bet_out in HColE'; auto.
}
intro HNColE'.
clear HE'Nout.
elim(Col_dec D E F).
{ intro HColE.
assert(¬ Bet D E F) by (intro; apply HNColE'; apply bet_col; apply (bet_lea__bet D E F); auto).
apply (l11_30 A B C G' H' I'); try (apply conga_refl); auto.
apply (sams_suma__lea123789 _ _ _ D' E' F'); auto.
apply (out546_suma__conga _ _ _ D E F); auto.
apply not_bet_out; auto.
}
intro HNColE.
elim(Col_dec G' H' I').
{ intro HColH'.
elim(bet_dec G' H' I').
apply l11_31_2; auto.
intro HH'out.
apply not_bet_out in HH'out; auto.
exfalso.
apply HNColB.
apply col_permutation_4.
apply out_col.
apply (out_lea__out _ _ _ G' H' I'); auto.
apply (sams_suma__lea123789 _ _ _ D' E' F'); auto.
}
intro HNColH'.
destruct Hisi' as [_[_[F'1]]].
spliter.
apply(l11_30 _ _ _ _ _ _ D E F C B F'1) in Hlea; CongA.
destruct Hlea as [F1].
spliter.
assert_diffs.
assert(CongA A B F'1 G' H' I').
apply (suma2__conga A B C D' E' F'); auto; ∃ F'1; repeat (split; CongA).
assert(¬ Col A B F'1) by (apply (ncol_conga_ncol G' H' I'); CongA).
assert(¬ Col C B F'1) by (apply (ncol_conga_ncol D' E' F'); CongA).
apply (l11_30 A B F1 A B F'1); auto.
- ∃ F1.
split; CongA.
apply l11_24.
apply (in_angle_trans _ _ _ C).
apply l11_24; auto.
assert(Hts : TS B C A F'1) by (apply not_one_side_two_sides; Col).
destruct Hts as [_ [_ [X]]].
spliter.
repeat split; auto.
∃ X.
split; Between.
right.
apply (col_one_side_out _ A); Col.
apply invert_one_side.
apply (one_side_transitivity _ _ _ F'1); auto.
2: apply one_side_symmetry; apply not_two_sides_one_side; Col.
apply out_one_side; Col.
apply bet_out; auto; intro; subst A; Col.
- apply (suma2__conga A B C D E F); auto.
∃ F1.
repeat (split; CongA).
apply l9_9.
apply l9_2.
apply (l9_8_2 _ _ F'1).
apply l9_2; apply not_one_side_two_sides; Col.
apply invert_one_side; apply one_side_symmetry.
apply in_angle_one_side; Col.
apply not_col_permutation_4; apply (ncol_conga_ncol D E F); auto.
Qed.
Lemma sams_lea123_suma2__lea : ∀ A B C D E F G H I A' B' C' G' H' I',
LeA A B C A' B' C' → SAMS A' B' C' D E F → SumA A B C D E F G H I →
SumA A' B' C' D E F G' H' I' → LeA G H I G' H' I'.
Proof.
intros A B C D E F G H I A' B' C'.
intros.
apply (sams_lea456_suma2__lea D E F A B C _ _ _ A' B' C'); SumA.
Qed.
SumA preserves LeA.
Lemma sams_lea2_suma2__lea : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LeA A B C A' B' C' → LeA D E F D' E' F' → SAMS A' B' C' D' E' F' →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LeA G H I G' H' I'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I' HleaB HleaD Hisi' Hsuma Hsuma'.
assert_diffs.
assert(Haux := ex_suma A B C D' E' F').
destruct Haux as [G'' [H'' [I'']]]; auto.
apply (lea_trans _ _ _ G'' H'' I'').
- apply (sams_lea456_suma2__lea A B C D E F _ _ _ D' E' F'); auto.
apply (sams_lea2__sams _ _ _ _ _ _ A' B' C' D' E' F'); Lea.
- apply (sams_lea123_suma2__lea A B C D' E' F' _ _ _ A' B' C'); auto.
Qed.
Unicity of the difference of angles.
Lemma sams2_suma2__conga456 : ∀ A B C D E F D' E' F' G H I,
SAMS A B C D E F → SAMS A B C D' E' F' →
SumA A B C D E F G H I → SumA A B C D' E' F' G H I →
CongA D E F D' E' F'.
Proof.
intros A B C D E F D' E' F' G H I Hisi Hisi' Hsuma Hsuma'.
assert_diffs.
elim(Col_dec A B C).
{ intro HColB.
elim(bet_dec A B C).
{ intro HBBet.
destruct Hisi as [_ [[HEout|]_]]; try solve [exfalso; Between].
destruct Hisi' as [_ [[HE'out|]_]]; try solve [exfalso; Between].
apply l11_21_b; auto.
}
intro HBout.
apply not_bet_out in HBout; auto.
apply (conga_trans _ _ _ G H I).
- apply (out213_suma__conga A B C); auto.
- apply conga_sym.
apply (out213_suma__conga A B C); auto.
}
intro HNColB.
destruct Hisi as [_[_[J [HJ1 [HJ2 HJ3]]]]].
destruct Hisi' as [_[_[J' [HJ'1 [HJ'2 HJ'3]]]]].
assert_diffs.
apply (conga_trans _ _ _ C B J); try solve [apply conga_sym; auto].
apply (conga_trans _ _ _ C B J'); auto.
assert(CongA A B J A B J').
{ apply (conga_trans _ _ _ G H I).
apply (suma2__conga A B C D E F); auto; ∃ J; CongA.
apply (suma2__conga A B C D' E' F'); auto; ∃ J'; CongA.
}
assert(HJJ' : Out B J J' ∨ TS A B J J') by (apply conga__or_out_ts; auto).
destruct HJJ' as [Hout|Hts].
- apply (out_conga C B J C B J); try (apply out_trivial); CongA.
- exfalso.
apply HJ'3.
apply (l9_8_2 _ _ J); auto.
apply one_side_symmetry.
apply not_two_sides_one_side; Col.
apply two_sides_not_col in Hts; Col.
Qed.
Unicity of the difference on the left.
Lemma sams2_suma2__conga123 : ∀ A B C A' B' C' D E F G H I,
SAMS A B C D E F → SAMS A' B' C' D E F →
SumA A B C D E F G H I → SumA A' B' C' D E F G H I →
CongA A B C A' B' C'.
Proof.
intros A B C A' B' C' D E F G H I Hisi Hisi' Hsuma Hsuma'.
apply (sams2_suma2__conga456 D E F _ _ _ _ _ _ G H I); SumA.
Qed.
Lemma suma_assoc_1 : ∀ A B C D E F G H I K L M A' B' C' D' E' F',
SAMS A B C D E F → SAMS D E F G H I →
SumA A B C D E F A' B' C' → SumA D E F G H I D' E' F' →
SumA A' B' C' G H I K L M → SumA A B C D' E' F' K L M.
Proof.
intros A B C D E F G H I K L M A' B' C' D' E' F' HisiBE HisiEH HsBE HsEH HsB'H.
assert(HA0 : ∃ A0, Midpoint B A A0) by apply symmetric_point_construction.
destruct HA0 as [A0].
assert(HD0 : ∃ D0, Midpoint E D D0) by apply symmetric_point_construction.
destruct HD0 as [D0].
assert_diffs.
elim(Col_dec A B C).
{ intro HColB.
elim(bet_dec A B C).
{ intro HBBet.
destruct HisiBE as [_ [[HEout | HBNBet] HJ]]; try solve [exfalso; Between].
apply (conga3_suma__suma A' B' C' G H I K L M); try (apply conga_refl); auto.
apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto.
apply (out213_suma__conga D E F); auto.
}
intro HBout.
apply not_bet_out in HBout; auto.
assert(Hexsuma : ∃ K0 L0 M0, SumA A B C D' E' F' K0 L0 M0) by (apply ex_suma; auto).
destruct Hexsuma as [K0 [L0 [M0]]].
apply (conga3_suma__suma A B C D' E' F' K0 L0 M0); try (apply conga_refl); auto.
apply (conga_trans _ _ _ D' E' F').
apply conga_sym; apply (out213_suma__conga A B C); auto.
apply (suma2__conga D E F G H I); auto.
apply (conga3_suma__suma A' B' C' G H I K L M); try (apply conga_refl); auto.
apply conga_sym.
apply (out213_suma__conga A B C); auto.
}
intro HNColB.
assert(¬ Col C B A0) by (intro; apply HNColB; apply (l6_16_1 _ A0); Col).
elim(Col_dec D E F).
{ intro HColE.
elim(bet_dec D E F).
{ intro HEBet.
destruct HisiEH as [_ [[HHout | HENBet] HJ]]; try solve [exfalso; Between].
apply (conga3_suma__suma A B C D E F A' B' C'); try (apply conga_refl); try (apply (out546_suma__conga _ _ _ G H I)); auto.
}
intro HEout.
apply not_bet_out in HEout; auto.
apply (conga3_suma__suma A' B' C' G H I K L M); try (apply conga_refl); auto.
apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto.
apply (out213_suma__conga D E F); auto.
}
intro HNColE.
assert(¬ Col F E D0) by (intro; apply HNColE; apply (l6_16_1 _ D0); Col).
elim(Col_dec G H I).
{ intro HColH.
elim(bet_dec G H I).
{ intro HHBet.
apply sams_sym in HisiEH.
destruct HisiEH as [_ [[HEout | HHNBet] HJ]]; try solve [exfalso; Between].
exfalso.
apply HNColE.
apply col_permutation_4.
apply out_col; auto.
}
intro HHout.
apply not_bet_out in HHout; auto.
apply (conga3_suma__suma A B C D E F A' B' C'); try (apply conga_refl); try (apply (out546_suma__conga _ _ _ G H I)); auto.
}
intro HNColH.
assert(¬ OS B C A A0).
{ apply l9_9.
repeat split; Col.
∃ B.
split; Col; Between.
}
assert(HisiA0: SAMS A B C A0 B C).
{ split; auto.
split.
right; intro; assert_cols; Col.
∃ A0.
repeat (split; CongA).
unfold TS.
intro; spliter; assert_cols; Col.
}
assert(¬ OS E F D D0).
{ apply l9_9.
repeat split; Col.
∃ E.
split; Col; Between.
}
assert(HisiD0: SAMS D E F D0 E F).
{ split; auto.
split.
right; intro; assert_cols; Col.
∃ D0.
repeat (split; CongA).
unfold TS.
intro; spliter; assert_cols; Col.
}
elim(Col_dec A' B' C').
{ intro HColB'.
elim(bet_dec A' B' C').
{ intro HB'Bet.
elim(Col_dec D' E' F').
{ intro HColE'.
elim(bet_dec D' E' F').
{ intro HE'Bet.
apply suma_sym.
apply (conga3_suma__suma A' B' C' G H I K L M); try (apply conga_refl); auto; try solve [apply conga_line; auto].
apply conga_sym.
apply (conga_trans _ _ _ D0 E F).
- apply (sams2_suma2__conga123 _ _ _ _ _ _ D E F A' B' C'); SumA.
apply suma_sym.
∃ D0.
split.
apply conga_pseudo_refl; auto.
split; auto.
apply conga_line; Between.
- apply (sams2_suma2__conga456 D E F _ _ _ _ _ _ D' E' F'); auto.
∃ D0.
split.
apply conga_pseudo_refl; auto.
split; auto.
apply conga_line; Between.
}
intro HE'out.
apply not_bet_out in HE'out; auto.
exfalso.
apply HNColE.
apply col_permutation_4.
apply out_col.
apply (out_lea__out _ _ _ D' E' F'); auto.
apply (sams_suma__lea123789 _ _ _ G H I); auto.
}
intro HNColE'.
assert(CongA D E F C B A0).
{ apply (sams2_suma2__conga456 A B C _ _ _ _ _ _ A' B' C'); auto.
apply (sams_chara _ _ _ _ _ _ A0); try (apply lea_refl); Between.
apply (conga3_suma__suma A B C C B A0 A B A0); try (apply conga_refl); try (apply conga_line); Between.
∃ A0.
repeat (split; CongA).
}
assert(HJ : SAMS C B A0 G H I) by (apply (conga2_sams__sams D E F G H I); try (apply conga_refl); auto).
destruct HJ as [_ [_ [J]]].
destruct HisiEH as [_ [_ [F1]]].
spliter.
assert_diffs.
assert(CongA C B J D' E' F').
{ apply (conga_trans _ _ _ D E F1); auto.
- apply (l11_22 _ _ _ A0 _ _ _ F); auto.
split.
left; split; apply not_one_side_two_sides; auto; apply (ncol_conga_ncol G H I); CongA.
split.
{ apply (sams2_suma2__conga456 A B C _ _ _ _ _ _ A' B' C'); auto.
apply (sams_chara _ _ _ _ _ _ A0); try (apply lea_refl); Between.
apply (conga3_suma__suma A B C C B A0 A B A0); try (apply conga_refl); try (apply conga_line); Between.
∃ A0.
repeat (split; CongA).
}
apply (conga_trans _ _ _ G H I); auto.
apply conga_sym; auto.
- apply (suma2__conga D E F G H I); auto.
∃ F1.
repeat (split; CongA).
}
apply (conga3_suma__suma A B C D' E' F' A B J); try (apply conga_refl); auto.
{ ∃ J.
split.
{ apply (suma2__conga C B A0 G H I).
∃ J; repeat (split; CongA).
apply (conga3_suma__suma D E F G H I D' E' F'); CongA.
}
split; CongA.
apply l9_9.
apply invert_two_sides; apply l9_2.
apply (l9_8_2 _ _ A0).
repeat split; Col; ∃ B; split; Col; Between.
apply not_two_sides_one_side; Col.
apply not_col_permutation_2.
apply (ncol_conga_ncol D' E' F'); CongA.
}
apply (suma2__conga A' B' C' G H I); auto.
apply (conga3_suma__suma A B A0 A0 B J A B J); try (apply conga_refl); auto; try (apply conga_line); Between.
∃ J.
repeat (split; CongA).
apply col123__nos; Col.
}
intro HB'out.
apply not_bet_out in HB'out; auto.
exfalso.
apply HNColB.
apply col_permutation_4.
apply out_col.
apply (out_lea__out _ _ _ A' B' C'); auto.
apply (sams_suma__lea123789 _ _ _ D E F); auto.
}
intro HNColB'.
clear dependent A0.
destruct HisiBE as [_ [_ [C1 HC1]]].
spliter.
assert_diffs.
assert(CongA A' B' C' A B C1).
{ apply (suma2__conga A B C D E F); auto.
apply (conga3_suma__suma A B C C B C1 A B C1); CongA.
∃ C1.
repeat (split; CongA).
}
assert(OS B C1 C A).
{ apply one_side_symmetry.
apply os_ts1324__os.
- apply invert_one_side.
apply not_two_sides_one_side; Col.
apply not_col_permutation_2; apply (ncol_conga_ncol A' B' C'); auto.
- apply not_one_side_two_sides; Col.
apply (ncol_conga_ncol D E F); CongA.
}
elim(Col_dec D' E' F').
{ intro HColE'.
elim(bet_dec D' E' F').
{ intro HE'Bet.
assert(HC0 : ∃ C0, Midpoint B C C0) by apply symmetric_point_construction.
destruct HC0 as [C0].
spliter.
assert_diffs.
assert(TS B C1 C C0).
{ repeat split; auto.
apply (ncol_conga_ncol D E F); CongA.
intro; apply HNColE; apply (col_conga_col C B C1); CongA; apply (l6_16_1 _ C0); Col.
∃ B.
split; Col; Between.
}
apply (conga3_suma__suma A B C C B C0 A B C0); try (apply conga_refl); auto.
∃ C0; repeat (split; CongA); apply col124__nos; Col.
apply conga_line; Between.
apply (suma2__conga A' B' C' G H I); auto.
apply (conga3_suma__suma A B C1 C1 B C0 A B C0); try (apply conga_refl); try solve [apply conga_sym; auto]; auto.
∃ C0; repeat (split; CongA); apply l9_9; apply (l9_8_2 _ _ C); auto.
apply (sams2_suma2__conga456 C B C1 _ _ _ _ _ _ C B C0); auto.
apply (sams_chara _ _ _ _ _ _ C0); try (apply lea_refl); Between.
apply (conga2_sams__sams D E F G H I); CongA.
∃ C0; repeat (split; CongA); apply l9_9; auto.
apply (conga3_suma__suma D E F G H I D' E' F'); try (apply conga_refl); try (apply conga_sym); auto.
apply conga_line; Between.
}
intro HE'out.
apply not_bet_out in HE'out; auto.
exfalso.
apply HNColE.
apply col_permutation_4.
apply out_col.
apply (out_lea__out _ _ _ D' E' F'); auto.
apply (sams_suma__lea123789 _ _ _ G H I); auto.
}
intro HNColE'.
clear dependent D0.
assert(HJ : SAMS C B C1 G H I) by (apply (conga2_sams__sams D E F G H I); CongA).
destruct HJ as [_ [_ [J]]].
destruct HisiEH as [_ [_ [F1 HF1]]].
spliter.
assert_diffs.
assert(CongA C B J D' E' F').
{ apply (conga_trans _ _ _ D E F1); auto.
- apply (l11_22 _ _ _ C1 _ _ _ F); auto.
split.
left; split; apply not_one_side_two_sides; auto; try solve [apply (ncol_conga_ncol G H I); CongA]; apply (ncol_conga_ncol D E F); CongA.
split.
CongA.
apply (conga_trans _ _ _ G H I); CongA.
- apply (suma2__conga D E F G H I); auto.
∃ F1.
repeat (split; CongA).
}
apply (conga3_suma__suma A B C C B J A B J); try (apply conga_refl); auto.
- ∃ J.
repeat (split; CongA).
apply l9_9.
apply l9_2.
apply (l9_8_2 _ _ C1).
apply l9_2; apply not_one_side_two_sides; auto; apply (ncol_conga_ncol D E F); CongA.
apply invert_one_side.
apply not_two_sides_one_side; auto; apply not_col_permutation_2.
apply (ncol_conga_ncol D E F); CongA.
apply (ncol_conga_ncol D' E' F'); CongA.
- apply (suma2__conga A' B' C' G H I); auto.
apply (conga3_suma__suma A B C1 C1 B J A B J); CongA.
∃ J.
repeat (split; CongA).
apply l9_9.
apply (l9_8_2 _ _ C); auto.
apply not_one_side_two_sides; auto.
apply (ncol_conga_ncol D E F); CongA.
apply (ncol_conga_ncol G H I); CongA.
Qed.
Lemma suma_assoc_2 : ∀ A B C D E F G H I K L M A' B' C' D' E' F',
SAMS A B C D E F → SAMS D E F G H I →
SumA A B C D E F A' B' C' → SumA D E F G H I D' E' F' →
SumA A B C D' E' F' K L M → SumA A' B' C' G H I K L M.
Proof.
intros A B C D E F G H I K L M A' B' C' D' E' F'.
intros.
apply suma_sym.
apply (suma_assoc_1 G H I D E F A B C K L M D' E' F'); SumA.
Qed.
Associativity of the sum of angles.
Lemma suma_assoc : ∀ A B C D E F G H I K L M A' B' C' D' E' F',
SAMS A B C D E F → SAMS D E F G H I →
SumA A B C D E F A' B' C' → SumA D E F G H I D' E' F' →
(SumA A' B' C' G H I K L M ↔ SumA A B C D' E' F' K L M).
Proof.
intros A B C D E F G H I K L M A' B' C' D' E' F'.
intros.
split.
apply (suma_assoc_1 _ _ _ D E F); auto.
apply (suma_assoc_2 _ _ _ D E F); auto.
Qed.
Lemma sams_assoc_1 : ∀ A B C D E F G H I A' B' C' D' E' F',
SAMS A B C D E F → SAMS D E F G H I →
SumA A B C D E F A' B' C' → SumA D E F G H I D' E' F' →
SAMS A' B' C' G H I → SAMS A B C D' E' F'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' Hsams1 Hsams2 Hs1 Hs2 Hsams1'.
assert_diffs.
elim(Col_dec A B C).
{ intro HColB.
destruct Hsams1 as [_ [[HEout|HBout]_]].
- apply (conga2_sams__sams A' B' C' G H I); auto.
apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto.
apply (out213_suma__conga D E F); auto.
- apply not_bet_out in HBout; auto.
apply sams_sym.
repeat split; auto.
∃ F'.
split.
apply l11_21_b; try (apply out_trivial); auto.
split.
apply col124__nos; Col.
apply not_two_sides_id.
}
intro HNColB.
elim(Col_dec D E F).
{ intro HColE.
destruct Hsams2 as [_ [[HHout|HEout]_]].
- apply (conga2_sams__sams A B C D E F); try (apply conga_refl); auto.
apply (out546_suma__conga _ _ _ G H I); auto.
- apply not_bet_out in HEout; auto.
apply (conga2_sams__sams A' B' C' G H I); auto.
apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto.
apply (out213_suma__conga D E F); auto.
}
intro HNColE.
elim(Col_dec G H I).
{ intro HColH.
apply sams_sym in Hsams2.
destruct Hsams2 as [_ [[HEout|HHout]_]].
exfalso; assert_cols; Col.
apply not_bet_out in HHout; auto.
apply (conga2_sams__sams A B C D E F); try (apply conga_refl); auto.
apply (out546_suma__conga _ _ _ G H I); auto.
}
intro HNColH.
split; auto.
split.
right; intro; assert_cols; Col.
assert(¬ Col A' B' C').
{ intro.
exfalso.
destruct Hsams1' as [_ [[|HB'out]_]].
assert_cols; Col.
apply not_bet_out in HB'out; auto.
apply HNColB.
apply col_permutation_4.
apply out_col.
apply (out_lea__out _ _ _ A' B' C'); auto.
apply (sams_suma__lea123789 _ _ _ D E F); auto.
}
assert(HC1 : ∃ C1, CongA C B C1 D E F ∧ ¬ OS B C A C1 ∧ ¬ TS A B C C1) by (destruct Hsams1 as [_ []]; auto).
destruct HC1 as [C1].
spliter.
assert_diffs.
assert(CongA A B C1 A' B' C') by (apply (suma2__conga A B C D E F); auto; ∃ C1; repeat (split; CongA)).
assert(HJ :∃ J, CongA C1 B J G H I ∧ ¬ OS B C1 C J ∧ ¬ TS C B C1 J).
{ apply (conga2_sams__sams _ _ _ _ _ _ C B C1 G H I) in Hsams2; CongA.
destruct Hsams2 as [_ [_ HJ]]; auto.
}
destruct HJ as [J [HJ1 [HJ2 HJ3]]].
spliter.
apply (conga2_sams__sams _ _ _ _ _ _ A B C1 C1 B J) in Hsams1'; CongA.
destruct Hsams1' as [_ [_ [J']]].
spliter.
assert_diffs.
assert (HUn : Out B J' J ∨ TS C1 B J' J) by (apply conga__or_out_ts; auto).
destruct HUn as [HJJ'|Hts].
{ ∃ J.
split.
2:split.
- apply (suma2__conga D E F G H I); auto.
apply (conga3_suma__suma C B C1 C1 B J C B J); try (apply conga_refl); auto.
∃ J.
repeat (split; CongA).
- elim(Col_dec C B J).
intro; apply col124__nos; Col.
intro.
apply l9_9.
apply l9_2.
apply (l9_8_2 _ _ C1).
apply l9_2; apply not_one_side_two_sides; Col; apply (ncol_conga_ncol D E F); CongA.
apply invert_one_side.
apply not_two_sides_one_side; Col.
apply not_col_permutation_2; apply (ncol_conga_ncol D E F); CongA.
- elim(Col_dec A B J).
intro; intro Hts; destruct Hts; spliter; Col.
intro.
apply l9_9_bis.
apply (one_side_transitivity _ _ _ C1).
apply not_two_sides_one_side; Col; apply not_col_permutation_2; apply (ncol_conga_ncol A' B' C'); CongA.
apply (one_side_transitivity _ _ _ J').
2: apply invert_one_side; apply out_one_side; Col.
apply not_two_sides_one_side; auto.
apply not_col_permutation_2; apply (ncol_conga_ncol A' B' C'); CongA.
apply not_col_permutation_2; apply (ncol_conga_ncol A B J); auto.
apply (out_conga A B J' A B J'); try (apply out_trivial); try (apply conga_refl); auto.
}
exfalso.
apply l9_2 in Hts.
apply invert_two_sides in Hts.
apply HJ2.
∃ J'.
split; auto.
apply (l9_8_2 _ _ A).
- apply not_one_side_two_sides; auto.
apply (ncol_conga_ncol A' B' C'); CongA.
apply (ncol_conga_ncol G H I); auto.
apply (conga_trans _ _ _ C1 B J); CongA.
- apply os_ts1324__os.
apply invert_one_side; apply not_two_sides_one_side; Col; apply not_col_permutation_2; apply (ncol_conga_ncol A' B' C'); CongA.
apply not_one_side_two_sides; Col; apply (ncol_conga_ncol D E F); CongA.
Qed.
Lemma sams_assoc_2 : ∀ A B C D E F G H I A' B' C' D' E' F',
SAMS A B C D E F → SAMS D E F G H I →
SumA A B C D E F A' B' C' → SumA D E F G H I D' E' F' →
SAMS A B C D' E' F' → SAMS A' B' C' G H I.
Proof.
intros A B C D E F G H I A' B' C' D' E' F'.
intros.
apply sams_sym.
apply (sams_assoc_1 G H I D E F A B C D' E' F'); SumA.
Qed.
Lemma sams_assoc : ∀ A B C D E F G H I A' B' C' D' E' F',
SAMS A B C D E F → SAMS D E F G H I →
SumA A B C D E F A' B' C' → SumA D E F G H I D' E' F' →
(SAMS A' B' C' G H I ↔ SAMS A B C D' E' F').
Proof.
intros A B C D E F.
split.
apply (sams_assoc_1 _ _ _ D E F); auto.
apply (sams_assoc_2 _ _ _ D E F); auto.
Qed.
Lemma sams_nos__nts : ∀ A B C J, SAMS A B C C B J → ¬ OS B C A J →
¬ TS A B C J.
Proof.
intros A B C J HIsi HNOS HTS.
destruct HIsi as [_ [HUn [J' [HConga [HNOS' HNTS]]]]].
destruct (conga__or_out_ts C B J J') as [HOut|HTS1]; CongA.
- apply HNTS.
apply l9_2, l9_8_2 with J; Side.
apply invert_one_side, out_one_side; trivial.
destruct HTS as [_ []]; Col.
- destruct HTS as [HNCol1 [HNCol2 _]].
assert_diffs.
absurd (OS B C J J'); Side.
destruct HTS1 as [HNCol _].
∃ A; split; apply not_one_side_two_sides; Col; Side.
apply not_col_permutation_3, ncol_conga_ncol with C B J; Col; CongA.
Qed.
Lemma conga_sams_nos__nts : ∀ A B C D E F J, SAMS A B C D E F → CongA C B J D E F → ¬ OS B C A J →
¬ TS A B C J.
Proof.
intros A B C D E F J HIsi HConga.
apply sams_nos__nts.
assert_diffs.
apply (conga2_sams__sams A B C D E F); CongA.
Qed.
If B <= B', E <= E' and B + E = B' + E', then B = B' and E = E'
Lemma sams_lea2_suma2__conga123 : ∀ A B C D E F G H I A' B' C' D' E' F',
LeA A B C A' B' C' → LeA D E F D' E' F' → SAMS A' B' C' D' E' F' →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G H I → CongA A B C A' B' C'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' HleaB HleaE Hisi' Hsuma Hsuma'.
assert_diffs.
apply (sams2_suma2__conga123 _ _ _ _ _ _ D E F G H I); auto.
apply (sams_lea2__sams _ _ _ _ _ _ A' B' C' D' E' F'); auto.
apply (sams_lea2__sams _ _ _ _ _ _ A' B' C' D' E' F'); Lea.
assert (Haux := ex_suma A' B' C' D E F).
destruct Haux as [G' [H' [I']]]; auto.
apply (conga3_suma__suma A' B' C' D E F G' H' I'); try (apply conga_refl); auto.
apply lea_asym.
apply (sams_lea456_suma2__lea A' B' C' D E F _ _ _ D' E' F'); auto.
apply (sams_lea123_suma2__lea A B C D E F _ _ _ A' B' C'); auto.
apply (sams_lea2__sams _ _ _ _ _ _ A' B' C' D' E' F'); Lea.
Qed.
Lemma sams_lea2_suma2__conga456 : ∀ A B C D E F G H I A' B' C' D' E' F',
LeA A B C A' B' C' → LeA D E F D' E' F' → SAMS A' B' C' D' E' F' →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G H I → CongA D E F D' E' F'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F'.
intros.
apply (sams_lea2_suma2__conga123 _ _ _ A B C G H I _ _ _ A' B' C'); SumA.
Qed.
If B + E = E, then B = 0
Lemma sams_suma__out213 : ∀ A B C D E F, SumA A B C D E F D E F → SAMS A B C D E F → Out B A C.
Proof.
intros A B C D E F HSuma HIsi.
assert_diffs.
apply (l11_21_a D E D).
apply out_trivial; auto.
apply sams_lea2_suma2__conga123 with D E F D E F D E F; Lea.
∃ F; repeat (split; CongA).
apply col123__nos; Col.
Qed.
Lemma sams_suma__out546 : ∀ A B C D E F, SumA A B C D E F A B C → SAMS A B C D E F → Out E D F.
Proof.
intros A B C D E F HSuma HIsi.
apply sams_suma__out213 with A B C.
apply suma_sym; trivial.
apply sams_sym; trivial.
Qed.
If B < B' and E <= E', then B + E < B' + E'
Lemma sams_lea_lta123_suma2__lta : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LtA A B C A' B' C' → LeA D E F D' E' F' → SAMS A' B' C' D' E' F' →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA G H I G' H' I'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I' HltaB HleaE Hisi' Hsuma Hsuma'.
assert_diffs.
split.
apply (sams_lea2_suma2__lea A B C D E F _ _ _ A' B' C' D' E' F'); Lea.
intro.
destruct HltaB as [HleaB HNConga].
apply HNConga.
apply (sams_lea2_suma2__conga123 _ _ _ D E F G H I _ _ _ D' E' F'); auto.
apply (conga3_suma__suma A' B' C' D' E' F' G' H' I'); CongA.
Qed.
Lemma sams_lea_lta456_suma2__lta : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LeA A B C A' B' C' → LtA D E F D' E' F' → SAMS A' B' C' D' E' F' →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA G H I G' H' I'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
apply (sams_lea_lta123_suma2__lta D E F A B C _ _ _ D' E' F' A' B' C'); SumA.
Qed.
Lemma sams_lta2_suma2__lta : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LtA A B C A' B' C' → LtA D E F D' E' F' → SAMS A' B' C' D' E' F' →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA G H I G' H' I'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
apply (sams_lea_lta123_suma2__lta A B C D E F _ _ _ A' B' C' D' E' F'); auto.
apply lta__lea; auto.
Qed.
If E >= E' and B + E <= B' + E', then B <= B'
Lemma sams_lea2_suma2__lea123 : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LeA D' E' F' D E F → LeA G H I G' H' I' → SAMS A B C D E F →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LeA A B C A' B' C'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
assert_diffs.
elim(lta_dec A' B' C' A B C).
2: intro; apply nlta__lea; auto.
intro Hlta.
exfalso.
assert(¬ LeA G H I G' H' I'); auto.
apply lta__nlea.
apply(sams_lea_lta123_suma2__lta A' B' C' D' E' F' _ _ _ A B C D E F); auto.
Qed.
Lemma sams_lea2_suma2__lea456 : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LeA A' B' C' A B C → LeA G H I G' H' I' → SAMS A B C D E F →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LeA D E F D' E' F'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
apply (sams_lea2_suma2__lea123 _ _ _ A B C G H I _ _ _ A' B' C' G' H' I'); try (apply suma_sym); auto.
apply sams_sym; assumption.
Qed.
If E > E' and B + E <= B' + E', then B < B'
Lemma sams_lea_lta456_suma2__lta123 : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LtA D' E' F' D E F → LeA G H I G' H' I' → SAMS A B C D E F →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA A B C A' B' C'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
assert_diffs.
elim(lea_dec A' B' C' A B C).
2: intro; apply nlea__lta; auto.
intro Hlea.
exfalso.
assert(¬ LeA G H I G' H' I'); auto.
apply lta__nlea.
apply(sams_lea_lta456_suma2__lta A' B' C' D' E' F' _ _ _ A B C D E F); auto.
Qed.
Lemma sams_lea_lta123_suma2__lta456 : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LtA A' B' C' A B C → LeA G H I G' H' I' → SAMS A B C D E F →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA D E F D' E' F'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
apply (sams_lea_lta456_suma2__lta123 _ _ _ A B C G H I _ _ _ A' B' C' G' H' I'); try (apply suma_sym); auto.
apply sams_sym; assumption.
Qed.
If E >= E' and B + E < B' + E', then B < B'
Lemma sams_lea_lta789_suma2__lta123 : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LeA D' E' F' D E F → LtA G H I G' H' I' → SAMS A B C D E F →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA A B C A' B' C'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
assert_diffs.
elim(lea_dec A' B' C' A B C).
2: intro; apply nlea__lta; auto.
intro Hlta.
exfalso.
assert(¬ LtA G H I G' H' I'); auto.
apply lea__nlta.
apply(sams_lea2_suma2__lea A' B' C' D' E' F' _ _ _ A B C D E F); auto.
Qed.
Lemma sams_lea_lta789_suma2__lta456 : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LeA A' B' C' A B C → LtA G H I G' H' I' → SAMS A B C D E F →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA D E F D' E' F'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
apply (sams_lea_lta789_suma2__lta123 _ _ _ A B C G H I _ _ _ A' B' C' G' H' I'); try (apply suma_sym); auto.
apply sams_sym; assumption.
Qed.
Lemma sams_lta2_suma2__lta123 : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LtA D' E' F' D E F → LtA G H I G' H' I' → SAMS A B C D E F →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA A B C A' B' C'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
apply (sams_lea_lta789_suma2__lta123 _ _ _ D E F G H I _ _ _ D' E' F' G' H' I'); auto.
apply lta__lea; assumption.
Qed.
Lemma sams_lta2_suma2__lta456 : ∀ A B C D E F G H I A' B' C' D' E' F' G' H' I',
LtA A' B' C' A B C → LtA G H I G' H' I' → SAMS A B C D E F →
SumA A B C D E F G H I → SumA A' B' C' D' E' F' G' H' I' → LtA D E F D' E' F'.
Proof.
intros A B C D E F G H I A' B' C' D' E' F' G' H' I'.
intros.
apply (sams_lea_lta789_suma2__lta456 A B C _ _ _ G H I A' B' C' _ _ _ G' H' I'); auto.
apply lta__lea; assumption.
Qed.
Lemma sams2_suma2__conga : ∀ A B C D E F A' B' C',
SAMS A B C A B C → SumA A B C A B C D E F →
SAMS A' B' C' A' B' C' → SumA A' B' C' A' B' C' D E F →
CongA A B C A' B' C'.
Proof.
intros A B C D E F A' B' C' HIsi HSuma HIsi' HSuma'.
assert_diffs.
destruct (lea_total A B C A' B' C'); trivial; [|apply conga_sym];
eapply sams_lea2_suma2__conga123; eauto.
Qed.
Lemma sams123231 : ∀ A B C, A ≠ B → A ≠ C → B ≠ C → SAMS A B C B C A.
Proof.
intros A B C.
intros.
assert(HA' := symmetric_point_construction A B).
destruct HA' as [A'].
assert_diffs.
apply (sams_chara _ _ _ _ _ _ A'); Between.
elim(Col_dec A B C).
{ intro HCol.
elim(bet_dec A C B).
{ intro HCBet.
apply conga__lea.
apply conga_line; Between.
apply (between_exchange3 A); Between.
}
intro.
apply l11_31_1; auto.
apply l6_6.
apply not_bet_out; Col.
}
intro.
apply lta__lea.
apply l11_41_aux; Col; Between.
Qed.
Lemma ncol_suma__ncol : ∀ A B C D E F, ¬ Col A B C → SumA A B C B C A D E F → ¬ Col D E F.
Proof.
intros A B C D E F HNCol HSuma HCol.
elim(bet_dec D E F).
- intro.
assert(HP := symmetric_point_construction A B).
destruct HP as [P].
assert_diffs.
assert(Hlta : LtA D E F A B P).
2: destruct Hlta as [Hlea HNConga]; apply HNConga; apply conga_line; Between.
assert(TS B C A P).
{ repeat split; Col.
intro; apply HNCol; ColR.
∃ B; Col; Between.
}
apply (sams_lea_lta456_suma2__lta A B C B C A _ _ _ A B C C B P); Lea.
apply l11_41_aux; Col; Between.
2: ∃ P; repeat (split; CongA); Side.
split; auto; split.
right; intro; apply HNCol; Col.
∃ P.
split; CongA.
split; Side.
intro Hts.
destruct Hts as [_ [Habs]].
apply Habs; Col.
- intro.
assert_diffs.
apply HNCol.
apply col_permutation_3.
apply out_col.
apply (out_lea__out _ _ _ D E F).
apply not_bet_out; Col.
apply (sams_suma__lea456789 A B C); auto.
apply sams123231; auto.
Qed.
Sum of two right angles is a straight angle:
90+90=180.
Lemma per2_suma__bet : ∀ A B C D E F G H I, Per A B C → Per D E F →
SumA A B C D E F G H I → Bet G H I.
Proof.
intros A B C D E F G H I HBRight HERight HSuma.
destruct HSuma as [A1 [HConga1 [HNos HConga2]]].
assert_diffs.
assert(Per A1 B C) by (apply (l11_17 D E F); CongA).
apply (bet_conga_bet A B A1); auto.
apply (col_two_sides_bet _ C).
apply col_permutation_2; apply (per_per_col _ _ C); auto.
apply not_one_side_two_sides; auto; apply per_not_col; auto.
Qed.
If 90+x=180 then x=90.
Lemma bet_per_suma__per456 : ∀ A B C D E F G H I, Per A B C → Bet G H I →
SumA A B C D E F G H I → Per D E F.
Proof.
intros A B C D E F G H I HPer HBet HSuma.
assert(HA1 := symmetric_point_construction A B).
destruct HA1 as [A1].
assert_diffs.
assert(¬ Col A B C) by (apply per_not_col; auto).
apply (l11_17 A B C); auto.
apply (sams2_suma2__conga456 A B C _ _ _ _ _ _ G H I); auto.
- apply (sams_chara _ _ _ _ _ _ A1); Between.
apply conga__lea.
apply conga_left_comm.
apply l11_18_1; Between; Perp.
- destruct HSuma as [F1 [HConga1 [HNos HConga2]]].
repeat split; auto.
right; intro; assert_cols; Col.
∃ F1.
repeat (split; auto).
intro Habs.
destruct Habs as [_ [Habs]].
apply Habs.
apply col_permutation_2.
apply bet_col.
apply (bet_conga_bet G H I); CongA.
- assert(HSuma' := ex_suma A B C A B C).
destruct HSuma' as [G' [H' [I']]]; auto.
assert_diffs.
apply (conga3_suma__suma A B C A B C G' H' I'); try (apply conga_refl); auto.
apply conga_line; auto.
apply (per2_suma__bet A B C A B C); auto.
Qed.
If x+90=180 then x=90.
Lemma bet_per_suma__per123 : ∀ A B C D E F G H I, Per D E F → Bet G H I →
SumA A B C D E F G H I → Per A B C.
Proof.
intros A B C D E F G H I HPer HBet HSuma.
apply (bet_per_suma__per456 D E F _ _ _ G H I); SumA.
Qed.
If x+x=180 then x=90.
Lemma bet_suma__per : ∀ A B C D E F, Bet D E F → SumA A B C A B C D E F →
Per A B C.
Proof.
intros A B C D E F HBet HSuma.
assert_diffs.
destruct HSuma as [A' [HConga1 [_ HConga2]]].
apply l8_2.
apply (l11_18_2 _ _ _ A'); CongA.
apply (bet_conga_bet D E F); CongA.
Qed.
If x<90 then x+x<180 (two lemmas).
Lemma acute__sams : ∀ A B C, Acute A B C → SAMS A B C A B C.
Proof.
intros A B C Hacute.
assert(HA' := symmetric_point_construction A B).
destruct HA' as [A'].
assert_diffs.
apply (sams_chara _ _ _ _ _ _ A'); Between.
apply lea_acute_obtuse; auto.
apply obtuse_sym.
apply (bet_acute__obtuse A); Between.
Qed.
Lemma acute_suma__nbet : ∀ A B C D E F, Acute A B C → SumA A B C A B C D E F → ¬ Bet D E F.
Proof.
intros A B C D E F Hacute HSuma.
assert_diffs.
intro.
apply (nlta A B C).
apply acute_per__lta; auto.
apply (bet_suma__per _ _ _ D E F); auto.
Qed.
If x>90 then x+x>180.
Lemma obtuse__nsams : ∀ A B C, Obtuse A B C → ¬ SAMS A B C A B C.
Proof.
intros A B C Hobtuse.
assert(HA' := symmetric_point_construction A B).
destruct HA' as [A'].
assert_diffs.
intro.
apply (nlta A B C).
apply (lea123456_lta__lta _ _ _ A' B C).
- apply lea_right_comm.
apply (sams_chara A); Between.
- apply acute_obtuse__lta; auto.
apply (bet_obtuse__acute A); Between.
Qed.
If x+x<180 then x<90.
Lemma nbet_sams_suma__acute : ∀ A B C D E F, ¬ Bet D E F → SAMS A B C A B C →
SumA A B C A B C D E F → Acute A B C.
Proof.
intros A B C D E F HNBet HIsi HSuma.
assert_diffs.
elim(angle_partition A B C); auto.
intro HUn.
exfalso.
destruct HUn.
- apply HNBet.
apply (per2_suma__bet A B C A B C); auto.
- assert(¬ SAMS A B C A B C); auto.
apply obtuse__nsams; auto.
Qed.
If x+x>180 then x>90.
Lemma nsams__obtuse : ∀ A B C, A ≠ B → B ≠ C → ¬ SAMS A B C A B C → Obtuse A B C.
Proof.
intros A B C HAB HBC HNIsi.
elim(angle_partition A B C); auto.
- intro.
exfalso.
apply HNIsi.
apply acute__sams; auto.
- intro HUn.
destruct HUn; auto.
exfalso.
apply HNIsi.
assert(HA' := symmetric_point_construction A B).
assert(HNCol : ¬ Col A B C) by (apply per_not_col; auto).
destruct HA' as [A'].
assert_diffs.
repeat split; auto.
right; intro; Col.
∃ A'.
split.
apply conga_right_comm; apply conga_sym; apply l11_18_1; Between; Perp.
split.
2: intro Hts; destruct Hts as [_ []]; assert_cols; Col.
apply l9_9.
repeat split; Col.
intro; apply HNCol; ColR.
∃ B; Col; Between.
Qed.
Sum of two straight angles is a null angle
Lemma bet2_suma__out : ∀ A B C D E F G H I, Bet A B C → Bet D E F →
SumA A B C D E F G H I → Out H G I.
Proof.
intros A B C D E F G H I HBet1 HBet2 HSuma.
assert_diffs.
apply (eq_conga_out A B).
apply (suma2__conga A B C D E F); trivial.
∃ A; split.
apply conga_line; Between.
split; CongA.
apply col123__nos; Col.
Qed.
Sum of two degenerate angles is degenerate
Lemma col2_suma__col : ∀ A B C D E F G H I, Col A B C → Col D E F →
SumA A B C D E F G H I → Col G H I.
Proof.
intros A B C D E F G H I HCol1 HCol2 HSuma.
destruct (bet_dec A B C).
destruct (bet_dec D E F).
- apply col_permutation_4, out_col, (bet2_suma__out A B C D E F); assumption.
- apply (col_conga_col A B C); trivial.
apply out546_suma__conga with D E F; trivial.
apply not_bet_out; assumption.
- apply (col_conga_col D E F); trivial.
apply (out213_suma__conga A B C); trivial.
apply not_bet_out; assumption.
Qed.
Lemma trisuma_distincts : ∀ A B C D E F, TriSumA A B C D E F →
A ≠ B ∧ B ≠ C ∧ A ≠ C ∧ D ≠ E ∧ E ≠ F.
Proof.
intros A B C D E F HTri.
destruct HTri as [G [H [I [HSuma HSuma1]]]].
assert_diffs; repeat split; auto.
Qed.
Lemma ex_trisuma : ∀ A B C, A ≠ B → B ≠ C → A ≠ C →
∃ D E F, TriSumA A B C D E F.
Proof.
intros A B C HAB HBC HAC.
destruct (ex_suma A B C B C A) as [G [H [I HSuma1]]]; auto.
assert_diffs.
destruct (ex_suma G H I C A B) as [D [E [F HSuma2]]]; auto.
∃ D; ∃ E; ∃ F; ∃ G; ∃ H; ∃ I.
split; assumption.
Qed.
Some permutation properties
Lemma trisuma_perm_231 : ∀ A B C D E F, TriSumA A B C D E F → TriSumA B C A D E F.
Proof.
intros A B C D E F HT.
destruct HT as [A1 [B1 [C1 [HT1 HT2]]]].
assert_diffs.
assert(Hex:= ex_suma B C A C A B).
destruct Hex as [B2 [C2 [A2 Hex]]]; auto.
∃ B2.
∃ C2.
∃ A2.
split; auto.
apply suma_sym.
apply (suma_assoc A B C B C A C A B D E F A1 B1 C1 B2 C2 A2); try (apply sams123231); auto.
Qed.
Lemma trisuma_perm_312 : ∀ A B C D E F, TriSumA A B C D E F → TriSumA C A B D E F.
Proof.
intros.
do 2 apply trisuma_perm_231.
assumption.
Qed.
Lemma trisuma_perm_321 : ∀ A B C D E F, TriSumA A B C D E F → TriSumA C B A D E F.
Proof.
intros A B C D E F HT.
destruct HT as [A1 [B1 [C1 [HT1 HT2]]]].
apply suma_sym in HT2.
assert_diffs.
assert(Hex:= ex_suma C A B A B C).
destruct Hex as [C2 [A2 [B2 Hex]]]; auto.
∃ C2.
∃ A2.
∃ B2.
split.
SumA.
apply suma_middle_comm.
apply (suma_assoc C A B A B C B C A D E F C2 A2 B2 A1 B1 C1); try (apply sams123231); auto.
Qed.
Lemma trisuma_perm_213 : ∀ A B C D E F, TriSumA A B C D E F → TriSumA B A C D E F.
Proof.
intros.
apply trisuma_perm_321.
apply trisuma_perm_312.
assumption.
Qed.
Lemma trisuma_perm_132 : ∀ A B C D E F, TriSumA A B C D E F → TriSumA A C B D E F.
Proof.
intros.
apply trisuma_perm_321.
apply trisuma_perm_231.
assumption.
Qed.
Lemma conga_trisuma__trisuma : ∀ A B C D E F D' E' F', TriSumA A B C D E F → CongA D E F D' E' F' →
TriSumA A B C D' E' F'.
Proof.
intros A B C D E F D' E' F' HTri HConga.
destruct HTri as [G [H [I [HSuma1 HSuma2]]]].
∃ G; ∃ H; ∃ I; split; trivial.
assert_diffs; apply (conga3_suma__suma G H I C A B D E F); CongA.
Qed.
Lemma trisuma2__conga : ∀ A B C D E F D' E' F', TriSumA A B C D E F → TriSumA A B C D' E' F' →
CongA D E F D' E' F'.
Proof.
intros A B C D E F D' E' F' HTri HTri'.
destruct HTri as [G [H [I [HSuma1 HSuma2]]]].
destruct HTri' as [G' [H' [I' [HSuma1' HSuma2']]]].
apply (suma2__conga G H I C A B); trivial.
assert_diffs.
apply (conga3_suma__suma G' H' I' C A B D' E' F'); CongA.
apply (suma2__conga A B C B C A); trivial.
Qed.
Lemma conga3_trisuma__trisuma : ∀ A B C D E F A' B' C', TriSumA A B C D E F →
CongA A B C A' B' C' → CongA B C A B' C' A' → CongA C A B C' A' B' →
TriSumA A' B' C' D E F.
Proof.
intros A B C D E F A' B' C' HTri HCongaB HCongaC HCongaA.
destruct HTri as [G [H [I [HSuma HSuma']]]].
assert_diffs; ∃ G; ∃ H; ∃ I; split;
[apply (conga3_suma__suma A B C B C A G H I)|apply (conga3_suma__suma G H I C A B D E F)]; CongA.
Qed.
The sum of the angles of a degenerate triangle is a straight angle
Lemma col_trisuma__bet : ∀ A B C P Q R, Col A B C → TriSumA A B C P Q R → Bet P Q R.
Proof.
intros A B C P Q R HCol HTri.
destruct HTri as [D [E [F []]]].
assert_diffs.
destruct HCol as [|[|]].
- apply (bet_conga_bet A B C); auto.
apply (conga_trans _ _ _ D E F).
apply (out546_suma__conga _ _ _ B C A); try (apply bet_out); Between.
apply (out546_suma__conga _ _ _ C A B); try (apply l6_6; apply bet_out); auto.
- apply (bet_conga_bet B C A); auto.
apply (conga_trans _ _ _ D E F).
apply (out213_suma__conga A B C); try (apply l6_6; apply bet_out); auto.
apply (out546_suma__conga _ _ _ C A B); try (apply bet_out); Between.
- apply (bet_conga_bet C A B); auto.
apply (out213_suma__conga D E F); auto.
apply (out_conga_out B C A); try (apply l6_6; apply bet_out); auto.
apply (out213_suma__conga A B C); try (apply bet_out); Between.
Qed.
Lemma suma_dec : ∀ A B C D E F G H I, SumA A B C D E F G H I ∨ ¬ SumA A B C D E F G H I.
Proof.
intros A B C D E F G H I.
destruct(eq_dec_points A B).
subst; right; intro; assert_diffs; auto.
destruct(eq_dec_points C B).
subst; right; intro; assert_diffs; auto.
destruct(eq_dec_points D E).
subst; right; intro; assert_diffs; auto.
destruct(eq_dec_points F E).
subst; right; intro; assert_diffs; auto.
destruct (ex_suma A B C D E F) as [G' [H' [I']]]; auto.
destruct(conga_dec G H I G' H' I') as [|HNCongA].
left; apply (conga3_suma__suma A B C D E F G' H' I'); CongA.
right.
intro.
apply HNCongA, (suma2__conga A B C D E F); auto.
Qed.
Lemma sams_dec : ∀ A B C D E F, SAMS A B C D E F ∨ ¬ SAMS A B C D E F.
Proof.
intros A B C D E F.
destruct(eq_dec_points A B).
subst; right; intro; assert_diffs; auto.
assert(HA' := symmetric_point_construction A B).
destruct HA' as [A'].
assert_diffs.
destruct(lea_dec D E F C B A') as [|HNlea].
left; apply (sams_chara _ _ _ _ _ _ A'); Between.
right.
intro.
apply HNlea, (sams_chara A); Between.
Qed.
End Suma_2.
Hint Resolve acute__sams sams123231 : suma.