proposition: Lemma acute2_suma2__conga : forall A B C D E F A' B' C', Acute A B C -> SumA A B C A B C D E F -> Acute 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'. apply sams2_suma2__conga; try apply acute__sams; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles