Merged requested to merge ralf/op_instance_names into master
This was done using the following sed script:
sed -i -E 's/Instance ([a-zA-Z0-9_]+)( .*: (Op|P?Core|ValidN?|Unit) )/Instance \1_instance\2/' $(find iris/algebra -name "*.v")
Some manual fixup was needed; see the second commit for that. We might want to do something about some of these proofs?
This rename opens the opportunity of renaming lemmas such as
frac_valid' to remove the
' that makes no sense here.