proposition: Lemma incenter_dec : forall A B C I, is_incenter I A B C \/ ~ is_incenter I A B C.
proof: Proof. intros A B C I. unfold is_incenter. destruct (col_dec A B C) as [HCOL | HNCOL]. right. intro HCOLIN. destruct HCOLIN as [HNCOL [HCONGAA [HCONGAB HCONGAC]]]. elim HNCOL;auto. destruct (conga_dec B A I I A C) as [HAC | HANC]. destruct (conga_dec A B I I B C) as [HBC | HBNC]. destruct (conga_dec A C I I C B) as [HCC | HCNC]. left;split;auto. right;intro HN. destruct HN as [HNCOL1 [HCONGA [HCONGAB HCONGAC]]]. elim HCNC;auto. right;intro HN. destruct HN as [HNCOL1 [HCONGA [HCONGAB HCONGAC]]]. elim HBNC;CongA. right;intro HN. destruct HN as [HNCOL1 [HCONGA [HCONGAB HCONGAC]]]. elim HANC;auto. Qed.
imports: GeoCoq.Highschool.bisector GeoCoq.Tarski_dev.Ch13_1