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...

requested review from @sbozhko

assigned to @bbb

added 2 commits

• 3ab704f7 - 1 commit from branch master
• 2d48a53f - address deprecation warnings (iota_add -> iotaD)

Compare with previous version

added 1 commit

• a1d79828 - address deprecation warnings in classic Prosa

Compare with previous version

Thanks!

approved this merge request

added 3 commits

• 9cc286c2 - 1 commit from branch master
• 6f8121d5 - address deprecation warnings (iota_add -> iotaD)
• 40facd1d - address deprecation warnings in classic Prosa

Compare with previous version

enabled an automatic merge when the pipeline for 40facd1d succeeds

canceled the automatic merge

enabled an automatic merge when the pipeline for 40facd1d succeeds

merged