Dans ce billet j'ai posé l'exercice de montrer que la loi binaire

x¤y := x(y2+1)½+y(x2+1)½

définit une structure de groupe sur l'ensemble des réels. Le seul obstacle est l'associativité; la preuve n'est pas très difficile (il s'agit d'un simple transport de la loi + par le sinus hyperbolique). Mais avec Maple je n'arrive pas à faire la preuve par force brute; en effet, je ne sais pas comment faire en sorte que le logiciel simplifie l'expression concernée (tandis que le logiciel Xcas y arrive, comme l'a remarqué Tukikun).

Dans le même esprit, je me demande si quelqu'un arrive à démontrer avec Maple que, sur les courbes elliptiques (réelles), l'addition par la méthode des sécantes est associative. Je n'y suis pas arrivé.