proposition: Lemma bet2_suma__out : forall 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: 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. exists A. repeat (split; CongA); Cop. apply col123__nos; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles