HOL-Light: Add proof for x86_64 poly_tobytes#1383

hanno-becker merged 2 commits intomainpq-code-package/mlkem-native:mainfrom

hol-light-x86-tobytespq-code-package/mlkem-native:hol-light-x86-tobytesCopy head branch name to clipboard