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