fact: Definition prod_hrel A A' B B' (rA : A -> A' -> Type) (rB : B -> B' -> Type) : A * B -> A' * B' -> Type := fun x y => (rA x.1 y.1 * rB x.2 y.2)%type.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset bigop)