proposition: Lemma bet__sams : forall A B C P, A <> B -> B <> C -> P <> B -> Bet A B C -> SAMS A B P P B C.
proof: Proof. intros A B C P HAB HBC HPB HBet. apply bet_suma__sams with A B C. apply bet__suma; auto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles