Fix #110 (stabilize field tactic)

[proux01]

Fix #110

This doesn't work with no_check but no_check doesn't lake much sense in this context anway, as it's essentially meant to be used wrapped in abstract, hence for goal-terminating tactics.

[pi8027]

The no_check stuff is there to skip only the check that the reified term indeed evaluates back to the goal. I don't see how this is related to post-processing the proof obligation.

[proux01]

My bad, I confused that with the common abstract/no_check pattern to speed up Qed.
Then, I guess we can do it that way.

[proux01]

The CI error is probably due to some stalled Docker image, not sure there is much we can do about that.

[proux01]

Now that affeldt-aist/infotheo#178 is merged, let's merge (and hope it doesn't break too much reverse dependencies).

[pi8027]

Apery seems broken.

[proux01]

Should be fixed by rocq-community/apery#38