proposition: Lemma bet__suma : forall A B C P, A <> B -> B <> C -> P <> B -> Bet A B C -> SumA A B P P B C A B C.
proof: Proof. intros A B C P HAB HBC HPB HBet. apply inangle__suma; Side. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles