ben defadd c'est défini de la seule façon naturelle possible, defmult aussi, et defdiv c'est x*1/y avec les 1/y qu'il a définis...

par contre defpower est effectivement différent de la définition usuelle qui dirait 0^0 = 1, et c'est vrai que comme a^(x+y) != a^x * a^y dans le cas général c'est un peu malhonnête de pas préciser qu'il y a plein de conditions supplémentaires alors que son système est censé éviter les conditions supplémentaires :/