https://github.com/math-comp/analysis/blob/7933dc1ebfcf48f44c18893e43762f120db10bef/theories/measure.v#L2702 indeed, we usually use `subdef`/`subproof` suffixes for internals