Égalité de polynomes
C'est peut-être pas le truc le plus urgent pour l'instant, mais c'est pas propre, et ça pourrait poser des problèmes pour la suite. Il faut faire un choix quant à notre définition de l'égalité de polynômes : soit on fait en sorte de pouvoir utiliser cette égalité dans des rewrite
en utilisant le module Setoid
, soit on change nos polynômes de manière à ce qu'ils aient une écriture réellement unique. Et je crois que la seule chose qui manque à cette fin soit d'interdire que les polynômes soient des constantes nulles (et le polynôme nul, on peut toujours le rajouter comme un cas particulier au dessus).
C'est pas du tout à faire tout de suite, c'est juste que l'idée soit marquée quelque part !