Crit-Bit Iterators and 64-bit Compatibility

[vfukala]

Improvements of the crit-bit tree implementation verified using Live Verification

• Adding verified functions that allow iteration over a crit-bit tree
• Parametrizing the crit-bit tree implementation and proofs to be valid both for 32 and 64 bit width

[samuelgruetter]

This works with Coq 8.18, but not with Coq master:

File "/home/runner/work/bedrock2/bedrock2/LiveVerif/src/LiveVerifExamples/critbit.v", line 3982, characters 0-4:
Error:  (in proof map_take_ge_monotone): Attempt to save an incomplete proof
(there are remaining open goals).

My guess is that it's due to this change in the 8.20 release notes:

Changed: syntactic global references passed through the using clauses of auto-like tactics are now handled as plain references rather than interpreted terms. In particular, their typeclass arguments will not be inferred. In general, the previous behaviour can be emulated by replacing auto using foo with pose proof foo; auto (#18909, by Pierre-Marie Pédrot).

@vfukala would you mind trying out this fix?