proposition: Lemma trisuma_dec : forall A B C P Q R, TriSumA A B C P Q R \/ ~ TriSumA A B C P Q R.
proof: Proof. intros A B C P Q R. destruct(eq_dec_points A B). subst; right; intros [D [E [F []]]]; assert_diffs; auto. destruct(eq_dec_points B C). subst; right; intros [D [E [F []]]]; assert_diffs; auto. destruct(eq_dec_points A C). subst; right; intros [D [E [F []]]]; assert_diffs; auto. destruct (ex_trisuma A B C) as [D [E [F]]]; auto. destruct (conga_dec D E F P Q R) as [|HNCong]. left; apply conga_trisuma__trisuma with D E F; assumption. right; intro; apply HNCong, (trisuma2__conga A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles