Library mathcomp.ssreflect.ssrfun

From Coq Require Export ssrfun.
From mathcomp Require Export ssrnotations.