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