proposition: Lemma ex_trisuma : forall A B C, A <> B -> B <> C -> A <> C -> exists D E F, TriSumA A B C D E F.
proof: Proof. intros A B C HAB HBC HAC. destruct (ex_suma A B C B C A) as [G [H [I HSuma1]]]; auto. assert_diffs. destruct (ex_suma G H I C A B) as [D [E [F HSuma2]]]; auto. exists D; exists E; exists F; exists G; exists H; exists I. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles