mathlib3

d0f90b61 - playing with chilapla's examples