mathlib3

f4b49f3e - Outline proof;Add material from Vladimir Goryachev & Stepan Nesterov