proposition: Lemma suma2_obtuse2__conga : forall A B C D E F A' B' C', Obtuse A B C -> SumA A B C A B C D E F -> Obtuse A' B' C' -> SumA A' B' C' A' B' C' D E F -> CongA A B C A' B' C'.
proof: Proof. intros A B C D E F A' B' C' HB HSuma HB' HSuma'. destruct (segment_construction A B A B) as [A0 []]. destruct (segment_construction A' B' A' B') as [A0' []]. assert_diffs. apply l11_13 with A0 A0'; Between. apply acute2_suma2__conga with D E F. apply (bet_obtuse__acute A); auto. apply bet2_suma__suma with A A; auto. apply (bet_obtuse__acute A'); auto. apply bet2_suma__suma with A' A'; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles