proposition: Lemma sams_chara : forall 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: Proof. intros A B C D E F A' HAB HA'B HABA'. split. - intro Hint. destruct Hint as [_ [HUn [J [HJ1 [HJ2 [HJ3 HJ4]]]]]]. 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). repeat split; Col. intro; apply HNColB; apply (l6_16_1 B J C A); Col. exists B. split; Col; Between. } intro; apply l11_31_1; auto; apply l6_4_2; auto. } intro HNColE. apply lea_trans with C B J; [Lea|]. exists J. split; CongA. apply l11_24; apply (in_angle_reverse A); auto. assert (HTwo : TS B C A J). { apply cop_nos__ts; Cop. apply (ncol_conga_ncol D E F); CongA. } destruct HTwo as [_ [_ [X [HXCol HXBet]]]]. repeat split; auto. exists 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). apply bet_out; auto. } apply one_side_symmetry. apply cop_nts__os; Col; Cop. 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; exists A; repeat split; Between). apply (l11_21_a C B A'); auto. apply lea_asym; auto. apply l11_31_1; auto. } split; try left; auto. exists C. split. apply l11_21_b; try (apply out_trivial); auto. split. apply col124__nos; Col. split; Cop. apply not_two_sides_id. } intro HBNBet. assert (HBOut : Out B A C) by (apply not_bet_out; auto). split. right; auto. assert (HJ : exists 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]. exists J. split; CongA. split. apply col123__nos; Col. split; Cop. 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. exists C. split. apply l11_21_b; try (apply out_trivial); auto. split. apply col124__nos; Col. split; Cop. apply not_two_sides_id. } intro HNColE. split. right; intro; Col. assert (HJ : exists 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. exists J. split; CongA. split. apply l9_9; apply l9_2; apply invert_two_sides; auto. elim (col_dec A B J). { intro HColJ. split; Cop. 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. exists A; split; auto. apply l9_2, invert_two_sides, bet__ts; Col. } split; Cop. intro; apply HF. apply (col_preserves_two_sides A B); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles