mathlib3

57cc3843 - chore(integration): missing lemmas (#7364)

chore(integration): missing lemmas (#7364) These are still preliminaries for derivation of parametric integrals. From the sphere eversion project