proposition: Lemma high_school_exterior_angle_theorem : forall A B C B', A <> B -> B <> C -> A <> C -> A <> B' -> Bet B A B' -> SumA A B C B C A C A B'.
proof: Proof. intros A B C B'; intros. destruct (ex_suma A B C B C A) as [D [E [F HSuma]]]; auto. apply (conga3_suma__suma A B C B C A D E F); try apply conga_refl; auto. apply suppa2__conga123 with C A B. apply suma__suppa; assumption. apply suppa_sym, suppa_left_comm, bet__suppa; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec