[Add] padRight properties to Data.Vec.Properties

[e-mniang]

This PR adds several equational properties for padRight to Data.Vec.Properties, extending the standard vector operations toolkit with useful lemmas for reasoning about padding on the right.

Added properties:

-     padRight-lookup: accessing a padded vector retrieves the original values at valid indices

-     padRight-map : padRight commutes with map

-     padRight-zipWith : padRight commutes with zipWith

-     padRight-zipWith₁: generalizes padRight-zipWith for different vector lengths

-     padRight-take: recovers the original prefix with take

-     padRight-drop: the suffix added by padding equals replicate

-     padRight-updateAt: updates on padded vectors correspond to updates on the original vectors

Each property is proven by structural induction and uses standard lemmas such as zipWith-replicate, map-replicate, and inject≤.

---

Authored by : @jmougeot

[jamesmckinna]

See also: #2770 . Even if the types of the Base operations are not (yet) changed, their properties should, where possible, be written to reflect that they only make irrelevant use of their m ≤ n arguments... UPDATED hmm, but it's not quite as simple as I'd hoped (and suggested as changes) unless we also make the changes proposed in #2770 which allow padRight to reduce more eagerly under weaker assumptions about the proofs of m ≤ n...

Tat being the case, I'll shout out to @JacquesCarette as to whether we go for this PR as is, and refactor downstream, or mark this blocking on #2770 ?

[jamesmckinna]

I should have minded my manners better, and thanked you for the PR before piling in with my nitpicks! These are all, in whatever form they eventually take, a useful contribution... and since padRight goes hand-in-hand with truncate, we should perhaps welcome a follow-up PR with the corresponding lemmas for truncate too?

[e-mniang]

Hi!
Thanks for your comments! I've made the necessary changes based on your feedback. I just had a small issue with the last point — the irrelevant part of the type signature.
Looking forward to your review of this version!

Great idea for the lemmas for truncate, will definitely look into that!