another bit from Simuliris, original proof by @msammler
changed the description
LGTM.
mentioned in commit 9faffcdd
merged