proposition: Lemma col2_suma__col : forall 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: 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.
imports: GeoCoq.Tarski_dev.Ch11_angles