address deprecation warnings (`iota_add` ➔ `iotaD`)

mathcomp has deprecated iota_add in favor of iotaD.

As iotaD wasn't added until mathcomp 1.12, this patch breaks compatibility with earlier versions, which we just did anyway, so now is a good time to finally merge this.

Some cosmetic cleanups while we're touching the lemma, too.

Does not address deprecation warnings in classic Prosa, which is slowly aging away...