fact: Definition leq_big_internal_of T (b : big_rel_of T) (phb : phantom (rel T) b) := leq_big_internal_op (big_rel_class b).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype)