https://github.com/affeldt-aist/trajectories/blob/a0a147cf08c3f3a5eebef5a559c0487be241bcdf/theories/preliminaries_hull.v#L15 Should use `'Z_p` instead of `'I_p` though, but might require a bit of work.
