proposition: Lemma col_suma__col : forall A B C D E F, Col D E F -> SumA A B C B C A D E F -> Col A B C.
proof: Proof. intros A B C D E F HCol HSuma. destruct (col_dec A B C) as [|HNCol]; [trivial|]. exfalso. destruct (bet_dec D E F). - assert (HP := symmetric_point_construction A B). destruct HP as [P []]. assert_diffs. assert (Hlta : LtA D E F A B P); [|destruct Hlta as [Hlea HNConga]; apply HNConga; CongA]. assert (TS B C A P). apply bet__ts; Col. apply (sams_lea_lta456_suma2__lta A B C B C A _ _ _ A B C C B P); [Lea| |SumA..]. apply l11_41_aux; Col. - 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.
imports: GeoCoq.Tarski_dev.Ch11_angles