mathlib

3f0f5016 - Use proof by contradiction; fix lemma direction