proposition: Lemma incenter_permut213 : forall A B C I, is_incenter I A B C -> is_incenter I B A C.
proof: Proof. unfold is_incenter. intros A B C I HIABC. destruct HIABC as [HNCOL [HCONGAA [HCONGAB HCONGAC]]]. split. intro;Col. split;auto. split;CongA. Qed.
imports: GeoCoq.Highschool.bisector GeoCoq.Tarski_dev.Ch13_1