Add list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_spec

Some more lemmas...

added 5 commits

• 12e2f67f...78b6bc41 - 4 commits from branch master
• f30a1ec2 - Add list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_spec

Compare with previous version

added 1 commit

• dfc3bc3e - Tweak proofs.

Compare with previous version

I pushed a tweak to the proofs since I couldn't really follow what was going on. For Z_to_little_endian_lookup_Some I now do induction on m (instead of i) as also done in other proofs. For little_endian_to_Z_spec I do induction on the Forall (instead of the list) and perform case distinction on whether i < n. That makes stuff much shorter.

I also tried to avoid all: since that's not something we commonly do in std++, and I tried to use rewrite ... by ... when possible.

I think the CI will fail on this MR now, but once !342 (merged) is through, and we have a more powerful lia, we should be fine.

Thanks for refactoring the proofs!

added 6 commits

• dfc3bc3e...ea36eb94 - 4 commits from branch master
• beb86674 - Add list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_spec
• 858cefdb - Tweak proofs.

Compare with previous version

added 1 commit

• 20fc3620 - list_fmap_inj1 -> list_fmap_inj_1

Compare with previous version

I rebased this branch and now the CI goes through. Should I add a CHANGELOG for this? From my side, I don't think that one is necessary and this MR is ready to go from my side.

resolved all threads

LGTM. Merging!

merged

mentioned in commit 0a8d6074

mentioned in merge request !349 (merged)