These lemmas were added in https://github.com/coq/coq/commit/ea05377f19404e0627a105b07c10ce72fb010af9, which was included in Coq 8.6. Time to remove our copies of them. :)