[Iris-Club] Final breaking changes before Iris 3.0

[Ralf Jung]

Hi all,

> The actual module name is
> algebra.deprecated.dec_agree.

Indeed, sorry for the confusion.  I renamed it because it turned out that

  From iris Require Import dec_agree.

does not actually continue to work.  The reason I addded _deprecated
even to the submodule name is that I want to maintain the following
invariant: If grepping for "deprecated" produces no results, then
nothing deprecated can possibly be used.

Kind regards,
Ralf