mathlib3

c47c7874 - Prove that sqrt_aux is positive if f is