`fix` tactic without a name is deprecated.
The tactic form fix N where N is a number is deprecated as it depends on the name of the current lemma.
See https://github.com/coq/coq/pull/7196.
The backwards compatible fix is to use fix name_of_the_fixpoint N.
Edited by Ghost User