La solution avec Xcas

Le choix des paramètres est important ! Sans perte de généralité, on peut prendre l'origine du repère en B, et C sur l'axe des x d'abscisse a. Le point M est donc sur l'axe des x d'abscisse m < a .
Si on choisit comme paramètres les coordonnèes de A, Xcas n'arrive pas à faire les calculs (cf la remarque ci-après). Mais si on choisit comme paramètres les longueurs b et c des côtés AC et AB les calculs sont simples même si on ne définit pas les centres des cercles inscrits comme des barycentres : on peut indifférement mettre pour définir I :
I:=barycentre([A,m],[B,l1],[M,c]); (cf lemme2) ou
I:=normal(centre(inscrit(A,B,M))); (idem pour définir J et K) On tape :

B:=point(0);
supposons(a=[1,0,2,0.1]);
C:=point(a);
supposons(b=[0.9,0,2,0.1]);
supposons(c=[1.1,0,2,0.1]);
A:=inter(cercle(B,c),cercle(C,b))[1];
triangle(A,B,C);
supposons(m=[0.4,0,a,0.1]);
M:=point(m);
b1:=longueur(A,M);
I:=barycentre([A,m],[B,b1],[M,c]);
J:=barycentre([A,a-m],[C,b1],[M,b]);
K:=barycentre([A,a],[B,b],[C,c],affichage=1);
I1:=projection(droite(y=0),I,affichage=quadrant3);
J1:=projection(droite(y=0),J,affichage=quadrant4);
K1:=projection(droite(y=0),K,affichage=quadrant2+
                               epaisseur_point_2);

On obtient :

On tape :

simplify(2*longueur(B,K1)-a))

On obtient :

-b+c

cela prouve le lemme3 puisque CK1 = a - BK1 on a :

BK1 - CK1 = 2*BK1 - a = c - b = AB - AC

On tape en se servant du lemme1 pour définir P :

P:=I1+vecteur(M,J1):;

simplify(affixe(P))

On obtient :

(a-b+c)/2

Donc P est fixe.
On tape :

simplify(affixe(K1))

On obtient :

(a-b+c)/2

Donc P et K1 sont confondus.

Remarque On peut aussi faire faire le calcul à Xcas avec au départ plus de paramètres que nécessaire et donner ensuite les relations entre ces paramètres seulement à la fin des calculs.
On choisit comme paramètres :
a1 l'abscisse de A,
a l'abscisse de C,
m l'abscisse de M,
b1 la longueur de AM,
b la longueur de AC,
c la longueur de AB.
cos(B) le cosinus de l'angle B qu triangle ABC Ces paramètres vérifient :
a1 = c*cos(B)
b1² = m² + c² - 2m*c*cos(B)
b² = c² + a² -2a*c*cos(B)
Si on note i1 l'affixe de I1, j1 l'affixe de J1 et p1 l'affixe de P1, on a, avec les notations précédentes, PB - PC = 2*PB - a.
On tape :

i1:=affixe(barycentre([point(a1),m],[point(0),b1],[point(m),c]));
j1:=affixe(barycentre([point(a1),a-m],[point(m),b],[point(a),b1]));
p1:=simplify(i1+j1-m);
res:=simplify(2*p1-1);
res:=simplify(subst(subst(res,[a1=c*cos(B),b1^2=m^2+c^2-2*m*c*cos(B)]),
            cos(B)=(-b^2+c^2+a^2)/(2*c*a)));

On obtient alors facilement pour PB - PC = 2*PB - a=res :
-b+c
Donc PB - PC = c - b = AB - AC.