proposition: Lemma conga_trisuma__trisuma : forall A B C D E F D' E' F', TriSumA A B C D E F -> CongA D E F D' E' F' -> TriSumA A B C D' E' F'.
proof: Proof. intros A B C D E F D' E' F' HTri HConga. destruct HTri as [G [H [I [HSuma1 HSuma2]]]]. exists G; exists H; exists I; split; trivial. assert_diffs; apply (conga3_suma__suma G H I C A B D E F); CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles