Améliorer les tactiques field
Il pourrait devenir important d'ajouter certains /modifiers/, comme indiqué ici : [https://coq.inria.fr/refman/addendum/ring.html#coq:cmd.add-field]. En effet, ils sont présents dans l'implémentation de field sur les réels (voir ici : [https://github.com/coq/coq/blob/master/plugins/setoid_ring/RealField.v])
Je ne comprends pas bien ce que fait completeness
. Si jamais tu as des idées, hésite pas. Normalement, j'ai déjà fait ce qu'il fallait pour les puissances, mais je n'arrive pas à comprendre si ça marche bien.