Have you ever questioned about the same definition of incenter and excenter in def.txt?
Have you ever questioned about the same definition of incenter and excenter in def.txt? Was it right or you give a wrong definition?
In line 73: incenter x a b c x : a b c a b c = ncoll a b c x : eqangle a b a x a x a c, eqangle c a c x c x c b; eqangle b c b x b x b a bisect a b c, bisect b c a
incenter2 x y z i a b c i : a b c, x : i b c, y : i c a, z : i a b a b c = ncoll a b c i : eqangle a b a i a i a c, eqangle c a c i c i c b; eqangle b c b i b i b a; x : coll x b c, perp i x b c; y : coll y c a, perp i y c a; z : coll z a b, perp i z a b; cong i x i y, cong i y i z incenter2 a b c
excenter x a b c x : a b c a b c = ncoll a b c x : eqangle a b a x a x a c, eqangle c a c x c x c b; eqangle b c b x b x b a bisect b a c, exbisect b c a
excenter2 x y z i a b c i : a b c, x : i b c, y : i c a, z : i a b a b c = ncoll a b c i : eqangle a b a i a i a c, eqangle c a c i c i c b; eqangle b c b i b i b a; x : coll x b c, perp i x b c; y : coll y c a, perp i y c a; z : coll z a b, perp i z a b; cong i x i y, cong i y i z excenter2 a b c