proposition: Lemma bet_per_suma__per456 : forall 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: 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(HNCol : ~ 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 [HCop HConga2]]]]. repeat split; auto. right; intro; apply HNCol; Col. exists 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.
imports: GeoCoq.Tarski_dev.Ch11_angles