proposition: Lemma suma_dec : forall A B C D E F G H I, SumA A B C D E F G H I \/ ~ SumA A B C D E F G H I.
proof: Proof. intros A B C D E F G H I. destruct(eq_dec_points A B). subst; right; intro; assert_diffs; auto. destruct(eq_dec_points C B). subst; right; intro; assert_diffs; auto. destruct(eq_dec_points D E). subst; right; intro; assert_diffs; auto. destruct(eq_dec_points F E). subst; right; intro; assert_diffs; auto. destruct (ex_suma A B C D E F) as [G' [H' [I']]]; auto. destruct(conga_dec G H I G' H' I') as [|HNCongA]. left; apply (conga3_suma__suma A B C D E F G' H' I'); CongA. right. intro. apply HNCongA, (suma2__conga A B C D E F); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles