package coq-mathcomp-algebra-tactics

This library provides ring, field, lra, nra, and psatz tactics for algebraic structures of the Mathematical Components library. The ring and field tactics respectively work with any comRingType and fieldType. The other (Micromega) tactics work with any realDomainType or realFieldType. Their instance resolution is done through canonical structure inference. Therefore, they work with abstract rings and do not require Add Ring and Add Field commands. Another key feature of this library is that they automatically push down ring morphisms and additive functions to leaves of ring/field expressions before applying the proof procedures.