add iff lemma for '✓ (to_agree a ⋅ to_agree b)'

This seems like such a clear characterization of agreement that I wonder why we do not have this already.

merged

mentioned in commit 2d8560ca