proposition: Lemma conga3_trisuma__trisuma : forall A B C D E F A' B' C', TriSumA A B C D E F -> CongA A B C A' B' C' -> CongA B C A B' C' A' -> CongA C A B C' A' B' -> TriSumA A' B' C' D E F.
proof: Proof. intros A B C D E F A' B' C' HTri HCongaB HCongaC HCongaA. destruct HTri as [G [H [I [HSuma HSuma']]]]. assert_diffs; exists G; exists H; exists I; split; [apply (conga3_suma__suma A B C B C A G H I)|apply (conga3_suma__suma G H I C A B D E F)]; CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles