Missing `padRight` properties

[gallais]

As noticed by one of my students, we only have a minimal number of properties involving padRight
and are missing its interaction with map, zipWith, lookup, update, etc.

http://agda.github.io/agda-stdlib/v2.2/Data.Vec.Properties.html#5752

[jamesmckinna]

Meta: feature issue type? (both: what is it, and how does this issue fall under such a rubric?)

Object: is there an abstract characterisation (as an adjoint? as hcf/lcm wrt some Divisibility ordering #2604 ) of what padRight is doing that would allow us to 'read off' the missing properties?