fact: Definition sub_hrel A B (R R' : A -> B -> Type) := forall (x : A) (y : B), R x y -> R' x y.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset bigop)