proposition: Lemma incenter_permut321 : forall A B C I, is_incenter I A B C -> is_incenter I C B A.
proof: Proof. intros A B C I HIABC. apply (incenter_permut312 B A C I). apply (incenter_permut213 A B C I);auto. Qed.
imports: GeoCoq.Highschool.bisector GeoCoq.Tarski_dev.Ch13_1