Lemmas slated for Mathlib

This module gathers auxiliary lemmas from the SardMoreira project that are candidates for upstreaming to Mathlib.