proposition: Lemma bet_suma__per : forall A B C D E F, Bet D E F -> SumA A B C A B C D E F -> Per A B C.
proof: Proof. intros A B C D E F HBet HSuma. assert_diffs. destruct HSuma as [A' [HConga1 [_ [_ HConga2]]]]. apply l8_2. apply (l11_18_2 _ _ _ A'); CongA. apply (bet_conga__bet D E F); CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles