proposition: Lemma inangle__suma : forall A B C P, InAngle P A B C -> SumA A B P P B C A B C.
proof: Proof. intros A B C P HInangle. assert (Hcopy := HInangle); destruct Hcopy as [HAB [HCB [HPB _]]]. exists C; repeat (split; CongA); Cop. elim (col_dec B P A). apply col123__nos. intro HNCol. elim (col_dec B P C). apply col124__nos. intro HNCol2. apply l9_9, invert_two_sides, in_angle_two_sides; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles