[stdlib] add Fin and Vector lemmas

[mrhaandi]

• added to Fin
  • L_inj, R_inj, L_R_neq, case_L_R', case_L_R
• added to Vector
  • nth_append_L, nth_append_R, In_nth, nth_replace_eq, nth_replace_neq, replace_append_L, replace_append_R, append_const, map_append, map2_ext, append_inj, In_cons_iff, Forall_cons_iff, Forall_map, Forall_append, Forall_nth, Forall2_nth, Forall2_append, map_shiftin, fold_right_shiftin, In_shiftin, Forall_shiftin, rev_nil, rev_cons, rev_shiftin, rev_rev, map_rev, fold_left_rev_right, In_rev, Forall_rev

Notably, rev_rev and fold_left_rev_right lemmas are shown for the tail-recursive rev definition, in contrast to PR #16742.
Only properties of existing definitions are shown, no new definitions are added.

Closes rocq-prover/stdlib#54

• Added changelog.

[andres-erbsen]

I don't really understand Vector, but more lemmas about existing definitions seems like a good idea and I don't see any issues.

@coqbot run full ci

[mrhaandi]

It would be best to merge #16731 first, to work with the new definition here.

[mrhaandi]

Rebased, squared for easier review, and added changelog.

[mrhaandi]

This PR addresses the main concerns of rocq-prover/stdlib#54 and arguably closes it, by providing a good toolset to work with stdlib vectors.
Should I reflect this in the changelog and mark rocq-prover/stdlib#54 to be closed upon merge?

[andres-erbsen]

#16731 is merged; I imagine this PR will need to be rebased and adjusted.

As for what to do with rocq-prover/stdlib#54, I don't really see a reason to keep it open 🤷. I too prefer vectors defined using fix or sig, but I don't think keeping the issue helps with moving towards that (that issue doesn't have an alternative design, a list of considerations, or a list of affected developments). I'm not even sure Vector particularly stands out as cumbersome out of stuff bundled with Coq.

[mrhaandi]

#16731 is merged; I imagine this PR will need to be rebased and adjusted.

Rebased on top of master to account for #16731, and squashed. Now the present PR should be ready to go.

@coqbot run full ci

[andres-erbsen]

@coqbot merge now